case h
ι : Sort ?u.16896
α : Type u_1
β : Type ?u.16902
X : Type ?u.16905
Y : Type ?u.16908
l l' : Filter α
⊢ l' ∈ closure {l} ↔ l' ∈ Ici l
ι : Sort ?u.16896
α : Type u_1
β : Type ?u.16902
X : Type ?u.16905
Y : Type ?u.16908
l : Filter α
⊢ closure {l} = Ici l
ext l'
no goals
case h
ι : Sort ?u.16896
α : Type u_1
β : Type ?u.16902
X : Type ?u.16905
Y : Type ?u.16908
l l' : Filter α
⊢ l' ∈ closure {l} ↔ l' ∈ Ici l
simp [Filter.mem_closure, Filter.le_def]