case a
ι : Type ?u.114646
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : DecidableEq α
a a✝ : α
⊢ a✝ ∈ insert a (Ioi a) ↔ a✝ ∈ Ici a
ι : Type ?u.114646
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : DecidableEq α
a : α
⊢ insert a (Ioi a) = Ici a
ext
no goals
case a
ι : Type ?u.114646
α : Type u_1
inst✝² : PartialOrder α
inst✝¹ : LocallyFiniteOrderTop α
inst✝ : DecidableEq α
a a✝ : α
⊢ a✝ ∈ insert a (Ioi a) ↔ a✝ ∈ Ici a
simp_rw [Finset.mem_insert, mem_Ici, mem_Ioi, le_iff_lt_or_eq, or_comm, eq_comm]