no goals
ι : Sort ?u.15925
α : Type u_1
β : Type ?u.15931
X : Type ?u.15934
Y : Type ?u.15937
s : Set (Filter α)
l : Filter α
⊢ l ∈ closure s ↔ ∀ (t : Set α), t ∈ l → ∃ l', l' ∈ s ∧ t ∈ l'
simp only [closure_eq_compl_interior_compl, Filter.mem_interior, mem_compl_iff, not_exists,
  not_forall, Classical.not_not, exists_prop, not_and, and_comm, subset_def, mem_Iic,
  le_principal_iff]