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