[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
