rw [mem_nhds_def]
α : Type u_1
τ : TopologicalSpace α
a : α
s : Set α
hs : sets τ s
ha : a ∈ s
⊢ s ∈ 𝓝 a
α : Type u_1
τ : TopologicalSpace α
a : α
s : Set α
hs : sets τ s
ha : a ∈ s
⊢ ∃ t, t ⊆ s ∧ sets τ t ∧ a ∈ t