rw [mem_nhds_def]
α : Type u_1
τ : TopologicalSpace α
f : Filter α
a : α
s : Set α
h : a ∈ s
ho : sets τ s
hsf : 𝓟 s ≤ f
u : Set α
hu : u ∈ f
⊢ u ∈ 𝓝 a
α : Type u_1
τ : TopologicalSpace α
f : Filter α
a : α
s : Set α
h : a ∈ s
ho : sets τ s
hsf : 𝓟 s ≤ f
u : Set α
hu : u ∈ f
⊢ ∃ t, t ⊆ u ∧ sets τ t ∧ a ∈ t