case a
ι : Type ?u.113545
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : DecidableEq α
a a✝ : α
⊢ a✝ ∈ erase (Ici a) a ↔ a✝ ∈ Ioi a
ι : Type ?u.113545
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : DecidableEq α
a : α
⊢ erase (Ici a) a = Ioi a
ext
no goals
case a
ι : Type ?u.113545
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : DecidableEq α
a a✝ : α
⊢ a✝ ∈ erase (Ici a) a ↔ a✝ ∈ Ioi a
simp_rw [Finset.mem_erase, mem_Ici, mem_Ioi, lt_iff_le_and_ne, and_comm, ne_comm]