no goals
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
s : Set α
x : α
⊢ x ∈ closure s ↔ ∃ u, s ∈ u ∧ ↑u ≤ 𝓝 x
simp [closure_eq_cluster_pts, ClusterPt, ← exists_ultrafilter_iff, and_comm]