case a
ι : Type ?u.117576
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : DecidableEq α
b a✝ : α
⊢ a✝ ∈ erase (Iic b) b ↔ a✝ ∈ Iio b
ι : Type ?u.117576
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : DecidableEq α
b : α
⊢ erase (Iic b) b = Iio b
ext
no goals
case a
ι : Type ?u.117576
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : DecidableEq α
b a✝ : α
⊢ a✝ ∈ erase (Iic b) b ↔ a✝ ∈ Iio b
simp_rw [Finset.mem_erase, mem_Iic, mem_Iio, lt_iff_le_and_ne, and_comm]