no goals
α : Type u
β : Type v
ι : Sort w
a : α
s s₁ s₂ t : Set α
p p₁ p₂ : α → Prop
inst✝ : TopologicalSpace α
x : α
f : Filter α
H : 𝓝 x ≤ f
⊢ ClusterPt x f
simp only [ClusterPt, inf_eq_left.mpr H, nhds_neBot]