case a
ι : Type ?u.118371
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : DecidableEq α
b a✝ : α
⊢ a✝ ∈ insert b (Iio b) ↔ a✝ ∈ Iic b
ι : Type ?u.118371
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : DecidableEq α
b : α
⊢ insert b (Iio b) = Iic b
ext
no goals
case a
ι : Type ?u.118371
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderBot α
inst✝ : DecidableEq α
b a✝ : α
⊢ a✝ ∈ insert b (Iio b) ↔ a✝ ∈ Iic b
simp_rw [Finset.mem_insert, mem_Iic, mem_Iio, le_iff_lt_or_eq, or_comm]