[GOAL]
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
finsetIcc : α → α → Finset α
mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b
a b x : α
⊢ x ∈ (fun a b => filter (fun x => ¬b ≤ x) (finsetIcc a b)) a b ↔ a ≤ x ∧ x < b
[PROOFSTEP]
rw [Finset.mem_filter, mem_Icc, and_assoc, lt_iff_le_not_le]
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
finsetIcc : α → α → Finset α
mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b
a b x : α
⊢ x ∈ (fun a b => filter (fun x => ¬x ≤ a) (finsetIcc a b)) a b ↔ a < x ∧ x ≤ b
[PROOFSTEP]
rw [Finset.mem_filter, mem_Icc, and_right_comm, lt_iff_le_not_le]
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
finsetIcc : α → α → Finset α
mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b
a b x : α
⊢ x ∈ (fun a b => filter (fun x => ¬x ≤ a ∧ ¬b ≤ x) (finsetIcc a b)) a b ↔ a < x ∧ x < b
[PROOFSTEP]
rw [Finset.mem_filter, mem_Icc, and_and_and_comm, lt_iff_le_not_le, lt_iff_le_not_le]
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : DecidableEq α
finsetIcc : α → α → Finset α
mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b
a b x : α
⊢ x ∈ (fun a b => filter (fun x => x ≠ b) (finsetIcc a b)) a b ↔ a ≤ x ∧ x < b
[PROOFSTEP]
rw [Finset.mem_filter, mem_Icc, and_assoc, lt_iff_le_and_ne]
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : DecidableEq α
finsetIcc : α → α → Finset α
mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b
a b x : α
⊢ x ∈ (fun a b => filter (fun x => a ≠ x) (finsetIcc a b)) a b ↔ a < x ∧ x ≤ b
[PROOFSTEP]
rw [Finset.mem_filter, mem_Icc, and_right_comm, lt_iff_le_and_ne]
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : DecidableEq α
finsetIcc : α → α → Finset α
mem_Icc : ∀ (a b x : α), x ∈ finsetIcc a b ↔ a ≤ x ∧ x ≤ b
a b x : α
⊢ x ∈ (fun a b => filter (fun x => a ≠ x ∧ x ≠ b) (finsetIcc a b)) a b ↔ a < x ∧ x < b
[PROOFSTEP]
rw [Finset.mem_filter, mem_Icc, and_and_and_comm, lt_iff_le_and_ne, lt_iff_le_and_ne]
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
finsetIci : α → Finset α
mem_Ici : ∀ (a x : α), x ∈ finsetIci a ↔ a ≤ x
a x : α
⊢ x ∈ (fun a => filter (fun x => ¬x ≤ a) (finsetIci a)) a ↔ a < x
[PROOFSTEP]
rw [mem_filter, mem_Ici, lt_iff_le_not_le]
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : DecidableEq α
finsetIci : α → Finset α
mem_Ici : ∀ (a x : α), x ∈ finsetIci a ↔ a ≤ x
a x : α
⊢ x ∈ (fun a => filter (fun x => a ≠ x) (finsetIci a)) a ↔ a < x
[PROOFSTEP]
rw [mem_filter, mem_Ici, lt_iff_le_and_ne]
[GOAL]
α : Type u_1
inst✝¹ : Preorder α
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
finsetIic : α → Finset α
mem_Iic : ∀ (a x : α), x ∈ finsetIic a ↔ x ≤ a
a x : α
⊢ x ∈ (fun a => filter (fun x => ¬a ≤ x) (finsetIic a)) a ↔ x < a
[PROOFSTEP]
rw [mem_filter, mem_Iic, lt_iff_le_not_le]
[GOAL]
α : Type u_1
inst✝¹ : PartialOrder α
inst✝ : DecidableEq α
finsetIic : α → Finset α
mem_Iic : ∀ (a x : α), x ∈ finsetIic a ↔ x ≤ a
a x : α
⊢ x ∈ (fun a => filter (fun x => x ≠ a) (finsetIic a)) a ↔ x < a
[PROOFSTEP]
rw [mem_filter, mem_Iic, lt_iff_le_and_ne]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : OrderTop α
a✝ x✝ a x : α
⊢ x ∈ (fun b => Icc b ⊤) a ↔ a ≤ x
[PROOFSTEP]
rw [mem_Icc, and_iff_left le_top]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : LocallyFiniteOrder α
inst✝ : OrderTop α
a✝ x✝ a x : α
⊢ x ∈ (fun b => Ioc b ⊤) a ↔ a < x
[PROOFSTEP]
rw [mem_Ioc, and_iff_left le_top]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : OrderBot α
inst✝ : LocallyFiniteOrder α
b x✝ a x : α
⊢ x ∈ Icc ⊥ a ↔ x ≤ a
[PROOFSTEP]
rw [mem_Icc, and_iff_right bot_le]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : OrderBot α
inst✝ : LocallyFiniteOrder α
b x✝ a x : α
⊢ x ∈ Ico ⊥ a ↔ x < a
[PROOFSTEP]
rw [mem_Ico, and_iff_right bot_le]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b x : α
⊢ x ∈ Icc a b ↔ a ≤ x ∧ x ≤ b
[PROOFSTEP]
rw [Icc, ← Finset.mem_def, Finset.mem_Icc]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b x : α
⊢ x ∈ Ico a b ↔ a ≤ x ∧ x < b
[PROOFSTEP]
rw [Ico, ← Finset.mem_def, Finset.mem_Ico]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b x : α
⊢ x ∈ Ioc a b ↔ a < x ∧ x ≤ b
[PROOFSTEP]
rw [Ioc, ← Finset.mem_def, Finset.mem_Ioc]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrder α
a b x : α
⊢ x ∈ Ioo a b ↔ a < x ∧ x < b
[PROOFSTEP]
rw [Ioo, ← Finset.mem_def, Finset.mem_Ioo]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderTop α
a x : α
⊢ x ∈ Ici a ↔ a ≤ x
[PROOFSTEP]
rw [Ici, ← Finset.mem_def, Finset.mem_Ici]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderTop α
a x : α
⊢ x ∈ Ioi a ↔ a < x
[PROOFSTEP]
rw [Ioi, ← Finset.mem_def, Finset.mem_Ioi]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderBot α
b x : α
⊢ x ∈ Iic b ↔ x ≤ b
[PROOFSTEP]
rw [Iic, ← Finset.mem_def, Finset.mem_Iic]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderBot α
b x : α
⊢ x ∈ Iio b ↔ x < b
[PROOFSTEP]
rw [Iio, ← Finset.mem_def, Finset.mem_Iio]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h : ∀ (a b : α), Set.Finite (Set.Icc a b)
a b x : α
⊢ x ∈ (fun a b => Set.Finite.toFinset (_ : Set.Finite (Set.Icc a b))) a b ↔ a ≤ x ∧ x ≤ b
[PROOFSTEP]
rw [Set.Finite.mem_toFinset, Set.mem_Icc]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : Preorder β
inst✝² : Fintype α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
a b x : α
⊢ x ∈ (fun a b => Set.toFinset (Set.Icc a b)) a b ↔ a ≤ x ∧ x ≤ b
[PROOFSTEP]
simp only [Set.mem_toFinset, Set.mem_Icc]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : Preorder β
inst✝² : Fintype α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
a b x : α
⊢ x ∈ (fun a b => Set.toFinset (Set.Ico a b)) a b ↔ a ≤ x ∧ x < b
[PROOFSTEP]
simp only [Set.mem_toFinset, Set.mem_Ico]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : Preorder β
inst✝² : Fintype α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
a b x : α
⊢ x ∈ (fun a b => Set.toFinset (Set.Ioc a b)) a b ↔ a < x ∧ x ≤ b
[PROOFSTEP]
simp only [Set.mem_toFinset, Set.mem_Ioc]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : Preorder β
inst✝² : Fintype α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
a b x : α
⊢ x ∈ (fun a b => Set.toFinset (Set.Ioo a b)) a b ↔ a < x ∧ x < b
[PROOFSTEP]
simp only [Set.mem_toFinset, Set.mem_Ioo]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h₀ h₁ : LocallyFiniteOrder α
⊢ h₀ = h₁
[PROOFSTEP]
cases' h₀ with h₀_finset_Icc h₀_finset_Ico h₀_finset_Ioc h₀_finset_Ioo h₀_finset_mem_Icc h₀_finset_mem_Ico
  h₀_finset_mem_Ioc h₀_finset_mem_Ioo
[GOAL]
case mk
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h₁ : LocallyFiniteOrder α
h₀_finset_Icc h₀_finset_Ico h₀_finset_Ioc h₀_finset_Ioo : α → α → Finset α
h₀_finset_mem_Icc : ∀ (a b x : α), x ∈ h₀_finset_Icc a b ↔ a ≤ x ∧ x ≤ b
h₀_finset_mem_Ico : ∀ (a b x : α), x ∈ h₀_finset_Ico a b ↔ a ≤ x ∧ x < b
h₀_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₀_finset_Ioc a b ↔ a < x ∧ x ≤ b
h₀_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₀_finset_Ioo a b ↔ a < x ∧ x < b
⊢ { finsetIcc := h₀_finset_Icc, finsetIco := h₀_finset_Ico, finsetIoc := h₀_finset_Ioc, finsetIoo := h₀_finset_Ioo,
      finset_mem_Icc := h₀_finset_mem_Icc, finset_mem_Ico := h₀_finset_mem_Ico, finset_mem_Ioc := h₀_finset_mem_Ioc,
      finset_mem_Ioo := h₀_finset_mem_Ioo } =
    h₁
[PROOFSTEP]
cases' h₁ with h₁_finset_Icc h₁_finset_Ico h₁_finset_Ioc h₁_finset_Ioo h₁_finset_mem_Icc h₁_finset_mem_Ico
  h₁_finset_mem_Ioc h₁_finset_mem_Ioo
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h₀_finset_Icc h₀_finset_Ico h₀_finset_Ioc h₀_finset_Ioo : α → α → Finset α
h₀_finset_mem_Icc : ∀ (a b x : α), x ∈ h₀_finset_Icc a b ↔ a ≤ x ∧ x ≤ b
h₀_finset_mem_Ico : ∀ (a b x : α), x ∈ h₀_finset_Ico a b ↔ a ≤ x ∧ x < b
h₀_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₀_finset_Ioc a b ↔ a < x ∧ x ≤ b
h₀_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₀_finset_Ioo a b ↔ a < x ∧ x < b
h₁_finset_Icc h₁_finset_Ico h₁_finset_Ioc h₁_finset_Ioo : α → α → Finset α
h₁_finset_mem_Icc : ∀ (a b x : α), x ∈ h₁_finset_Icc a b ↔ a ≤ x ∧ x ≤ b
h₁_finset_mem_Ico : ∀ (a b x : α), x ∈ h₁_finset_Ico a b ↔ a ≤ x ∧ x < b
h₁_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₁_finset_Ioc a b ↔ a < x ∧ x ≤ b
h₁_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₁_finset_Ioo a b ↔ a < x ∧ x < b
⊢ { finsetIcc := h₀_finset_Icc, finsetIco := h₀_finset_Ico, finsetIoc := h₀_finset_Ioc, finsetIoo := h₀_finset_Ioo,
      finset_mem_Icc := h₀_finset_mem_Icc, finset_mem_Ico := h₀_finset_mem_Ico, finset_mem_Ioc := h₀_finset_mem_Ioc,
      finset_mem_Ioo := h₀_finset_mem_Ioo } =
    { finsetIcc := h₁_finset_Icc, finsetIco := h₁_finset_Ico, finsetIoc := h₁_finset_Ioc, finsetIoo := h₁_finset_Ioo,
      finset_mem_Icc := h₁_finset_mem_Icc, finset_mem_Ico := h₁_finset_mem_Ico, finset_mem_Ioc := h₁_finset_mem_Ioc,
      finset_mem_Ioo := h₁_finset_mem_Ioo }
[PROOFSTEP]
have hIcc : h₀_finset_Icc = h₁_finset_Icc := by
  ext a b x
  rw [h₀_finset_mem_Icc, h₁_finset_mem_Icc]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h₀_finset_Icc h₀_finset_Ico h₀_finset_Ioc h₀_finset_Ioo : α → α → Finset α
h₀_finset_mem_Icc : ∀ (a b x : α), x ∈ h₀_finset_Icc a b ↔ a ≤ x ∧ x ≤ b
h₀_finset_mem_Ico : ∀ (a b x : α), x ∈ h₀_finset_Ico a b ↔ a ≤ x ∧ x < b
h₀_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₀_finset_Ioc a b ↔ a < x ∧ x ≤ b
h₀_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₀_finset_Ioo a b ↔ a < x ∧ x < b
h₁_finset_Icc h₁_finset_Ico h₁_finset_Ioc h₁_finset_Ioo : α → α → Finset α
h₁_finset_mem_Icc : ∀ (a b x : α), x ∈ h₁_finset_Icc a b ↔ a ≤ x ∧ x ≤ b
h₁_finset_mem_Ico : ∀ (a b x : α), x ∈ h₁_finset_Ico a b ↔ a ≤ x ∧ x < b
h₁_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₁_finset_Ioc a b ↔ a < x ∧ x ≤ b
h₁_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₁_finset_Ioo a b ↔ a < x ∧ x < b
⊢ h₀_finset_Icc = h₁_finset_Icc
[PROOFSTEP]
ext a b x
[GOAL]
case h.h.a
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h₀_finset_Icc h₀_finset_Ico h₀_finset_Ioc h₀_finset_Ioo : α → α → Finset α
h₀_finset_mem_Icc : ∀ (a b x : α), x ∈ h₀_finset_Icc a b ↔ a ≤ x ∧ x ≤ b
h₀_finset_mem_Ico : ∀ (a b x : α), x ∈ h₀_finset_Ico a b ↔ a ≤ x ∧ x < b
h₀_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₀_finset_Ioc a b ↔ a < x ∧ x ≤ b
h₀_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₀_finset_Ioo a b ↔ a < x ∧ x < b
h₁_finset_Icc h₁_finset_Ico h₁_finset_Ioc h₁_finset_Ioo : α → α → Finset α
h₁_finset_mem_Icc : ∀ (a b x : α), x ∈ h₁_finset_Icc a b ↔ a ≤ x ∧ x ≤ b
h₁_finset_mem_Ico : ∀ (a b x : α), x ∈ h₁_finset_Ico a b ↔ a ≤ x ∧ x < b
h₁_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₁_finset_Ioc a b ↔ a < x ∧ x ≤ b
h₁_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₁_finset_Ioo a b ↔ a < x ∧ x < b
a b x : α
⊢ x ∈ h₀_finset_Icc a b ↔ x ∈ h₁_finset_Icc a b
[PROOFSTEP]
rw [h₀_finset_mem_Icc, h₁_finset_mem_Icc]
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h₀_finset_Icc h₀_finset_Ico h₀_finset_Ioc h₀_finset_Ioo : α → α → Finset α
h₀_finset_mem_Icc : ∀ (a b x : α), x ∈ h₀_finset_Icc a b ↔ a ≤ x ∧ x ≤ b
h₀_finset_mem_Ico : ∀ (a b x : α), x ∈ h₀_finset_Ico a b ↔ a ≤ x ∧ x < b
h₀_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₀_finset_Ioc a b ↔ a < x ∧ x ≤ b
h₀_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₀_finset_Ioo a b ↔ a < x ∧ x < b
h₁_finset_Icc h₁_finset_Ico h₁_finset_Ioc h₁_finset_Ioo : α → α → Finset α
h₁_finset_mem_Icc : ∀ (a b x : α), x ∈ h₁_finset_Icc a b ↔ a ≤ x ∧ x ≤ b
h₁_finset_mem_Ico : ∀ (a b x : α), x ∈ h₁_finset_Ico a b ↔ a ≤ x ∧ x < b
h₁_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₁_finset_Ioc a b ↔ a < x ∧ x ≤ b
h₁_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₁_finset_Ioo a b ↔ a < x ∧ x < b
hIcc : h₀_finset_Icc = h₁_finset_Icc
⊢ { finsetIcc := h₀_finset_Icc, finsetIco := h₀_finset_Ico, finsetIoc := h₀_finset_Ioc, finsetIoo := h₀_finset_Ioo,
      finset_mem_Icc := h₀_finset_mem_Icc, finset_mem_Ico := h₀_finset_mem_Ico, finset_mem_Ioc := h₀_finset_mem_Ioc,
      finset_mem_Ioo := h₀_finset_mem_Ioo } =
    { finsetIcc := h₁_finset_Icc, finsetIco := h₁_finset_Ico, finsetIoc := h₁_finset_Ioc, finsetIoo := h₁_finset_Ioo,
      finset_mem_Icc := h₁_finset_mem_Icc, finset_mem_Ico := h₁_finset_mem_Ico, finset_mem_Ioc := h₁_finset_mem_Ioc,
      finset_mem_Ioo := h₁_finset_mem_Ioo }
[PROOFSTEP]
have hIco : h₀_finset_Ico = h₁_finset_Ico := by
  ext a b x
  rw [h₀_finset_mem_Ico, h₁_finset_mem_Ico]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h₀_finset_Icc h₀_finset_Ico h₀_finset_Ioc h₀_finset_Ioo : α → α → Finset α
h₀_finset_mem_Icc : ∀ (a b x : α), x ∈ h₀_finset_Icc a b ↔ a ≤ x ∧ x ≤ b
h₀_finset_mem_Ico : ∀ (a b x : α), x ∈ h₀_finset_Ico a b ↔ a ≤ x ∧ x < b
h₀_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₀_finset_Ioc a b ↔ a < x ∧ x ≤ b
h₀_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₀_finset_Ioo a b ↔ a < x ∧ x < b
h₁_finset_Icc h₁_finset_Ico h₁_finset_Ioc h₁_finset_Ioo : α → α → Finset α
h₁_finset_mem_Icc : ∀ (a b x : α), x ∈ h₁_finset_Icc a b ↔ a ≤ x ∧ x ≤ b
h₁_finset_mem_Ico : ∀ (a b x : α), x ∈ h₁_finset_Ico a b ↔ a ≤ x ∧ x < b
h₁_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₁_finset_Ioc a b ↔ a < x ∧ x ≤ b
h₁_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₁_finset_Ioo a b ↔ a < x ∧ x < b
hIcc : h₀_finset_Icc = h₁_finset_Icc
⊢ h₀_finset_Ico = h₁_finset_Ico
[PROOFSTEP]
ext a b x
[GOAL]
case h.h.a
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h₀_finset_Icc h₀_finset_Ico h₀_finset_Ioc h₀_finset_Ioo : α → α → Finset α
h₀_finset_mem_Icc : ∀ (a b x : α), x ∈ h₀_finset_Icc a b ↔ a ≤ x ∧ x ≤ b
h₀_finset_mem_Ico : ∀ (a b x : α), x ∈ h₀_finset_Ico a b ↔ a ≤ x ∧ x < b
h₀_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₀_finset_Ioc a b ↔ a < x ∧ x ≤ b
h₀_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₀_finset_Ioo a b ↔ a < x ∧ x < b
h₁_finset_Icc h₁_finset_Ico h₁_finset_Ioc h₁_finset_Ioo : α → α → Finset α
h₁_finset_mem_Icc : ∀ (a b x : α), x ∈ h₁_finset_Icc a b ↔ a ≤ x ∧ x ≤ b
h₁_finset_mem_Ico : ∀ (a b x : α), x ∈ h₁_finset_Ico a b ↔ a ≤ x ∧ x < b
h₁_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₁_finset_Ioc a b ↔ a < x ∧ x ≤ b
h₁_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₁_finset_Ioo a b ↔ a < x ∧ x < b
hIcc : h₀_finset_Icc = h₁_finset_Icc
a b x : α
⊢ x ∈ h₀_finset_Ico a b ↔ x ∈ h₁_finset_Ico a b
[PROOFSTEP]
rw [h₀_finset_mem_Ico, h₁_finset_mem_Ico]
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h₀_finset_Icc h₀_finset_Ico h₀_finset_Ioc h₀_finset_Ioo : α → α → Finset α
h₀_finset_mem_Icc : ∀ (a b x : α), x ∈ h₀_finset_Icc a b ↔ a ≤ x ∧ x ≤ b
h₀_finset_mem_Ico : ∀ (a b x : α), x ∈ h₀_finset_Ico a b ↔ a ≤ x ∧ x < b
h₀_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₀_finset_Ioc a b ↔ a < x ∧ x ≤ b
h₀_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₀_finset_Ioo a b ↔ a < x ∧ x < b
h₁_finset_Icc h₁_finset_Ico h₁_finset_Ioc h₁_finset_Ioo : α → α → Finset α
h₁_finset_mem_Icc : ∀ (a b x : α), x ∈ h₁_finset_Icc a b ↔ a ≤ x ∧ x ≤ b
h₁_finset_mem_Ico : ∀ (a b x : α), x ∈ h₁_finset_Ico a b ↔ a ≤ x ∧ x < b
h₁_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₁_finset_Ioc a b ↔ a < x ∧ x ≤ b
h₁_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₁_finset_Ioo a b ↔ a < x ∧ x < b
hIcc : h₀_finset_Icc = h₁_finset_Icc
hIco : h₀_finset_Ico = h₁_finset_Ico
⊢ { finsetIcc := h₀_finset_Icc, finsetIco := h₀_finset_Ico, finsetIoc := h₀_finset_Ioc, finsetIoo := h₀_finset_Ioo,
      finset_mem_Icc := h₀_finset_mem_Icc, finset_mem_Ico := h₀_finset_mem_Ico, finset_mem_Ioc := h₀_finset_mem_Ioc,
      finset_mem_Ioo := h₀_finset_mem_Ioo } =
    { finsetIcc := h₁_finset_Icc, finsetIco := h₁_finset_Ico, finsetIoc := h₁_finset_Ioc, finsetIoo := h₁_finset_Ioo,
      finset_mem_Icc := h₁_finset_mem_Icc, finset_mem_Ico := h₁_finset_mem_Ico, finset_mem_Ioc := h₁_finset_mem_Ioc,
      finset_mem_Ioo := h₁_finset_mem_Ioo }
[PROOFSTEP]
have hIoc : h₀_finset_Ioc = h₁_finset_Ioc := by
  ext a b x
  rw [h₀_finset_mem_Ioc, h₁_finset_mem_Ioc]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h₀_finset_Icc h₀_finset_Ico h₀_finset_Ioc h₀_finset_Ioo : α → α → Finset α
h₀_finset_mem_Icc : ∀ (a b x : α), x ∈ h₀_finset_Icc a b ↔ a ≤ x ∧ x ≤ b
h₀_finset_mem_Ico : ∀ (a b x : α), x ∈ h₀_finset_Ico a b ↔ a ≤ x ∧ x < b
h₀_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₀_finset_Ioc a b ↔ a < x ∧ x ≤ b
h₀_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₀_finset_Ioo a b ↔ a < x ∧ x < b
h₁_finset_Icc h₁_finset_Ico h₁_finset_Ioc h₁_finset_Ioo : α → α → Finset α
h₁_finset_mem_Icc : ∀ (a b x : α), x ∈ h₁_finset_Icc a b ↔ a ≤ x ∧ x ≤ b
h₁_finset_mem_Ico : ∀ (a b x : α), x ∈ h₁_finset_Ico a b ↔ a ≤ x ∧ x < b
h₁_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₁_finset_Ioc a b ↔ a < x ∧ x ≤ b
h₁_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₁_finset_Ioo a b ↔ a < x ∧ x < b
hIcc : h₀_finset_Icc = h₁_finset_Icc
hIco : h₀_finset_Ico = h₁_finset_Ico
⊢ h₀_finset_Ioc = h₁_finset_Ioc
[PROOFSTEP]
ext a b x
[GOAL]
case h.h.a
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h₀_finset_Icc h₀_finset_Ico h₀_finset_Ioc h₀_finset_Ioo : α → α → Finset α
h₀_finset_mem_Icc : ∀ (a b x : α), x ∈ h₀_finset_Icc a b ↔ a ≤ x ∧ x ≤ b
h₀_finset_mem_Ico : ∀ (a b x : α), x ∈ h₀_finset_Ico a b ↔ a ≤ x ∧ x < b
h₀_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₀_finset_Ioc a b ↔ a < x ∧ x ≤ b
h₀_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₀_finset_Ioo a b ↔ a < x ∧ x < b
h₁_finset_Icc h₁_finset_Ico h₁_finset_Ioc h₁_finset_Ioo : α → α → Finset α
h₁_finset_mem_Icc : ∀ (a b x : α), x ∈ h₁_finset_Icc a b ↔ a ≤ x ∧ x ≤ b
h₁_finset_mem_Ico : ∀ (a b x : α), x ∈ h₁_finset_Ico a b ↔ a ≤ x ∧ x < b
h₁_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₁_finset_Ioc a b ↔ a < x ∧ x ≤ b
h₁_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₁_finset_Ioo a b ↔ a < x ∧ x < b
hIcc : h₀_finset_Icc = h₁_finset_Icc
hIco : h₀_finset_Ico = h₁_finset_Ico
a b x : α
⊢ x ∈ h₀_finset_Ioc a b ↔ x ∈ h₁_finset_Ioc a b
[PROOFSTEP]
rw [h₀_finset_mem_Ioc, h₁_finset_mem_Ioc]
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h₀_finset_Icc h₀_finset_Ico h₀_finset_Ioc h₀_finset_Ioo : α → α → Finset α
h₀_finset_mem_Icc : ∀ (a b x : α), x ∈ h₀_finset_Icc a b ↔ a ≤ x ∧ x ≤ b
h₀_finset_mem_Ico : ∀ (a b x : α), x ∈ h₀_finset_Ico a b ↔ a ≤ x ∧ x < b
h₀_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₀_finset_Ioc a b ↔ a < x ∧ x ≤ b
h₀_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₀_finset_Ioo a b ↔ a < x ∧ x < b
h₁_finset_Icc h₁_finset_Ico h₁_finset_Ioc h₁_finset_Ioo : α → α → Finset α
h₁_finset_mem_Icc : ∀ (a b x : α), x ∈ h₁_finset_Icc a b ↔ a ≤ x ∧ x ≤ b
h₁_finset_mem_Ico : ∀ (a b x : α), x ∈ h₁_finset_Ico a b ↔ a ≤ x ∧ x < b
h₁_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₁_finset_Ioc a b ↔ a < x ∧ x ≤ b
h₁_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₁_finset_Ioo a b ↔ a < x ∧ x < b
hIcc : h₀_finset_Icc = h₁_finset_Icc
hIco : h₀_finset_Ico = h₁_finset_Ico
hIoc : h₀_finset_Ioc = h₁_finset_Ioc
⊢ { finsetIcc := h₀_finset_Icc, finsetIco := h₀_finset_Ico, finsetIoc := h₀_finset_Ioc, finsetIoo := h₀_finset_Ioo,
      finset_mem_Icc := h₀_finset_mem_Icc, finset_mem_Ico := h₀_finset_mem_Ico, finset_mem_Ioc := h₀_finset_mem_Ioc,
      finset_mem_Ioo := h₀_finset_mem_Ioo } =
    { finsetIcc := h₁_finset_Icc, finsetIco := h₁_finset_Ico, finsetIoc := h₁_finset_Ioc, finsetIoo := h₁_finset_Ioo,
      finset_mem_Icc := h₁_finset_mem_Icc, finset_mem_Ico := h₁_finset_mem_Ico, finset_mem_Ioc := h₁_finset_mem_Ioc,
      finset_mem_Ioo := h₁_finset_mem_Ioo }
[PROOFSTEP]
have hIoo : h₀_finset_Ioo = h₁_finset_Ioo := by
  ext a b x
  rw [h₀_finset_mem_Ioo, h₁_finset_mem_Ioo]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h₀_finset_Icc h₀_finset_Ico h₀_finset_Ioc h₀_finset_Ioo : α → α → Finset α
h₀_finset_mem_Icc : ∀ (a b x : α), x ∈ h₀_finset_Icc a b ↔ a ≤ x ∧ x ≤ b
h₀_finset_mem_Ico : ∀ (a b x : α), x ∈ h₀_finset_Ico a b ↔ a ≤ x ∧ x < b
h₀_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₀_finset_Ioc a b ↔ a < x ∧ x ≤ b
h₀_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₀_finset_Ioo a b ↔ a < x ∧ x < b
h₁_finset_Icc h₁_finset_Ico h₁_finset_Ioc h₁_finset_Ioo : α → α → Finset α
h₁_finset_mem_Icc : ∀ (a b x : α), x ∈ h₁_finset_Icc a b ↔ a ≤ x ∧ x ≤ b
h₁_finset_mem_Ico : ∀ (a b x : α), x ∈ h₁_finset_Ico a b ↔ a ≤ x ∧ x < b
h₁_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₁_finset_Ioc a b ↔ a < x ∧ x ≤ b
h₁_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₁_finset_Ioo a b ↔ a < x ∧ x < b
hIcc : h₀_finset_Icc = h₁_finset_Icc
hIco : h₀_finset_Ico = h₁_finset_Ico
hIoc : h₀_finset_Ioc = h₁_finset_Ioc
⊢ h₀_finset_Ioo = h₁_finset_Ioo
[PROOFSTEP]
ext a b x
[GOAL]
case h.h.a
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h₀_finset_Icc h₀_finset_Ico h₀_finset_Ioc h₀_finset_Ioo : α → α → Finset α
h₀_finset_mem_Icc : ∀ (a b x : α), x ∈ h₀_finset_Icc a b ↔ a ≤ x ∧ x ≤ b
h₀_finset_mem_Ico : ∀ (a b x : α), x ∈ h₀_finset_Ico a b ↔ a ≤ x ∧ x < b
h₀_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₀_finset_Ioc a b ↔ a < x ∧ x ≤ b
h₀_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₀_finset_Ioo a b ↔ a < x ∧ x < b
h₁_finset_Icc h₁_finset_Ico h₁_finset_Ioc h₁_finset_Ioo : α → α → Finset α
h₁_finset_mem_Icc : ∀ (a b x : α), x ∈ h₁_finset_Icc a b ↔ a ≤ x ∧ x ≤ b
h₁_finset_mem_Ico : ∀ (a b x : α), x ∈ h₁_finset_Ico a b ↔ a ≤ x ∧ x < b
h₁_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₁_finset_Ioc a b ↔ a < x ∧ x ≤ b
h₁_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₁_finset_Ioo a b ↔ a < x ∧ x < b
hIcc : h₀_finset_Icc = h₁_finset_Icc
hIco : h₀_finset_Ico = h₁_finset_Ico
hIoc : h₀_finset_Ioc = h₁_finset_Ioc
a b x : α
⊢ x ∈ h₀_finset_Ioo a b ↔ x ∈ h₁_finset_Ioo a b
[PROOFSTEP]
rw [h₀_finset_mem_Ioo, h₁_finset_mem_Ioo]
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h₀_finset_Icc h₀_finset_Ico h₀_finset_Ioc h₀_finset_Ioo : α → α → Finset α
h₀_finset_mem_Icc : ∀ (a b x : α), x ∈ h₀_finset_Icc a b ↔ a ≤ x ∧ x ≤ b
h₀_finset_mem_Ico : ∀ (a b x : α), x ∈ h₀_finset_Ico a b ↔ a ≤ x ∧ x < b
h₀_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₀_finset_Ioc a b ↔ a < x ∧ x ≤ b
h₀_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₀_finset_Ioo a b ↔ a < x ∧ x < b
h₁_finset_Icc h₁_finset_Ico h₁_finset_Ioc h₁_finset_Ioo : α → α → Finset α
h₁_finset_mem_Icc : ∀ (a b x : α), x ∈ h₁_finset_Icc a b ↔ a ≤ x ∧ x ≤ b
h₁_finset_mem_Ico : ∀ (a b x : α), x ∈ h₁_finset_Ico a b ↔ a ≤ x ∧ x < b
h₁_finset_mem_Ioc : ∀ (a b x : α), x ∈ h₁_finset_Ioc a b ↔ a < x ∧ x ≤ b
h₁_finset_mem_Ioo : ∀ (a b x : α), x ∈ h₁_finset_Ioo a b ↔ a < x ∧ x < b
hIcc : h₀_finset_Icc = h₁_finset_Icc
hIco : h₀_finset_Ico = h₁_finset_Ico
hIoc : h₀_finset_Ioc = h₁_finset_Ioc
hIoo : h₀_finset_Ioo = h₁_finset_Ioo
⊢ { finsetIcc := h₀_finset_Icc, finsetIco := h₀_finset_Ico, finsetIoc := h₀_finset_Ioc, finsetIoo := h₀_finset_Ioo,
      finset_mem_Icc := h₀_finset_mem_Icc, finset_mem_Ico := h₀_finset_mem_Ico, finset_mem_Ioc := h₀_finset_mem_Ioc,
      finset_mem_Ioo := h₀_finset_mem_Ioo } =
    { finsetIcc := h₁_finset_Icc, finsetIco := h₁_finset_Ico, finsetIoc := h₁_finset_Ioc, finsetIoo := h₁_finset_Ioo,
      finset_mem_Icc := h₁_finset_mem_Icc, finset_mem_Ico := h₁_finset_mem_Ico, finset_mem_Ioc := h₁_finset_mem_Ioc,
      finset_mem_Ioo := h₁_finset_mem_Ioo }
[PROOFSTEP]
simp_rw [hIcc, hIco, hIoc, hIoo]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h₀ h₁ : LocallyFiniteOrderTop α
⊢ h₀ = h₁
[PROOFSTEP]
cases' h₀ with h₀_finset_Ioi h₀_finset_Ici h₀_finset_mem_Ici h₀_finset_mem_Ioi
[GOAL]
case mk
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h₁ : LocallyFiniteOrderTop α
h₀_finset_Ioi h₀_finset_Ici : α → Finset α
h₀_finset_mem_Ici : ∀ (a x : α), x ∈ h₀_finset_Ici a ↔ a ≤ x
h₀_finset_mem_Ioi : ∀ (a x : α), x ∈ h₀_finset_Ioi a ↔ a < x
⊢ { finsetIoi := h₀_finset_Ioi, finsetIci := h₀_finset_Ici, finset_mem_Ici := h₀_finset_mem_Ici,
      finset_mem_Ioi := h₀_finset_mem_Ioi } =
    h₁
[PROOFSTEP]
cases' h₁ with h₁_finset_Ioi h₁_finset_Ici h₁_finset_mem_Ici h₁_finset_mem_Ioi
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h₀_finset_Ioi h₀_finset_Ici : α → Finset α
h₀_finset_mem_Ici : ∀ (a x : α), x ∈ h₀_finset_Ici a ↔ a ≤ x
h₀_finset_mem_Ioi : ∀ (a x : α), x ∈ h₀_finset_Ioi a ↔ a < x
h₁_finset_Ioi h₁_finset_Ici : α → Finset α
h₁_finset_mem_Ici : ∀ (a x : α), x ∈ h₁_finset_Ici a ↔ a ≤ x
h₁_finset_mem_Ioi : ∀ (a x : α), x ∈ h₁_finset_Ioi a ↔ a < x
⊢ { finsetIoi := h₀_finset_Ioi, finsetIci := h₀_finset_Ici, finset_mem_Ici := h₀_finset_mem_Ici,
      finset_mem_Ioi := h₀_finset_mem_Ioi } =
    { finsetIoi := h₁_finset_Ioi, finsetIci := h₁_finset_Ici, finset_mem_Ici := h₁_finset_mem_Ici,
      finset_mem_Ioi := h₁_finset_mem_Ioi }
[PROOFSTEP]
have hIci : h₀_finset_Ici = h₁_finset_Ici := by
  ext a b
  rw [h₀_finset_mem_Ici, h₁_finset_mem_Ici]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h₀_finset_Ioi h₀_finset_Ici : α → Finset α
h₀_finset_mem_Ici : ∀ (a x : α), x ∈ h₀_finset_Ici a ↔ a ≤ x
h₀_finset_mem_Ioi : ∀ (a x : α), x ∈ h₀_finset_Ioi a ↔ a < x
h₁_finset_Ioi h₁_finset_Ici : α → Finset α
h₁_finset_mem_Ici : ∀ (a x : α), x ∈ h₁_finset_Ici a ↔ a ≤ x
h₁_finset_mem_Ioi : ∀ (a x : α), x ∈ h₁_finset_Ioi a ↔ a < x
⊢ h₀_finset_Ici = h₁_finset_Ici
[PROOFSTEP]
ext a b
[GOAL]
case h.a
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h₀_finset_Ioi h₀_finset_Ici : α → Finset α
h₀_finset_mem_Ici : ∀ (a x : α), x ∈ h₀_finset_Ici a ↔ a ≤ x
h₀_finset_mem_Ioi : ∀ (a x : α), x ∈ h₀_finset_Ioi a ↔ a < x
h₁_finset_Ioi h₁_finset_Ici : α → Finset α
h₁_finset_mem_Ici : ∀ (a x : α), x ∈ h₁_finset_Ici a ↔ a ≤ x
h₁_finset_mem_Ioi : ∀ (a x : α), x ∈ h₁_finset_Ioi a ↔ a < x
a b : α
⊢ b ∈ h₀_finset_Ici a ↔ b ∈ h₁_finset_Ici a
[PROOFSTEP]
rw [h₀_finset_mem_Ici, h₁_finset_mem_Ici]
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h₀_finset_Ioi h₀_finset_Ici : α → Finset α
h₀_finset_mem_Ici : ∀ (a x : α), x ∈ h₀_finset_Ici a ↔ a ≤ x
h₀_finset_mem_Ioi : ∀ (a x : α), x ∈ h₀_finset_Ioi a ↔ a < x
h₁_finset_Ioi h₁_finset_Ici : α → Finset α
h₁_finset_mem_Ici : ∀ (a x : α), x ∈ h₁_finset_Ici a ↔ a ≤ x
h₁_finset_mem_Ioi : ∀ (a x : α), x ∈ h₁_finset_Ioi a ↔ a < x
hIci : h₀_finset_Ici = h₁_finset_Ici
⊢ { finsetIoi := h₀_finset_Ioi, finsetIci := h₀_finset_Ici, finset_mem_Ici := h₀_finset_mem_Ici,
      finset_mem_Ioi := h₀_finset_mem_Ioi } =
    { finsetIoi := h₁_finset_Ioi, finsetIci := h₁_finset_Ici, finset_mem_Ici := h₁_finset_mem_Ici,
      finset_mem_Ioi := h₁_finset_mem_Ioi }
[PROOFSTEP]
have hIoi : h₀_finset_Ioi = h₁_finset_Ioi := by
  ext a b
  rw [h₀_finset_mem_Ioi, h₁_finset_mem_Ioi]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h₀_finset_Ioi h₀_finset_Ici : α → Finset α
h₀_finset_mem_Ici : ∀ (a x : α), x ∈ h₀_finset_Ici a ↔ a ≤ x
h₀_finset_mem_Ioi : ∀ (a x : α), x ∈ h₀_finset_Ioi a ↔ a < x
h₁_finset_Ioi h₁_finset_Ici : α → Finset α
h₁_finset_mem_Ici : ∀ (a x : α), x ∈ h₁_finset_Ici a ↔ a ≤ x
h₁_finset_mem_Ioi : ∀ (a x : α), x ∈ h₁_finset_Ioi a ↔ a < x
hIci : h₀_finset_Ici = h₁_finset_Ici
⊢ h₀_finset_Ioi = h₁_finset_Ioi
[PROOFSTEP]
ext a b
[GOAL]
case h.a
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h₀_finset_Ioi h₀_finset_Ici : α → Finset α
h₀_finset_mem_Ici : ∀ (a x : α), x ∈ h₀_finset_Ici a ↔ a ≤ x
h₀_finset_mem_Ioi : ∀ (a x : α), x ∈ h₀_finset_Ioi a ↔ a < x
h₁_finset_Ioi h₁_finset_Ici : α → Finset α
h₁_finset_mem_Ici : ∀ (a x : α), x ∈ h₁_finset_Ici a ↔ a ≤ x
h₁_finset_mem_Ioi : ∀ (a x : α), x ∈ h₁_finset_Ioi a ↔ a < x
hIci : h₀_finset_Ici = h₁_finset_Ici
a b : α
⊢ b ∈ h₀_finset_Ioi a ↔ b ∈ h₁_finset_Ioi a
[PROOFSTEP]
rw [h₀_finset_mem_Ioi, h₁_finset_mem_Ioi]
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h₀_finset_Ioi h₀_finset_Ici : α → Finset α
h₀_finset_mem_Ici : ∀ (a x : α), x ∈ h₀_finset_Ici a ↔ a ≤ x
h₀_finset_mem_Ioi : ∀ (a x : α), x ∈ h₀_finset_Ioi a ↔ a < x
h₁_finset_Ioi h₁_finset_Ici : α → Finset α
h₁_finset_mem_Ici : ∀ (a x : α), x ∈ h₁_finset_Ici a ↔ a ≤ x
h₁_finset_mem_Ioi : ∀ (a x : α), x ∈ h₁_finset_Ioi a ↔ a < x
hIci : h₀_finset_Ici = h₁_finset_Ici
hIoi : h₀_finset_Ioi = h₁_finset_Ioi
⊢ { finsetIoi := h₀_finset_Ioi, finsetIci := h₀_finset_Ici, finset_mem_Ici := h₀_finset_mem_Ici,
      finset_mem_Ioi := h₀_finset_mem_Ioi } =
    { finsetIoi := h₁_finset_Ioi, finsetIci := h₁_finset_Ici, finset_mem_Ici := h₁_finset_mem_Ici,
      finset_mem_Ioi := h₁_finset_mem_Ioi }
[PROOFSTEP]
simp_rw [hIci, hIoi]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h₀ h₁ : LocallyFiniteOrderBot α
⊢ h₀ = h₁
[PROOFSTEP]
cases' h₀ with h₀_finset_Iio h₀_finset_Iic h₀_finset_mem_Iic h₀_finset_mem_Iio
[GOAL]
case mk
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h₁ : LocallyFiniteOrderBot α
h₀_finset_Iio h₀_finset_Iic : α → Finset α
h₀_finset_mem_Iic : ∀ (a x : α), x ∈ h₀_finset_Iic a ↔ x ≤ a
h₀_finset_mem_Iio : ∀ (a x : α), x ∈ h₀_finset_Iio a ↔ x < a
⊢ { finsetIio := h₀_finset_Iio, finsetIic := h₀_finset_Iic, finset_mem_Iic := h₀_finset_mem_Iic,
      finset_mem_Iio := h₀_finset_mem_Iio } =
    h₁
[PROOFSTEP]
cases' h₁ with h₁_finset_Iio h₁_finset_Iic h₁_finset_mem_Iic h₁_finset_mem_Iio
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h₀_finset_Iio h₀_finset_Iic : α → Finset α
h₀_finset_mem_Iic : ∀ (a x : α), x ∈ h₀_finset_Iic a ↔ x ≤ a
h₀_finset_mem_Iio : ∀ (a x : α), x ∈ h₀_finset_Iio a ↔ x < a
h₁_finset_Iio h₁_finset_Iic : α → Finset α
h₁_finset_mem_Iic : ∀ (a x : α), x ∈ h₁_finset_Iic a ↔ x ≤ a
h₁_finset_mem_Iio : ∀ (a x : α), x ∈ h₁_finset_Iio a ↔ x < a
⊢ { finsetIio := h₀_finset_Iio, finsetIic := h₀_finset_Iic, finset_mem_Iic := h₀_finset_mem_Iic,
      finset_mem_Iio := h₀_finset_mem_Iio } =
    { finsetIio := h₁_finset_Iio, finsetIic := h₁_finset_Iic, finset_mem_Iic := h₁_finset_mem_Iic,
      finset_mem_Iio := h₁_finset_mem_Iio }
[PROOFSTEP]
have hIic : h₀_finset_Iic = h₁_finset_Iic := by
  ext a b
  rw [h₀_finset_mem_Iic, h₁_finset_mem_Iic]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h₀_finset_Iio h₀_finset_Iic : α → Finset α
h₀_finset_mem_Iic : ∀ (a x : α), x ∈ h₀_finset_Iic a ↔ x ≤ a
h₀_finset_mem_Iio : ∀ (a x : α), x ∈ h₀_finset_Iio a ↔ x < a
h₁_finset_Iio h₁_finset_Iic : α → Finset α
h₁_finset_mem_Iic : ∀ (a x : α), x ∈ h₁_finset_Iic a ↔ x ≤ a
h₁_finset_mem_Iio : ∀ (a x : α), x ∈ h₁_finset_Iio a ↔ x < a
⊢ h₀_finset_Iic = h₁_finset_Iic
[PROOFSTEP]
ext a b
[GOAL]
case h.a
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h₀_finset_Iio h₀_finset_Iic : α → Finset α
h₀_finset_mem_Iic : ∀ (a x : α), x ∈ h₀_finset_Iic a ↔ x ≤ a
h₀_finset_mem_Iio : ∀ (a x : α), x ∈ h₀_finset_Iio a ↔ x < a
h₁_finset_Iio h₁_finset_Iic : α → Finset α
h₁_finset_mem_Iic : ∀ (a x : α), x ∈ h₁_finset_Iic a ↔ x ≤ a
h₁_finset_mem_Iio : ∀ (a x : α), x ∈ h₁_finset_Iio a ↔ x < a
a b : α
⊢ b ∈ h₀_finset_Iic a ↔ b ∈ h₁_finset_Iic a
[PROOFSTEP]
rw [h₀_finset_mem_Iic, h₁_finset_mem_Iic]
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h₀_finset_Iio h₀_finset_Iic : α → Finset α
h₀_finset_mem_Iic : ∀ (a x : α), x ∈ h₀_finset_Iic a ↔ x ≤ a
h₀_finset_mem_Iio : ∀ (a x : α), x ∈ h₀_finset_Iio a ↔ x < a
h₁_finset_Iio h₁_finset_Iic : α → Finset α
h₁_finset_mem_Iic : ∀ (a x : α), x ∈ h₁_finset_Iic a ↔ x ≤ a
h₁_finset_mem_Iio : ∀ (a x : α), x ∈ h₁_finset_Iio a ↔ x < a
hIic : h₀_finset_Iic = h₁_finset_Iic
⊢ { finsetIio := h₀_finset_Iio, finsetIic := h₀_finset_Iic, finset_mem_Iic := h₀_finset_mem_Iic,
      finset_mem_Iio := h₀_finset_mem_Iio } =
    { finsetIio := h₁_finset_Iio, finsetIic := h₁_finset_Iic, finset_mem_Iic := h₁_finset_mem_Iic,
      finset_mem_Iio := h₁_finset_mem_Iio }
[PROOFSTEP]
have hIio : h₀_finset_Iio = h₁_finset_Iio := by
  ext a b
  rw [h₀_finset_mem_Iio, h₁_finset_mem_Iio]
[GOAL]
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h₀_finset_Iio h₀_finset_Iic : α → Finset α
h₀_finset_mem_Iic : ∀ (a x : α), x ∈ h₀_finset_Iic a ↔ x ≤ a
h₀_finset_mem_Iio : ∀ (a x : α), x ∈ h₀_finset_Iio a ↔ x < a
h₁_finset_Iio h₁_finset_Iic : α → Finset α
h₁_finset_mem_Iic : ∀ (a x : α), x ∈ h₁_finset_Iic a ↔ x ≤ a
h₁_finset_mem_Iio : ∀ (a x : α), x ∈ h₁_finset_Iio a ↔ x < a
hIic : h₀_finset_Iic = h₁_finset_Iic
⊢ h₀_finset_Iio = h₁_finset_Iio
[PROOFSTEP]
ext a b
[GOAL]
case h.a
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h₀_finset_Iio h₀_finset_Iic : α → Finset α
h₀_finset_mem_Iic : ∀ (a x : α), x ∈ h₀_finset_Iic a ↔ x ≤ a
h₀_finset_mem_Iio : ∀ (a x : α), x ∈ h₀_finset_Iio a ↔ x < a
h₁_finset_Iio h₁_finset_Iic : α → Finset α
h₁_finset_mem_Iic : ∀ (a x : α), x ∈ h₁_finset_Iic a ↔ x ≤ a
h₁_finset_mem_Iio : ∀ (a x : α), x ∈ h₁_finset_Iio a ↔ x < a
hIic : h₀_finset_Iic = h₁_finset_Iic
a b : α
⊢ b ∈ h₀_finset_Iio a ↔ b ∈ h₁_finset_Iio a
[PROOFSTEP]
rw [h₀_finset_mem_Iio, h₁_finset_mem_Iio]
[GOAL]
case mk.mk
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
h₀_finset_Iio h₀_finset_Iic : α → Finset α
h₀_finset_mem_Iic : ∀ (a x : α), x ∈ h₀_finset_Iic a ↔ x ≤ a
h₀_finset_mem_Iio : ∀ (a x : α), x ∈ h₀_finset_Iio a ↔ x < a
h₁_finset_Iio h₁_finset_Iic : α → Finset α
h₁_finset_mem_Iic : ∀ (a x : α), x ∈ h₁_finset_Iic a ↔ x ≤ a
h₁_finset_mem_Iio : ∀ (a x : α), x ∈ h₁_finset_Iio a ↔ x < a
hIic : h₀_finset_Iic = h₁_finset_Iic
hIio : h₀_finset_Iio = h₁_finset_Iio
⊢ { finsetIio := h₀_finset_Iio, finsetIic := h₀_finset_Iic, finset_mem_Iic := h₀_finset_mem_Iic,
      finset_mem_Iio := h₀_finset_mem_Iio } =
    { finsetIio := h₁_finset_Iio, finsetIic := h₁_finset_Iic, finset_mem_Iic := h₁_finset_mem_Iic,
      finset_mem_Iio := h₁_finset_mem_Iio }
[PROOFSTEP]
simp_rw [hIic, hIio]
  -- Should this be called `LocallyFiniteOrder.lift`?
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder β
f : α ↪o β
a b x : α
⊢ x ∈ (fun a b => preimage (Icc (↑f a) (↑f b)) ↑f (_ : Set.InjOn (↑f.toEmbedding) (↑f ⁻¹' ↑(Icc (↑f a) (↑f b))))) a b ↔
    a ≤ x ∧ x ≤ b
[PROOFSTEP]
rw [mem_preimage, mem_Icc, f.le_iff_le, f.le_iff_le]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder β
f : α ↪o β
a b x : α
⊢ x ∈ (fun a b => preimage (Ico (↑f a) (↑f b)) ↑f (_ : Set.InjOn (↑f.toEmbedding) (↑f ⁻¹' ↑(Ico (↑f a) (↑f b))))) a b ↔
    a ≤ x ∧ x < b
[PROOFSTEP]
rw [mem_preimage, mem_Ico, f.le_iff_le, f.lt_iff_lt]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder β
f : α ↪o β
a b x : α
⊢ x ∈ (fun a b => preimage (Ioc (↑f a) (↑f b)) ↑f (_ : Set.InjOn (↑f.toEmbedding) (↑f ⁻¹' ↑(Ioc (↑f a) (↑f b))))) a b ↔
    a < x ∧ x ≤ b
[PROOFSTEP]
rw [mem_preimage, mem_Ioc, f.lt_iff_lt, f.le_iff_le]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder β
f : α ↪o β
a b x : α
⊢ x ∈ (fun a b => preimage (Ioo (↑f a) (↑f b)) ↑f (_ : Set.InjOn (↑f.toEmbedding) (↑f ⁻¹' ↑(Ioo (↑f a) (↑f b))))) a b ↔
    a < x ∧ x < b
[PROOFSTEP]
rw [mem_preimage, mem_Ioo, f.lt_iff_lt, f.lt_iff_lt]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder α
a b : α
⊢ Icc (↑toDual a) (↑toDual b) = map (Equiv.toEmbedding toDual) (Icc b a)
[PROOFSTEP]
refine' Eq.trans _ map_refl.symm
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder α
a b : α
⊢ Icc (↑toDual a) (↑toDual b) = Icc b a
[PROOFSTEP]
ext c
[GOAL]
case a
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder α
a b : α
c : (fun x => αᵒᵈ) a
⊢ c ∈ Icc (↑toDual a) (↑toDual b) ↔ c ∈ Icc b a
[PROOFSTEP]
rw [mem_Icc, mem_Icc (α := α)]
[GOAL]
case a
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder α
a b : α
c : (fun x => αᵒᵈ) a
⊢ ↑toDual a ≤ c ∧ c ≤ ↑toDual b ↔ b ≤ c ∧ c ≤ a
[PROOFSTEP]
exact and_comm
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder α
a b : α
⊢ Ico (↑toDual a) (↑toDual b) = map (Equiv.toEmbedding toDual) (Ioc b a)
[PROOFSTEP]
refine' Eq.trans _ map_refl.symm
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder α
a b : α
⊢ Ico (↑toDual a) (↑toDual b) = Ioc b a
[PROOFSTEP]
ext c
[GOAL]
case a
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder α
a b : α
c : (fun x => αᵒᵈ) a
⊢ c ∈ Ico (↑toDual a) (↑toDual b) ↔ c ∈ Ioc b a
[PROOFSTEP]
rw [mem_Ico, mem_Ioc (α := α)]
[GOAL]
case a
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder α
a b : α
c : (fun x => αᵒᵈ) a
⊢ ↑toDual a ≤ c ∧ c < ↑toDual b ↔ b < c ∧ c ≤ a
[PROOFSTEP]
exact and_comm
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder α
a b : α
⊢ Ioc (↑toDual a) (↑toDual b) = map (Equiv.toEmbedding toDual) (Ico b a)
[PROOFSTEP]
refine' Eq.trans _ map_refl.symm
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder α
a b : α
⊢ Ioc (↑toDual a) (↑toDual b) = Ico b a
[PROOFSTEP]
ext c
[GOAL]
case a
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder α
a b : α
c : (fun x => αᵒᵈ) a
⊢ c ∈ Ioc (↑toDual a) (↑toDual b) ↔ c ∈ Ico b a
[PROOFSTEP]
rw [mem_Ioc, mem_Ico (α := α)]
[GOAL]
case a
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder α
a b : α
c : (fun x => αᵒᵈ) a
⊢ ↑toDual a < c ∧ c ≤ ↑toDual b ↔ b ≤ c ∧ c < a
[PROOFSTEP]
exact and_comm
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder α
a b : α
⊢ Ioo (↑toDual a) (↑toDual b) = map (Equiv.toEmbedding toDual) (Ioo b a)
[PROOFSTEP]
refine' Eq.trans _ map_refl.symm
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder α
a b : α
⊢ Ioo (↑toDual a) (↑toDual b) = Ioo b a
[PROOFSTEP]
ext c
[GOAL]
case a
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder α
a b : α
c : (fun x => αᵒᵈ) a
⊢ c ∈ Ioo (↑toDual a) (↑toDual b) ↔ c ∈ Ioo b a
[PROOFSTEP]
rw [mem_Ioo, mem_Ioo (α := α)]
[GOAL]
case a
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder α
a b : α
c : (fun x => αᵒᵈ) a
⊢ ↑toDual a < c ∧ c < ↑toDual b ↔ b < c ∧ c < a
[PROOFSTEP]
exact and_comm
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder α
a✝ b✝ : α
a b : αᵒᵈ
⊢ Icc (↑ofDual a) (↑ofDual b) = map (Equiv.toEmbedding ofDual) (Icc b a)
[PROOFSTEP]
refine' Eq.trans _ map_refl.symm
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder α
a✝ b✝ : α
a b : αᵒᵈ
⊢ Icc (↑ofDual a) (↑ofDual b) = Icc b a
[PROOFSTEP]
ext c
[GOAL]
case a
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder α
a✝ b✝ : α
a b : αᵒᵈ
c : (fun x => α) a
⊢ c ∈ Icc (↑ofDual a) (↑ofDual b) ↔ c ∈ Icc b a
[PROOFSTEP]
rw [mem_Icc, mem_Icc (α := αᵒᵈ)]
[GOAL]
case a
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder α
a✝ b✝ : α
a b : αᵒᵈ
c : (fun x => α) a
⊢ ↑ofDual a ≤ c ∧ c ≤ ↑ofDual b ↔ b ≤ c ∧ c ≤ a
[PROOFSTEP]
exact and_comm
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder α
a✝ b✝ : α
a b : αᵒᵈ
⊢ Ico (↑ofDual a) (↑ofDual b) = map (Equiv.toEmbedding ofDual) (Ioc b a)
[PROOFSTEP]
refine' Eq.trans _ map_refl.symm
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder α
a✝ b✝ : α
a b : αᵒᵈ
⊢ Ico (↑ofDual a) (↑ofDual b) = Ioc b a
[PROOFSTEP]
ext c
[GOAL]
case a
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder α
a✝ b✝ : α
a b : αᵒᵈ
c : (fun x => α) a
⊢ c ∈ Ico (↑ofDual a) (↑ofDual b) ↔ c ∈ Ioc b a
[PROOFSTEP]
rw [mem_Ico, mem_Ioc (α := αᵒᵈ)]
[GOAL]
case a
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder α
a✝ b✝ : α
a b : αᵒᵈ
c : (fun x => α) a
⊢ ↑ofDual a ≤ c ∧ c < ↑ofDual b ↔ b < c ∧ c ≤ a
[PROOFSTEP]
exact and_comm
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder α
a✝ b✝ : α
a b : αᵒᵈ
⊢ Ioc (↑ofDual a) (↑ofDual b) = map (Equiv.toEmbedding ofDual) (Ico b a)
[PROOFSTEP]
refine' Eq.trans _ map_refl.symm
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder α
a✝ b✝ : α
a b : αᵒᵈ
⊢ Ioc (↑ofDual a) (↑ofDual b) = Ico b a
[PROOFSTEP]
ext c
[GOAL]
case a
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder α
a✝ b✝ : α
a b : αᵒᵈ
c : (fun x => α) a
⊢ c ∈ Ioc (↑ofDual a) (↑ofDual b) ↔ c ∈ Ico b a
[PROOFSTEP]
rw [mem_Ioc, mem_Ico (α := αᵒᵈ)]
[GOAL]
case a
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder α
a✝ b✝ : α
a b : αᵒᵈ
c : (fun x => α) a
⊢ ↑ofDual a < c ∧ c ≤ ↑ofDual b ↔ b ≤ c ∧ c < a
[PROOFSTEP]
exact and_comm
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder α
a✝ b✝ : α
a b : αᵒᵈ
⊢ Ioo (↑ofDual a) (↑ofDual b) = map (Equiv.toEmbedding ofDual) (Ioo b a)
[PROOFSTEP]
refine' Eq.trans _ map_refl.symm
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder α
a✝ b✝ : α
a b : αᵒᵈ
⊢ Ioo (↑ofDual a) (↑ofDual b) = Ioo b a
[PROOFSTEP]
ext c
[GOAL]
case a
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder α
a✝ b✝ : α
a b : αᵒᵈ
c : (fun x => α) a
⊢ c ∈ Ioo (↑ofDual a) (↑ofDual b) ↔ c ∈ Ioo b a
[PROOFSTEP]
rw [mem_Ioo, mem_Ioo (α := αᵒᵈ)]
[GOAL]
case a
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder α
a✝ b✝ : α
a b : αᵒᵈ
c : (fun x => α) a
⊢ ↑ofDual a < c ∧ c < ↑ofDual b ↔ b < c ∧ c < a
[PROOFSTEP]
exact and_comm
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : Preorder β
inst✝² : LocallyFiniteOrder α
inst✝¹ : LocallyFiniteOrder β
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
a b x : α × β
⊢ x ∈ (fun a b => Icc a.fst b.fst ×ˢ Icc a.snd b.snd) a b ↔ a ≤ x ∧ x ≤ b
[PROOFSTEP]
rw [mem_product, mem_Icc, mem_Icc, and_and_and_comm]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : Preorder β
inst✝² : LocallyFiniteOrder α
inst✝¹ : LocallyFiniteOrder β
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
a b x : α × β
⊢ (a.fst ≤ x.fst ∧ a.snd ≤ x.snd) ∧ x.fst ≤ b.fst ∧ x.snd ≤ b.snd ↔ a ≤ x ∧ x ≤ b
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : Preorder β
inst✝² : LocallyFiniteOrderTop α
inst✝¹ : LocallyFiniteOrderTop β
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
a x : α × β
⊢ x ∈ (fun a => Ici a.fst ×ˢ Ici a.snd) a ↔ a ≤ x
[PROOFSTEP]
rw [mem_product, mem_Ici, mem_Ici]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : Preorder β
inst✝² : LocallyFiniteOrderTop α
inst✝¹ : LocallyFiniteOrderTop β
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
a x : α × β
⊢ a.fst ≤ x.fst ∧ a.snd ≤ x.snd ↔ a ≤ x
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : Preorder β
inst✝² : LocallyFiniteOrderBot α
inst✝¹ : LocallyFiniteOrderBot β
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
a x : α × β
⊢ x ∈ (fun a => Iic a.fst ×ˢ Iic a.snd) a ↔ x ≤ a
[PROOFSTEP]
rw [mem_product, mem_Iic, mem_Iic]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
inst✝³ : Preorder β
inst✝² : LocallyFiniteOrderBot α
inst✝¹ : LocallyFiniteOrderBot β
inst✝ : DecidableRel fun x x_1 => x ≤ x_1
a x : α × β
⊢ x.fst ≤ a.fst ∧ x.snd ≤ a.snd ↔ x ≤ a
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
x : α
p : α → Prop
⊢ (∃ a, p a ∧ Option.some a = Option.some x) ↔ p x
[PROOFSTEP]
constructor
[GOAL]
case mp
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
x : α
p : α → Prop
⊢ (∃ a, p a ∧ Option.some a = Option.some x) → p x
[PROOFSTEP]
rintro ⟨x', hx, hx'⟩
[GOAL]
case mp.intro.intro
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
x : α
p : α → Prop
x' : α
hx : p x'
hx' : Option.some x' = Option.some x
⊢ p x
[PROOFSTEP]
obtain rfl := Option.some_inj.mp hx'
[GOAL]
case mp.intro.intro
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
p : α → Prop
x' : α
hx : p x'
hx' : Option.some x' = Option.some x'
⊢ p x'
[PROOFSTEP]
exact hx
[GOAL]
case mpr
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
x : α
p : α → Prop
⊢ p x → ∃ a, p a ∧ Option.some a = Option.some x
[PROOFSTEP]
exact fun h => ⟨x, h, rfl⟩
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝ b x : WithTop α
a : α
⊢ ⊤ ∈
      (fun a b =>
          match a, b with
          | none, none => {⊤}
          | none, Option.some b => ∅
          | Option.some a, none => ↑insertNone (Ici a)
          | Option.some a, Option.some b => Finset.map Embedding.some (Icc a b))
        ↑a ⊤ ↔
    ↑a ≤ ⊤ ∧ ⊤ ≤ ⊤
[PROOFSTEP]
simp [WithTop.some, WithTop.top, insertNone]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝ b x✝ : WithTop α
a x : α
⊢ ↑x ∈
      (fun a b =>
          match a, b with
          | none, none => {⊤}
          | none, Option.some b => ∅
          | Option.some a, none => ↑insertNone (Ici a)
          | Option.some a, Option.some b => Finset.map Embedding.some (Icc a b))
        ↑a ⊤ ↔
    ↑a ≤ ↑x ∧ ↑x ≤ ⊤
[PROOFSTEP]
simp only [some, le_eq_subset, some_le_some, le_top, and_true]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝ b x✝ : WithTop α
a x : α
⊢ Option.some x ∈ ↑insertNone (Ici a) ↔ a ≤ x
[PROOFSTEP]
rw [some_mem_insertNone]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝ b x✝ : WithTop α
a x : α
⊢ x ∈ Ici a ↔ a ≤ x
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝ b✝ x : WithTop α
a b : α
⊢ ⊤ ∈
      (fun a b =>
          match a, b with
          | none, none => {⊤}
          | none, Option.some b => ∅
          | Option.some a, none => ↑insertNone (Ici a)
          | Option.some a, Option.some b => Finset.map Embedding.some (Icc a b))
        ↑a ↑b ↔
    ↑a ≤ ⊤ ∧ ⊤ ≤ ↑b
[PROOFSTEP]
simp only [some, le_eq_subset, mem_map, mem_Icc, le_top, top_le_iff, and_false, iff_false, not_exists, not_and, and_imp,
  Embedding.some, forall_const]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝ b✝ x✝ : WithTop α
a b x : α
⊢ ↑x ∈
      (fun a b =>
          match a, b with
          | none, none => {⊤}
          | none, Option.some b => ∅
          | Option.some a, none => ↑insertNone (Ici a)
          | Option.some a, Option.some b => Finset.map Embedding.some (Icc a b))
        ↑a ↑b ↔
    ↑a ≤ ↑x ∧ ↑x ≤ ↑b
[PROOFSTEP]
simp only [some, le_eq_subset, Embedding.some, mem_map, mem_Icc, Embedding.coeFn_mk, some_le_some, aux]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝ b x : WithTop α
a : α
⊢ ⊤ ∈
      (fun a b =>
          match a, b with
          | none, x => ∅
          | Option.some a, none => Finset.map Embedding.some (Ici a)
          | Option.some a, Option.some b => Finset.map Embedding.some (Ico a b))
        ↑a ⊤ ↔
    ↑a ≤ ⊤ ∧ ⊤ < ⊤
[PROOFSTEP]
simp [some, Embedding.some]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝ b x✝ : WithTop α
a x : α
⊢ ↑x ∈
      (fun a b =>
          match a, b with
          | none, x => ∅
          | Option.some a, none => Finset.map Embedding.some (Ici a)
          | Option.some a, Option.some b => Finset.map Embedding.some (Ico a b))
        ↑a ⊤ ↔
    ↑a ≤ ↑x ∧ ↑x < ⊤
[PROOFSTEP]
simp only [some, Embedding.some, mem_map, mem_Ici, Embedding.coeFn_mk, some_le_some, aux, top, some_lt_none, and_true]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝ b✝ x : WithTop α
a b : α
⊢ ⊤ ∈
      (fun a b =>
          match a, b with
          | none, x => ∅
          | Option.some a, none => Finset.map Embedding.some (Ici a)
          | Option.some a, Option.some b => Finset.map Embedding.some (Ico a b))
        ↑a ↑b ↔
    ↑a ≤ ⊤ ∧ ⊤ < ↑b
[PROOFSTEP]
simp [some, Embedding.some]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝ b✝ x✝ : WithTop α
a b x : α
⊢ ↑x ∈
      (fun a b =>
          match a, b with
          | none, x => ∅
          | Option.some a, none => Finset.map Embedding.some (Ici a)
          | Option.some a, Option.some b => Finset.map Embedding.some (Ico a b))
        ↑a ↑b ↔
    ↑a ≤ ↑x ∧ ↑x < ↑b
[PROOFSTEP]
simp [some, Embedding.some, aux]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝ b x : WithTop α
a : α
⊢ ⊤ ∈
      (fun a b =>
          match a, b with
          | none, x => ∅
          | Option.some a, none => ↑insertNone (Ioi a)
          | Option.some a, Option.some b => Finset.map Embedding.some (Ioc a b))
        ↑a ⊤ ↔
    ↑a < ⊤ ∧ ⊤ ≤ ⊤
[PROOFSTEP]
simp [some, insertNone, top]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝ b x✝ : WithTop α
a x : α
⊢ ↑x ∈
      (fun a b =>
          match a, b with
          | none, x => ∅
          | Option.some a, none => ↑insertNone (Ioi a)
          | Option.some a, Option.some b => Finset.map Embedding.some (Ioc a b))
        ↑a ⊤ ↔
    ↑a < ↑x ∧ ↑x ≤ ⊤
[PROOFSTEP]
simp [some, Embedding.some, insertNone, aux]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝ b✝ x : WithTop α
a b : α
⊢ ⊤ ∈
      (fun a b =>
          match a, b with
          | none, x => ∅
          | Option.some a, none => ↑insertNone (Ioi a)
          | Option.some a, Option.some b => Finset.map Embedding.some (Ioc a b))
        ↑a ↑b ↔
    ↑a < ⊤ ∧ ⊤ ≤ ↑b
[PROOFSTEP]
simp [some, Embedding.some, insertNone]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝ b✝ x✝ : WithTop α
a b x : α
⊢ ↑x ∈
      (fun a b =>
          match a, b with
          | none, x => ∅
          | Option.some a, none => ↑insertNone (Ioi a)
          | Option.some a, Option.some b => Finset.map Embedding.some (Ioc a b))
        ↑a ↑b ↔
    ↑a < ↑x ∧ ↑x ≤ ↑b
[PROOFSTEP]
simp [some, Embedding.some, insertNone, aux]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝ b x : WithTop α
a : α
⊢ ⊤ ∈
      (fun a b =>
          match a, b with
          | none, x => ∅
          | Option.some a, none => Finset.map Embedding.some (Ioi a)
          | Option.some a, Option.some b => Finset.map Embedding.some (Ioo a b))
        ↑a ⊤ ↔
    ↑a < ⊤ ∧ ⊤ < ⊤
[PROOFSTEP]
simp [some, Embedding.some, insertNone]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝ b x✝ : WithTop α
a x : α
⊢ ↑x ∈
      (fun a b =>
          match a, b with
          | none, x => ∅
          | Option.some a, none => Finset.map Embedding.some (Ioi a)
          | Option.some a, Option.some b => Finset.map Embedding.some (Ioo a b))
        ↑a ⊤ ↔
    ↑a < ↑x ∧ ↑x < ⊤
[PROOFSTEP]
simp [some, Embedding.some, insertNone, aux, top]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝ b✝ x : WithTop α
a b : α
⊢ ⊤ ∈
      (fun a b =>
          match a, b with
          | none, x => ∅
          | Option.some a, none => Finset.map Embedding.some (Ioi a)
          | Option.some a, Option.some b => Finset.map Embedding.some (Ioo a b))
        ↑a ↑b ↔
    ↑a < ⊤ ∧ ⊤ < ↑b
[PROOFSTEP]
simp [some, Embedding.some, insertNone]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : PartialOrder α
inst✝¹ : OrderTop α
inst✝ : LocallyFiniteOrder α
a✝ b✝ x✝ : WithTop α
a b x : α
⊢ ↑x ∈
      (fun a b =>
          match a, b with
          | none, x => ∅
          | Option.some a, none => Finset.map Embedding.some (Ioi a)
          | Option.some a, Option.some b => Finset.map Embedding.some (Ioo a b))
        ↑a ↑b ↔
    ↑a < ↑x ∧ ↑x < ↑b
[PROOFSTEP]
simp [some, Embedding.some, insertNone, aux]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder β
f : α ≃o β
⊢ ∀ (a b x : α), x ∈ (fun a b => map (Equiv.toEmbedding (symm f).toEquiv) (Icc (↑f a) (↑f b))) a b ↔ a ≤ x ∧ x ≤ b
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder β
f : α ≃o β
⊢ ∀ (a b x : α), x ∈ (fun a b => map (Equiv.toEmbedding (symm f).toEquiv) (Ico (↑f a) (↑f b))) a b ↔ a ≤ x ∧ x < b
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder β
f : α ≃o β
⊢ ∀ (a b x : α), x ∈ (fun a b => map (Equiv.toEmbedding (symm f).toEquiv) (Ioc (↑f a) (↑f b))) a b ↔ a < x ∧ x ≤ b
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrder β
f : α ≃o β
⊢ ∀ (a b x : α), x ∈ (fun a b => map (Equiv.toEmbedding (symm f).toEquiv) (Ioo (↑f a) (↑f b))) a b ↔ a < x ∧ x < b
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrderTop β
f : α ≃o β
⊢ ∀ (a x : α), x ∈ (fun a => map (Equiv.toEmbedding (symm f).toEquiv) (Ici (↑f a))) a ↔ a ≤ x
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrderTop β
f : α ≃o β
⊢ ∀ (a x : α), x ∈ (fun a => map (Equiv.toEmbedding (symm f).toEquiv) (Ioi (↑f a))) a ↔ a < x
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrderBot β
f : α ≃o β
⊢ ∀ (a x : α), x ∈ (fun a => map (Equiv.toEmbedding (symm f).toEquiv) (Iic (↑f a))) a ↔ x ≤ a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : LocallyFiniteOrderBot β
f : α ≃o β
⊢ ∀ (a x : α), x ∈ (fun a => map (Equiv.toEmbedding (symm f).toEquiv) (Iio (↑f a))) a ↔ x < a
[PROOFSTEP]
simp
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b x : Subtype p
⊢ x ∈ (fun a b => Finset.subtype p (Icc ↑a ↑b)) a b ↔ a ≤ x ∧ x ≤ b
[PROOFSTEP]
simp_rw [Finset.mem_subtype, mem_Icc, Subtype.coe_le_coe]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b x : Subtype p
⊢ x ∈ (fun a b => Finset.subtype p (Ico ↑a ↑b)) a b ↔ a ≤ x ∧ x < b
[PROOFSTEP]
simp_rw [Finset.mem_subtype, mem_Ico, Subtype.coe_le_coe, Subtype.coe_lt_coe]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b x : Subtype p
⊢ x ∈ (fun a b => Finset.subtype p (Ioc ↑a ↑b)) a b ↔ a < x ∧ x ≤ b
[PROOFSTEP]
simp_rw [Finset.mem_subtype, mem_Ioc, Subtype.coe_le_coe, Subtype.coe_lt_coe]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b x : Subtype p
⊢ x ∈ (fun a b => Finset.subtype p (Ioo ↑a ↑b)) a b ↔ a < x ∧ x < b
[PROOFSTEP]
simp_rw [Finset.mem_subtype, mem_Ioo, Subtype.coe_lt_coe]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrderTop α
a x : Subtype p
⊢ x ∈ (fun a => Finset.subtype p (Ici ↑a)) a ↔ a ≤ x
[PROOFSTEP]
simp_rw [Finset.mem_subtype, mem_Ici, Subtype.coe_le_coe]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrderTop α
a x : Subtype p
⊢ x ∈ (fun a => Finset.subtype p (Ioi ↑a)) a ↔ a < x
[PROOFSTEP]
simp_rw [Finset.mem_subtype, mem_Ioi, Subtype.coe_lt_coe]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrderBot α
a x : Subtype p
⊢ x ∈ (fun a => Finset.subtype p (Iic ↑a)) a ↔ x ≤ a
[PROOFSTEP]
simp_rw [Finset.mem_subtype, mem_Iic, Subtype.coe_le_coe]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrderBot α
a x : Subtype p
⊢ x ∈ (fun a => Finset.subtype p (Iio ↑a)) a ↔ x < a
[PROOFSTEP]
simp_rw [Finset.mem_subtype, mem_Iio, Subtype.coe_lt_coe]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
⊢ map (Embedding.subtype p) (Icc a b) = Icc ↑a ↑b
[PROOFSTEP]
rw [subtype_Icc_eq]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
⊢ map (Embedding.subtype p) (Finset.subtype p (Icc ↑a ↑b)) = Icc ↑a ↑b
[PROOFSTEP]
refine' Finset.subtype_map_of_mem fun x hx => _
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
x : α
hx : x ∈ Icc ↑a ↑b
⊢ p x
[PROOFSTEP]
rw [mem_Icc] at hx
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
x : α
hx : ↑a ≤ x ∧ x ≤ ↑b
⊢ p x
[PROOFSTEP]
exact hp hx.1 hx.2 a.prop b.prop
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
⊢ map (Embedding.subtype p) (Ico a b) = Ico ↑a ↑b
[PROOFSTEP]
rw [subtype_Ico_eq]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
⊢ map (Embedding.subtype p) (Finset.subtype p (Ico ↑a ↑b)) = Ico ↑a ↑b
[PROOFSTEP]
refine' Finset.subtype_map_of_mem fun x hx => _
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
x : α
hx : x ∈ Ico ↑a ↑b
⊢ p x
[PROOFSTEP]
rw [mem_Ico] at hx
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
x : α
hx : ↑a ≤ x ∧ x < ↑b
⊢ p x
[PROOFSTEP]
exact hp hx.1 hx.2.le a.prop b.prop
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
⊢ map (Embedding.subtype p) (Ioc a b) = Ioc ↑a ↑b
[PROOFSTEP]
rw [subtype_Ioc_eq]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
⊢ map (Embedding.subtype p) (Finset.subtype p (Ioc ↑a ↑b)) = Ioc ↑a ↑b
[PROOFSTEP]
refine' Finset.subtype_map_of_mem fun x hx => _
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
x : α
hx : x ∈ Ioc ↑a ↑b
⊢ p x
[PROOFSTEP]
rw [mem_Ioc] at hx
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
x : α
hx : ↑a < x ∧ x ≤ ↑b
⊢ p x
[PROOFSTEP]
exact hp hx.1.le hx.2 a.prop b.prop
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
⊢ map (Embedding.subtype p) (Ioo a b) = Ioo ↑a ↑b
[PROOFSTEP]
rw [subtype_Ioo_eq]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
⊢ map (Embedding.subtype p) (Finset.subtype p (Ioo ↑a ↑b)) = Ioo ↑a ↑b
[PROOFSTEP]
refine' Finset.subtype_map_of_mem fun x hx => _
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
x : α
hx : x ∈ Ioo ↑a ↑b
⊢ p x
[PROOFSTEP]
rw [mem_Ioo] at hx
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrder α
a b : Subtype p
hp : ∀ ⦃a b x : α⦄, a ≤ x → x ≤ b → p a → p b → p x
x : α
hx : ↑a < x ∧ x < ↑b
⊢ p x
[PROOFSTEP]
exact hp hx.1.le hx.2.le a.prop b.prop
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrderTop α
a : Subtype p
hp : ∀ ⦃a x : α⦄, a ≤ x → p a → p x
⊢ map (Embedding.subtype p) (Ici a) = Ici ↑a
[PROOFSTEP]
rw [subtype_Ici_eq]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrderTop α
a : Subtype p
hp : ∀ ⦃a x : α⦄, a ≤ x → p a → p x
⊢ map (Embedding.subtype p) (Finset.subtype p (Ici ↑a)) = Ici ↑a
[PROOFSTEP]
exact Finset.subtype_map_of_mem fun x hx => hp (mem_Ici.1 hx) a.prop
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrderTop α
a : Subtype p
hp : ∀ ⦃a x : α⦄, a ≤ x → p a → p x
⊢ map (Embedding.subtype p) (Ioi a) = Ioi ↑a
[PROOFSTEP]
rw [subtype_Ioi_eq]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrderTop α
a : Subtype p
hp : ∀ ⦃a x : α⦄, a ≤ x → p a → p x
⊢ map (Embedding.subtype p) (Finset.subtype p (Ioi ↑a)) = Ioi ↑a
[PROOFSTEP]
exact Finset.subtype_map_of_mem fun x hx => hp (mem_Ioi.1 hx).le a.prop
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrderBot α
a : Subtype p
hp : ∀ ⦃a x : α⦄, x ≤ a → p a → p x
⊢ map (Embedding.subtype p) (Iic a) = Iic ↑a
[PROOFSTEP]
rw [subtype_Iic_eq]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrderBot α
a : Subtype p
hp : ∀ ⦃a x : α⦄, x ≤ a → p a → p x
⊢ map (Embedding.subtype p) (Finset.subtype p (Iic ↑a)) = Iic ↑a
[PROOFSTEP]
exact Finset.subtype_map_of_mem fun x hx => hp (mem_Iic.1 hx) a.prop
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrderBot α
a : Subtype p
hp : ∀ ⦃a x : α⦄, x ≤ a → p a → p x
⊢ map (Embedding.subtype p) (Iio a) = Iio ↑a
[PROOFSTEP]
rw [subtype_Iio_eq]
[GOAL]
α : Type u_1
β : Type u_2
inst✝² : Preorder α
p : α → Prop
inst✝¹ : DecidablePred p
inst✝ : LocallyFiniteOrderBot α
a : Subtype p
hp : ∀ ⦃a x : α⦄, x ≤ a → p a → p x
⊢ map (Embedding.subtype p) (Finset.subtype p (Iio ↑a)) = Iio ↑a
[PROOFSTEP]
exact Finset.subtype_map_of_mem fun x hx => hp (mem_Iio.1 hx).le a.prop
[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝⁴ : Preorder α✝
p : α✝ → Prop
inst✝³ : DecidablePred p
α : Type u_3
s : Set α
inst✝² : SemilatticeSup α
inst✝¹ : LocallyFiniteOrder α
inst✝ : OrderBot α
h : Set.Finite s
x : α
hx : x ∈ s
⊢ x ∈ Finite.toFinset h
[PROOFSTEP]
simpa
[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝⁴ : Preorder α✝
p : α✝ → Prop
inst✝³ : DecidablePred p
α : Type u_3
s : Set α
inst✝² : Nonempty α
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
⊢ Set.Finite s ↔ BddBelow s ∧ BddAbove s
[PROOFSTEP]
obtain (rfl | hs) := s.eq_empty_or_nonempty
[GOAL]
case inl
α✝ : Type u_1
β : Type u_2
inst✝⁴ : Preorder α✝
p : α✝ → Prop
inst✝³ : DecidablePred p
α : Type u_3
inst✝² : Nonempty α
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
⊢ Set.Finite ∅ ↔ BddBelow ∅ ∧ BddAbove ∅
[PROOFSTEP]
simp only [Set.finite_empty, bddBelow_empty, bddAbove_empty, and_self]
[GOAL]
case inr
α✝ : Type u_1
β : Type u_2
inst✝⁴ : Preorder α✝
p : α✝ → Prop
inst✝³ : DecidablePred p
α : Type u_3
s : Set α
inst✝² : Nonempty α
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
hs : Set.Nonempty s
⊢ Set.Finite s ↔ BddBelow s ∧ BddAbove s
[PROOFSTEP]
exact
  ⟨fun h ↦
    ⟨⟨h.toFinset.inf' (by simpa) id, fun x hx ↦ Finset.inf'_le id (by simpa)⟩,
      ⟨h.toFinset.sup' (by simpa) id, fun x hx ↦ Finset.le_sup' id (by simpa)⟩⟩,
    fun ⟨⟨a, ha⟩, ⟨b, hb⟩⟩ ↦ (Set.finite_Icc a b).subset (fun x hx ↦ ⟨ha hx, hb hx⟩)⟩
[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝⁴ : Preorder α✝
p : α✝ → Prop
inst✝³ : DecidablePred p
α : Type u_3
s : Set α
inst✝² : Nonempty α
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
hs : Set.Nonempty s
h : Set.Finite s
⊢ Finset.Nonempty (Finite.toFinset h)
[PROOFSTEP]
simpa
[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝⁴ : Preorder α✝
p : α✝ → Prop
inst✝³ : DecidablePred p
α : Type u_3
s : Set α
inst✝² : Nonempty α
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
hs : Set.Nonempty s
h : Set.Finite s
x : α
hx : x ∈ s
⊢ x ∈ Finite.toFinset h
[PROOFSTEP]
simpa
[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝⁴ : Preorder α✝
p : α✝ → Prop
inst✝³ : DecidablePred p
α : Type u_3
s : Set α
inst✝² : Nonempty α
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
hs : Set.Nonempty s
h : Set.Finite s
⊢ Finset.Nonempty (Finite.toFinset h)
[PROOFSTEP]
simpa
[GOAL]
α✝ : Type u_1
β : Type u_2
inst✝⁴ : Preorder α✝
p : α✝ → Prop
inst✝³ : DecidablePred p
α : Type u_3
s : Set α
inst✝² : Nonempty α
inst✝¹ : Lattice α
inst✝ : LocallyFiniteOrder α
hs : Set.Nonempty s
h : Set.Finite s
x : α
hx : x ∈ s
⊢ x ∈ Finite.toFinset h
[PROOFSTEP]
simpa
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
p : α → Prop
inst✝³ : DecidablePred p
y : α
inst✝² : Preorder α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : LocallyFiniteOrder α
a : { x // x ≤ y }
⊢ y ≤ y
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
p : α → Prop
inst✝³ : DecidablePred p
y : α
inst✝² : Preorder α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : LocallyFiniteOrder α
a : { x // x ≤ y }
⊢ y ≤ y
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
p : α → Prop
inst✝³ : DecidablePred p
y : α
inst✝² : Preorder α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : LocallyFiniteOrder α
a b : { x // x ≤ y }
⊢ b ∈ (fun a => Icc a { val := y, property := (_ : y ≤ y) }) a ↔ a ≤ b
[PROOFSTEP]
simp only [Finset.mem_Icc, and_iff_left_iff_imp]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
p : α → Prop
inst✝³ : DecidablePred p
y : α
inst✝² : Preorder α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : LocallyFiniteOrder α
a b : { x // x ≤ y }
⊢ a ≤ b → b ≤ { val := y, property := (_ : y ≤ y) }
[PROOFSTEP]
exact fun _ => b.property
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
p : α → Prop
inst✝³ : DecidablePred p
y : α
inst✝² : Preorder α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : LocallyFiniteOrder α
a b : { x // x ≤ y }
⊢ b ∈ (fun a => Ioc a { val := y, property := (_ : y ≤ y) }) a ↔ a < b
[PROOFSTEP]
simp only [Finset.mem_Ioc, and_iff_left_iff_imp]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
p : α → Prop
inst✝³ : DecidablePred p
y : α
inst✝² : Preorder α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : LocallyFiniteOrder α
a b : { x // x ≤ y }
⊢ a < b → b ≤ { val := y, property := (_ : y ≤ y) }
[PROOFSTEP]
exact fun _ => b.property
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
p : α → Prop
inst✝³ : DecidablePred p
y : α
inst✝² : Preorder α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : LocallyFiniteOrder α
a b : { x // x < y }
⊢ b ∈ (fun a => Finset.subtype (fun x => x < y) (Ico (↑a) y)) a ↔ a ≤ b
[PROOFSTEP]
simp only [Finset.mem_subtype, Finset.mem_Ico, Subtype.coe_le_coe, and_iff_left_iff_imp]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
p : α → Prop
inst✝³ : DecidablePred p
y : α
inst✝² : Preorder α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : LocallyFiniteOrder α
a b : { x // x < y }
⊢ a ≤ b → ↑b < y
[PROOFSTEP]
exact fun _ => b.property
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
p : α → Prop
inst✝³ : DecidablePred p
y : α
inst✝² : Preorder α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : LocallyFiniteOrder α
a b : { x // x < y }
⊢ b ∈ (fun a => Finset.subtype (fun x => x < y) (Ioo (↑a) y)) a ↔ a < b
[PROOFSTEP]
simp only [Finset.mem_subtype, Finset.mem_Ioo, Subtype.coe_lt_coe, and_iff_left_iff_imp]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
p : α → Prop
inst✝³ : DecidablePred p
y : α
inst✝² : Preorder α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : LocallyFiniteOrder α
a b : { x // x < y }
⊢ a < b → ↑b < y
[PROOFSTEP]
exact fun _ => b.property
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
p : α → Prop
inst✝³ : DecidablePred p
y : α
inst✝² : Preorder α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : LocallyFiniteOrder α
a : { x // y ≤ x }
⊢ y ≤ y
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
p : α → Prop
inst✝³ : DecidablePred p
y : α
inst✝² : Preorder α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : LocallyFiniteOrder α
a : { x // y ≤ x }
⊢ y ≤ y
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
p : α → Prop
inst✝³ : DecidablePred p
y : α
inst✝² : Preorder α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : LocallyFiniteOrder α
a b : { x // y ≤ x }
⊢ b ∈ (fun a => Icc { val := y, property := (_ : y ≤ y) } a) a ↔ b ≤ a
[PROOFSTEP]
simp only [Finset.mem_Icc, and_iff_right_iff_imp]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
p : α → Prop
inst✝³ : DecidablePred p
y : α
inst✝² : Preorder α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : LocallyFiniteOrder α
a b : { x // y ≤ x }
⊢ b ≤ a → { val := y, property := (_ : y ≤ y) } ≤ b
[PROOFSTEP]
exact fun _ => b.property
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
p : α → Prop
inst✝³ : DecidablePred p
y : α
inst✝² : Preorder α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : LocallyFiniteOrder α
a b : { x // y ≤ x }
⊢ b ∈ (fun a => Ico { val := y, property := (_ : y ≤ y) } a) a ↔ b < a
[PROOFSTEP]
simp only [Finset.mem_Ico, and_iff_right_iff_imp]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
p : α → Prop
inst✝³ : DecidablePred p
y : α
inst✝² : Preorder α
inst✝¹ : DecidableRel fun x x_1 => x ≤ x_1
inst✝ : LocallyFiniteOrder α
a b : { x // y ≤ x }
⊢ b < a → { val := y, property := (_ : y ≤ y) } ≤ b
[PROOFSTEP]
exact fun _ => b.property
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
p : α → Prop
inst✝³ : DecidablePred p
y : α
inst✝² : Preorder α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : LocallyFiniteOrder α
a b : { x // y < x }
⊢ b ∈ (fun a => Finset.subtype (fun x => y < x) (Ioc y ↑a)) a ↔ b ≤ a
[PROOFSTEP]
simp only [Finset.mem_subtype, Finset.mem_Ioc, Subtype.coe_le_coe, and_iff_right_iff_imp]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
p : α → Prop
inst✝³ : DecidablePred p
y : α
inst✝² : Preorder α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : LocallyFiniteOrder α
a b : { x // y < x }
⊢ b ≤ a → y < ↑b
[PROOFSTEP]
exact fun _ => b.property
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
p : α → Prop
inst✝³ : DecidablePred p
y : α
inst✝² : Preorder α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : LocallyFiniteOrder α
a b : { x // y < x }
⊢ b ∈ (fun a => Finset.subtype (fun x => y < x) (Ioo y ↑a)) a ↔ b < a
[PROOFSTEP]
simp only [Finset.mem_subtype, Finset.mem_Ioo, Subtype.coe_lt_coe, and_iff_right_iff_imp]
[GOAL]
α : Type u_1
β : Type u_2
inst✝⁴ : Preorder α
p : α → Prop
inst✝³ : DecidablePred p
y : α
inst✝² : Preorder α
inst✝¹ : DecidableRel fun x x_1 => x < x_1
inst✝ : LocallyFiniteOrder α
a b : { x // y < x }
⊢ b < a → y < ↑b
[PROOFSTEP]
exact fun _ => b.property
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
p : α → Prop
inst✝² : DecidablePred p
y : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderBot α
⊢ Finite { x // x ≤ y }
[PROOFSTEP]
apply Set.Finite.to_subtype
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
p : α → Prop
inst✝² : DecidablePred p
y : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderBot α
⊢ Set.Finite fun x => Preorder.toLE.1 x y
[PROOFSTEP]
convert (Finset.Iic y).finite_toSet using 1
[GOAL]
case h.e'_2
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
p : α → Prop
inst✝² : DecidablePred p
y : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderBot α
⊢ (fun x => Preorder.toLE.1 x y) = ↑(Iic y)
[PROOFSTEP]
ext
[GOAL]
case h.e'_2.h
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
p : α → Prop
inst✝² : DecidablePred p
y : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderBot α
x✝ : α
⊢ (x✝ ∈ fun x => Preorder.toLE.1 x y) ↔ x✝ ∈ ↑(Iic y)
[PROOFSTEP]
simp
[GOAL]
case h.e'_2.h
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
p : α → Prop
inst✝² : DecidablePred p
y : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderBot α
x✝ : α
⊢ (x✝ ∈ fun x => Preorder.toLE.1 x y) ↔ x✝ ≤ y
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
p : α → Prop
inst✝² : DecidablePred p
y : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderBot α
⊢ Finite { x // x < y }
[PROOFSTEP]
apply Set.Finite.to_subtype
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
p : α → Prop
inst✝² : DecidablePred p
y : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderBot α
⊢ Set.Finite fun x => Preorder.toLT.1 x y
[PROOFSTEP]
convert (Finset.Iio y).finite_toSet using 1
[GOAL]
case h.e'_2
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
p : α → Prop
inst✝² : DecidablePred p
y : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderBot α
⊢ (fun x => Preorder.toLT.1 x y) = ↑(Iio y)
[PROOFSTEP]
ext
[GOAL]
case h.e'_2.h
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
p : α → Prop
inst✝² : DecidablePred p
y : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderBot α
x✝ : α
⊢ (x✝ ∈ fun x => Preorder.toLT.1 x y) ↔ x✝ ∈ ↑(Iio y)
[PROOFSTEP]
simp
[GOAL]
case h.e'_2.h
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
p : α → Prop
inst✝² : DecidablePred p
y : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderBot α
x✝ : α
⊢ (x✝ ∈ fun x => Preorder.toLT.1 x y) ↔ x✝ < y
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
p : α → Prop
inst✝² : DecidablePred p
y : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderTop α
⊢ Finite { x // y ≤ x }
[PROOFSTEP]
apply Set.Finite.to_subtype
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
p : α → Prop
inst✝² : DecidablePred p
y : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderTop α
⊢ Set.Finite fun x => Preorder.toLE.1 y x
[PROOFSTEP]
convert (Finset.Ici y).finite_toSet using 1
[GOAL]
case h.e'_2
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
p : α → Prop
inst✝² : DecidablePred p
y : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderTop α
⊢ (fun x => Preorder.toLE.1 y x) = ↑(Ici y)
[PROOFSTEP]
ext
[GOAL]
case h.e'_2.h
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
p : α → Prop
inst✝² : DecidablePred p
y : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderTop α
x✝ : α
⊢ (x✝ ∈ fun x => Preorder.toLE.1 y x) ↔ x✝ ∈ ↑(Ici y)
[PROOFSTEP]
simp
[GOAL]
case h.e'_2.h
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
p : α → Prop
inst✝² : DecidablePred p
y : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderTop α
x✝ : α
⊢ (x✝ ∈ fun x => Preorder.toLE.1 y x) ↔ y ≤ x✝
[PROOFSTEP]
rfl
[GOAL]
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
p : α → Prop
inst✝² : DecidablePred p
y : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderTop α
⊢ Finite { x // y < x }
[PROOFSTEP]
apply Set.Finite.to_subtype
[GOAL]
case h
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
p : α → Prop
inst✝² : DecidablePred p
y : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderTop α
⊢ Set.Finite fun x => Preorder.toLT.1 y x
[PROOFSTEP]
convert (Finset.Ioi y).finite_toSet using 1
[GOAL]
case h.e'_2
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
p : α → Prop
inst✝² : DecidablePred p
y : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderTop α
⊢ (fun x => Preorder.toLT.1 y x) = ↑(Ioi y)
[PROOFSTEP]
ext
[GOAL]
case h.e'_2.h
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
p : α → Prop
inst✝² : DecidablePred p
y : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderTop α
x✝ : α
⊢ (x✝ ∈ fun x => Preorder.toLT.1 y x) ↔ x✝ ∈ ↑(Ioi y)
[PROOFSTEP]
simp
[GOAL]
case h.e'_2.h
α : Type u_1
β : Type u_2
inst✝³ : Preorder α
p : α → Prop
inst✝² : DecidablePred p
y : α
inst✝¹ : Preorder α
inst✝ : LocallyFiniteOrderTop α
x✝ : α
⊢ (x✝ ∈ fun x => Preorder.toLT.1 y x) ↔ y < x✝
[PROOFSTEP]
rfl


[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
⊢ ∀ (p q : Bool), p ∆ q = xor p q
[PROOFSTEP]
decide
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ a ∆ b = b ∆ a
[PROOFSTEP]
simp only [symmDiff, sup_comm]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ a ∆ a = ⊥
[PROOFSTEP]
rw [symmDiff, sup_idem, sdiff_self]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ a ∆ ⊥ = a
[PROOFSTEP]
rw [symmDiff, sdiff_bot, bot_sdiff, sup_bot_eq]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ ⊥ ∆ a = a
[PROOFSTEP]
rw [symmDiff_comm, symmDiff_bot]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedCoheytingAlgebra α
a✝ b✝ c d a b : α
⊢ a ∆ b = ⊥ ↔ a = b
[PROOFSTEP]
simp_rw [symmDiff, sup_eq_bot_iff, sdiff_eq_bot_iff, le_antisymm_iff]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedCoheytingAlgebra α
a✝ b✝ c d a b : α
h : a ≤ b
⊢ a ∆ b = b \ a
[PROOFSTEP]
rw [symmDiff, sdiff_eq_bot_iff.2 h, bot_sup_eq]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedCoheytingAlgebra α
a✝ b✝ c d a b : α
h : b ≤ a
⊢ a ∆ b = a \ b
[PROOFSTEP]
rw [symmDiff, sdiff_eq_bot_iff.2 h, sup_bot_eq]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedCoheytingAlgebra α
a✝ b✝ c✝ d a b c : α
⊢ a ∆ b ≤ c ↔ a ≤ b ⊔ c ∧ b ≤ a ⊔ c
[PROOFSTEP]
simp_rw [symmDiff, sup_le_iff, sdiff_le_iff]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ a ∆ b = (a ⊔ b) \ (a ⊓ b)
[PROOFSTEP]
simp [sup_sdiff, symmDiff]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedCoheytingAlgebra α
a✝ b✝ c d a b : α
h : Disjoint a b
⊢ a ∆ b = a ⊔ b
[PROOFSTEP]
rw [symmDiff, h.sdiff_eq_left, h.sdiff_eq_right]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ a ∆ b \ c = a \ (b ⊔ c) ⊔ b \ (a ⊔ c)
[PROOFSTEP]
rw [symmDiff, sup_sdiff_distrib, sdiff_sdiff_left, sdiff_sdiff_left]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ a ∆ b \ (a ⊓ b) = a ∆ b
[PROOFSTEP]
rw [symmDiff_sdiff]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ a \ (b ⊔ a ⊓ b) ⊔ b \ (a ⊔ a ⊓ b) = a ∆ b
[PROOFSTEP]
simp [symmDiff]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ a ∆ (b \ a) = a ⊔ b
[PROOFSTEP]
rw [symmDiff, sdiff_idem]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ a \ (b \ a) ⊔ b \ a = a ⊔ b
[PROOFSTEP]
exact
  le_antisymm (sup_le_sup sdiff_le sdiff_le)
    (sup_le le_sdiff_sup <| le_sdiff_sup.trans <| sup_le le_sup_right le_sdiff_sup)
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ (a \ b) ∆ b = a ⊔ b
[PROOFSTEP]
rw [symmDiff_comm, symmDiff_sdiff_eq_sup, sup_comm]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ a ∆ b ⊔ a ⊓ b = a ⊔ b
[PROOFSTEP]
refine' le_antisymm (sup_le symmDiff_le_sup inf_le_sup) _
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ a ⊔ b ≤ a ∆ b ⊔ a ⊓ b
[PROOFSTEP]
rw [sup_inf_left, symmDiff]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ a ⊔ b ≤ (a \ b ⊔ b \ a ⊔ a) ⊓ (a \ b ⊔ b \ a ⊔ b)
[PROOFSTEP]
refine' sup_le (le_inf le_sup_right _) (le_inf _ le_sup_right)
[GOAL]
case refine'_1
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ a ≤ a \ b ⊔ b \ a ⊔ b
[PROOFSTEP]
rw [sup_right_comm]
[GOAL]
case refine'_1
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ a ≤ a \ b ⊔ b ⊔ b \ a
[PROOFSTEP]
exact le_sup_of_le_left le_sdiff_sup
[GOAL]
case refine'_2
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ b ≤ a \ b ⊔ b \ a ⊔ a
[PROOFSTEP]
rw [sup_assoc]
[GOAL]
case refine'_2
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ b ≤ a \ b ⊔ (b \ a ⊔ a)
[PROOFSTEP]
exact le_sup_of_le_right le_sdiff_sup
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ a ⊓ b ⊔ a ∆ b = a ⊔ b
[PROOFSTEP]
rw [sup_comm, symmDiff_sup_inf]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ a ∆ b ∆ (a ⊓ b) = a ⊔ b
[PROOFSTEP]
rw [← symmDiff_sdiff_inf a, sdiff_symmDiff_eq_sup, symmDiff_sup_inf]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ (a ⊓ b) ∆ (a ∆ b) = a ⊔ b
[PROOFSTEP]
rw [symmDiff_comm, symmDiff_symmDiff_inf]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ a ∆ c ≤ a ∆ b ⊔ b ∆ c
[PROOFSTEP]
refine' (sup_le_sup (sdiff_triangle a b c) <| sdiff_triangle _ b _).trans_eq _
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedCoheytingAlgebra α
a b c d : α
⊢ a \ b ⊔ b \ c ⊔ (c \ b ⊔ b \ a) = a ∆ b ⊔ b ∆ c
[PROOFSTEP]
rw [@sup_comm _ _ (c \ b), sup_sup_sup_comm, symmDiff, symmDiff]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedHeytingAlgebra α
a b c d : α
⊢ a ⇔ b = b ⇔ a
[PROOFSTEP]
simp only [(· ⇔ ·), inf_comm]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedHeytingAlgebra α
a b c d : α
⊢ a ⇔ a = ⊤
[PROOFSTEP]
rw [bihimp, inf_idem, himp_self]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedHeytingAlgebra α
a b c d : α
⊢ a ⇔ ⊤ = a
[PROOFSTEP]
rw [bihimp, himp_top, top_himp, inf_top_eq]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedHeytingAlgebra α
a b c d : α
⊢ ⊤ ⇔ a = a
[PROOFSTEP]
rw [bihimp_comm, bihimp_top]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedHeytingAlgebra α
a✝ b✝ c d a b : α
h : a ≤ b
⊢ a ⇔ b = b ⇨ a
[PROOFSTEP]
rw [bihimp, himp_eq_top_iff.2 h, inf_top_eq]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedHeytingAlgebra α
a✝ b✝ c d a b : α
h : b ≤ a
⊢ a ⇔ b = a ⇨ b
[PROOFSTEP]
rw [bihimp, himp_eq_top_iff.2 h, top_inf_eq]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedHeytingAlgebra α
a✝ b✝ c✝ d a b c : α
⊢ a ≤ b ⇔ c ↔ a ⊓ b ≤ c ∧ a ⊓ c ≤ b
[PROOFSTEP]
simp_rw [bihimp, le_inf_iff, le_himp_iff, and_comm]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedHeytingAlgebra α
a b c d : α
⊢ a ⇔ b = a ⊔ b ⇨ a ⊓ b
[PROOFSTEP]
simp [himp_inf_distrib, bihimp]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedHeytingAlgebra α
a✝ b✝ c d a b : α
h : Codisjoint a b
⊢ a ⇔ b = a ⊓ b
[PROOFSTEP]
rw [bihimp, h.himp_eq_left, h.himp_eq_right]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedHeytingAlgebra α
a b c d : α
⊢ a ⇨ b ⇔ c = (a ⊓ c ⇨ b) ⊓ (a ⊓ b ⇨ c)
[PROOFSTEP]
rw [bihimp, himp_inf_distrib, himp_himp, himp_himp]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedHeytingAlgebra α
a b c d : α
⊢ a ⊔ b ⇨ a ⇔ b = a ⇔ b
[PROOFSTEP]
rw [himp_bihimp]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedHeytingAlgebra α
a b c d : α
⊢ ((a ⊔ b) ⊓ b ⇨ a) ⊓ ((a ⊔ b) ⊓ a ⇨ b) = a ⇔ b
[PROOFSTEP]
simp [bihimp]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : CoheytingAlgebra α
a : α
⊢ a ∆ ⊤ = ￢a
[PROOFSTEP]
simp [symmDiff]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : CoheytingAlgebra α
a : α
⊢ ⊤ ∆ a = ￢a
[PROOFSTEP]
simp [symmDiff]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : CoheytingAlgebra α
a : α
⊢ (￢a) ∆ a = ⊤
[PROOFSTEP]
rw [eq_top_iff, symmDiff, hnot_sdiff, sup_sdiff_self]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : CoheytingAlgebra α
a : α
⊢ ⊤ ≤ ￢a ⊔ a
[PROOFSTEP]
exact Codisjoint.top_le codisjoint_hnot_left
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : CoheytingAlgebra α
a : α
⊢ a ∆ (￢a) = ⊤
[PROOFSTEP]
rw [symmDiff_comm, hnot_symmDiff_self]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : CoheytingAlgebra α
a✝ a b : α
h : IsCompl a b
⊢ a ∆ b = ⊤
[PROOFSTEP]
rw [h.eq_hnot, hnot_symmDiff_self]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : HeytingAlgebra α
a : α
⊢ a ⇔ ⊥ = aᶜ
[PROOFSTEP]
simp [bihimp]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : HeytingAlgebra α
a : α
⊢ ⊥ ⇔ a = aᶜ
[PROOFSTEP]
simp [bihimp]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : HeytingAlgebra α
a✝ a b : α
h : IsCompl a b
⊢ a ⇔ b = ⊥
[PROOFSTEP]
rw [h.eq_compl, compl_bihimp_self]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ (a ⊔ b) \ (a ⊓ b) = a ∆ b
[PROOFSTEP]
rw [symmDiff_eq_sup_sdiff_inf]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ Disjoint (a ∆ b) (a ⊓ b)
[PROOFSTEP]
rw [symmDiff_eq_sup_sdiff_inf]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ Disjoint ((a ⊔ b) \ (a ⊓ b)) (a ⊓ b)
[PROOFSTEP]
exact disjoint_sdiff_self_left
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ a ⊓ b ∆ c = (a ⊓ b) ∆ (a ⊓ c)
[PROOFSTEP]
rw [symmDiff_eq_sup_sdiff_inf, inf_sdiff_distrib_left, inf_sup_left, inf_inf_distrib_left, symmDiff_eq_sup_sdiff_inf]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ a ∆ b ⊓ c = (a ⊓ c) ∆ (b ⊓ c)
[PROOFSTEP]
simp_rw [@inf_comm _ _ _ c, inf_symmDiff_distrib_left]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ c \ a ∆ b = c ⊓ a ⊓ b ⊔ c \ a ⊓ c \ b
[PROOFSTEP]
simp only [(· ∆ ·), sdiff_sdiff_sup_sdiff']
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ c \ a ∆ b = c ⊓ a ⊓ b ⊔ c \ (a ⊔ b)
[PROOFSTEP]
rw [sdiff_symmDiff, sdiff_sup, sup_comm]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ a ∆ b \ a = b \ a
[PROOFSTEP]
rw [symmDiff_def, sup_sdiff, sdiff_idem, sdiff_sdiff_self, bot_sup_eq]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ a ∆ b \ b = a \ b
[PROOFSTEP]
rw [symmDiff_comm, symmDiff_sdiff_left]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ a \ a ∆ b = a ⊓ b
[PROOFSTEP]
simp [sdiff_symmDiff]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ b \ a ∆ b = a ⊓ b
[PROOFSTEP]
rw [symmDiff_comm, inf_comm, sdiff_symmDiff_left]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ a ∆ b = a ⊔ b ↔ Disjoint a b
[PROOFSTEP]
refine' ⟨fun h => _, Disjoint.symmDiff_eq_sup⟩
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
h : a ∆ b = a ⊔ b
⊢ Disjoint a b
[PROOFSTEP]
rw [symmDiff_eq_sup_sdiff_inf, sdiff_eq_self_iff_disjoint] at h
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
h : Disjoint (a ⊓ b) (a ⊔ b)
⊢ Disjoint a b
[PROOFSTEP]
exact h.of_disjoint_inf_of_le le_sup_left
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ a ≤ a ∆ b ↔ Disjoint a b
[PROOFSTEP]
refine' ⟨fun h => _, fun h => h.symmDiff_eq_sup.symm ▸ le_sup_left⟩
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
h : a ≤ a ∆ b
⊢ Disjoint a b
[PROOFSTEP]
rw [symmDiff_eq_sup_sdiff_inf] at h
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
h : a ≤ (a ⊔ b) \ (a ⊓ b)
⊢ Disjoint a b
[PROOFSTEP]
exact disjoint_iff_inf_le.mpr (le_sdiff_iff.1 <| inf_le_of_left_le h).le
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ b ≤ a ∆ b ↔ Disjoint a b
[PROOFSTEP]
rw [symmDiff_comm, le_symmDiff_iff_left, disjoint_comm]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ a ∆ b \ c ⊔ c \ a ∆ b = a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ⊔ (c \ (a ⊔ b) ⊔ c ⊓ a ⊓ b)
[PROOFSTEP]
{rw [sdiff_symmDiff', @sup_comm _ _ (c ⊓ a ⊓ b), symmDiff_sdiff]
}
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ a ∆ b \ c ⊔ c \ a ∆ b = a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ⊔ (c \ (a ⊔ b) ⊔ c ⊓ a ⊓ b)
[PROOFSTEP]
rw [sdiff_symmDiff', @sup_comm _ _ (c ⊓ a ⊓ b), symmDiff_sdiff]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ⊔ (c \ (a ⊔ b) ⊔ c ⊓ a ⊓ b) = a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ⊔ c \ (a ⊔ b) ⊔ a ⊓ b ⊓ c
[PROOFSTEP]
ac_rfl
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ a \ b ∆ c ⊔ b ∆ c \ a = a \ (b ⊔ c) ⊔ a ⊓ b ⊓ c ⊔ (b \ (c ⊔ a) ⊔ c \ (b ⊔ a))
[PROOFSTEP]
{rw [sdiff_symmDiff', @sup_comm _ _ (a ⊓ b ⊓ c), symmDiff_sdiff]
}
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ a \ b ∆ c ⊔ b ∆ c \ a = a \ (b ⊔ c) ⊔ a ⊓ b ⊓ c ⊔ (b \ (c ⊔ a) ⊔ c \ (b ⊔ a))
[PROOFSTEP]
rw [sdiff_symmDiff', @sup_comm _ _ (a ⊓ b ⊓ c), symmDiff_sdiff]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ a \ (b ⊔ c) ⊔ a ⊓ b ⊓ c ⊔ (b \ (c ⊔ a) ⊔ c \ (b ⊔ a)) = a \ (b ⊔ c) ⊔ b \ (a ⊔ c) ⊔ c \ (a ⊔ b) ⊔ a ⊓ b ⊓ c
[PROOFSTEP]
ac_rfl
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ a ∆ b ∆ c = a ∆ (b ∆ c)
[PROOFSTEP]
rw [symmDiff_symmDiff_left, symmDiff_symmDiff_right]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ a ∆ (b ∆ c) = b ∆ (a ∆ c)
[PROOFSTEP]
simp_rw [← symmDiff_assoc, symmDiff_comm]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ a ∆ b ∆ c = a ∆ c ∆ b
[PROOFSTEP]
simp_rw [symmDiff_assoc, symmDiff_comm]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ a ∆ b ∆ (c ∆ d) = a ∆ c ∆ (b ∆ d)
[PROOFSTEP]
simp_rw [symmDiff_assoc, symmDiff_left_comm]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ a ∆ (a ∆ b) = b
[PROOFSTEP]
simp [← symmDiff_assoc]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ b ∆ a ∆ a = b
[PROOFSTEP]
simp [symmDiff_assoc]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ a ∆ b ∆ a = b
[PROOFSTEP]
rw [symmDiff_comm, symmDiff_symmDiff_cancel_left]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ a ∆ b = a ↔ a ∆ b = a ∆ ⊥
[PROOFSTEP]
rw [symmDiff_bot]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ a ∆ b = a ∆ ⊥ ↔ b = ⊥
[PROOFSTEP]
rw [symmDiff_right_inj]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
⊢ a ∆ b = b ↔ a = ⊥
[PROOFSTEP]
rw [symmDiff_comm, symmDiff_eq_left]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
ha : Disjoint a c
hb : Disjoint b c
⊢ Disjoint (a ∆ b) c
[PROOFSTEP]
rw [symmDiff_eq_sup_sdiff_inf]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
ha : Disjoint a c
hb : Disjoint b c
⊢ Disjoint ((a ⊔ b) \ (a ⊓ b)) c
[PROOFSTEP]
exact (ha.sup_left hb).disjoint_sdiff_left
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
ha : a ≤ c
⊢ a ∆ b = c ↔ c \ a = b
[PROOFSTEP]
rw [← symmDiff_of_le ha]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : GeneralizedBooleanAlgebra α
a b c d : α
ha : a ≤ c
⊢ a ∆ b = c ↔ a ∆ c = b
[PROOFSTEP]
exact ((symmDiff_right_involutive a).toPerm _).apply_eq_iff_eq_symm_apply.trans eq_comm
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : BooleanAlgebra α
a b c d : α
⊢ a ⇔ (b ⇔ c) = b ⇔ (a ⇔ c)
[PROOFSTEP]
simp_rw [← bihimp_assoc, bihimp_comm]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : BooleanAlgebra α
a b c d : α
⊢ a ⇔ b ⇔ c = a ⇔ c ⇔ b
[PROOFSTEP]
simp_rw [bihimp_assoc, bihimp_comm]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : BooleanAlgebra α
a b c d : α
⊢ a ⇔ b ⇔ (c ⇔ d) = a ⇔ c ⇔ (b ⇔ d)
[PROOFSTEP]
simp_rw [bihimp_assoc, bihimp_left_comm]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : BooleanAlgebra α
a b c d : α
⊢ a ⇔ (a ⇔ b) = b
[PROOFSTEP]
simp [← bihimp_assoc]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : BooleanAlgebra α
a b c d : α
⊢ b ⇔ a ⇔ a = b
[PROOFSTEP]
simp [bihimp_assoc]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : BooleanAlgebra α
a b c d : α
⊢ a ⇔ b ⇔ a = b
[PROOFSTEP]
rw [bihimp_comm, bihimp_bihimp_cancel_left]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : BooleanAlgebra α
a b c d : α
⊢ a ∆ b = a ⊓ bᶜ ⊔ b ⊓ aᶜ
[PROOFSTEP]
simp only [(· ∆ ·), sdiff_eq]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : BooleanAlgebra α
a b c d : α
⊢ a ⇔ b = (a ⊔ bᶜ) ⊓ (b ⊔ aᶜ)
[PROOFSTEP]
simp only [(· ⇔ ·), himp_eq]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : BooleanAlgebra α
a b c d : α
⊢ a ∆ b = (a ⊔ b) ⊓ (aᶜ ⊔ bᶜ)
[PROOFSTEP]
rw [symmDiff_eq_sup_sdiff_inf, sdiff_eq, compl_inf]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : BooleanAlgebra α
a b c d : α
⊢ (a ∆ b)ᶜ = a ⇔ b
[PROOFSTEP]
simp_rw [symmDiff, compl_sup_distrib, compl_sdiff, bihimp, inf_comm]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : BooleanAlgebra α
a b c d : α
⊢ bᶜ \ aᶜ ⊔ aᶜ \ bᶜ = a ∆ b
[PROOFSTEP]
simp_rw [compl_sdiff_compl, sdiff_eq, symmDiff_eq]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : BooleanAlgebra α
a b c d : α
⊢ a ∆ b = ⊤ ↔ IsCompl a b
[PROOFSTEP]
rw [symmDiff_eq', ← compl_inf, inf_eq_top_iff, compl_eq_top, isCompl_iff, disjoint_iff, codisjoint_iff, and_comm]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : BooleanAlgebra α
a b c d : α
⊢ a ⇔ b = ⊥ ↔ IsCompl a b
[PROOFSTEP]
rw [bihimp_eq', ← compl_sup, sup_eq_bot_iff, compl_eq_bot, isCompl_iff, disjoint_iff, codisjoint_iff]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : BooleanAlgebra α
a b c d : α
⊢ a ∆ (b ∆ c) = a ⊓ (b ⊓ c ⊔ bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ
[PROOFSTEP]
{rw [symmDiff_eq, compl_symmDiff, bihimp_eq', symmDiff_eq]
}
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : BooleanAlgebra α
a b c d : α
⊢ a ∆ (b ∆ c) = a ⊓ (b ⊓ c ⊔ bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ
[PROOFSTEP]
rw [symmDiff_eq, compl_symmDiff, bihimp_eq', symmDiff_eq]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : BooleanAlgebra α
a b c d : α
⊢ a ⊓ (b ⊓ c ⊔ bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ
[PROOFSTEP]
{rw [inf_sup_left, inf_sup_right, ← sup_assoc, ← inf_assoc, ← inf_assoc]
}
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : BooleanAlgebra α
a b c d : α
⊢ a ⊓ (b ⊓ c ⊔ bᶜ ⊓ cᶜ) ⊔ (b ⊓ cᶜ ⊔ c ⊓ bᶜ) ⊓ aᶜ = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ
[PROOFSTEP]
rw [inf_sup_left, inf_sup_right, ← sup_assoc, ← inf_assoc, ← inf_assoc]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : BooleanAlgebra α
a b c d : α
⊢ a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ b ⊓ cᶜ ⊓ aᶜ ⊔ c ⊓ bᶜ ⊓ aᶜ = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ aᶜ ⊓ b ⊓ cᶜ ⊔ aᶜ ⊓ bᶜ ⊓ c
[PROOFSTEP]
congr 1
[GOAL]
case e_a
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : BooleanAlgebra α
a b c d : α
⊢ a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ b ⊓ cᶜ ⊓ aᶜ = a ⊓ b ⊓ c ⊔ a ⊓ bᶜ ⊓ cᶜ ⊔ aᶜ ⊓ b ⊓ cᶜ
[PROOFSTEP]
congr 1
[GOAL]
case e_a.e_a
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : BooleanAlgebra α
a b c d : α
⊢ b ⊓ cᶜ ⊓ aᶜ = aᶜ ⊓ b ⊓ cᶜ
[PROOFSTEP]
rw [inf_comm, inf_assoc]
[GOAL]
case e_a
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : BooleanAlgebra α
a b c d : α
⊢ c ⊓ bᶜ ⊓ aᶜ = aᶜ ⊓ bᶜ ⊓ c
[PROOFSTEP]
apply inf_left_right_swap
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : BooleanAlgebra α
a b c d : α
h : Disjoint a b
⊢ c ≤ a ∆ c ⊔ b ∆ c
[PROOFSTEP]
trans c \ (a ⊓ b)
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : BooleanAlgebra α
a b c d : α
h : Disjoint a b
⊢ c ≤ c \ (a ⊓ b)
[PROOFSTEP]
rw [h.eq_bot, sdiff_bot]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : BooleanAlgebra α
a b c d : α
h : Disjoint a b
⊢ c \ (a ⊓ b) ≤ a ∆ c ⊔ b ∆ c
[PROOFSTEP]
rw [sdiff_inf]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : BooleanAlgebra α
a b c d : α
h : Disjoint a b
⊢ c \ a ⊔ c \ b ≤ a ∆ c ⊔ b ∆ c
[PROOFSTEP]
exact sup_le_sup le_sup_right le_sup_right
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : BooleanAlgebra α
a b c d : α
h : Disjoint b c
⊢ a ≤ a ∆ b ⊔ a ∆ c
[PROOFSTEP]
simp_rw [symmDiff_comm a]
[GOAL]
ι : Type u_1
α : Type u_2
β : Type u_3
π : ι → Type u_4
inst✝ : BooleanAlgebra α
a b c d : α
h : Disjoint b c
⊢ a ≤ b ∆ a ⊔ c ∆ a
[PROOFSTEP]
exact h.le_symmDiff_sup_symmDiff_left