no goals
α : Type u
β : Type v
ι : Sort w
a : α
s✝ s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
x : α
s : Set α
⊢ ClusterPt x (𝓟 s) ↔ ∃ᶠ (y : α) in 𝓝 x, y ∈ s
simp only [clusterPt_principal_iff, frequently_iff, Set.Nonempty, exists_prop, mem_inter_iff]