have ⟨u, hu₁, hu₂, hu₃⟩ := hs
α : Type u_1
τ : TopologicalSpace α
a : α
s : Set α
hs : ∃ t, t ⊆ s ∧ sets τ t ∧ a ∈ t
⊢ a ∈ s
α : Type u_1
τ : TopologicalSpace α
a : α
s : Set α
hs : ∃ t, t ⊆ s ∧ sets τ t ∧ a ∈ t
u : Set α
hu₁ : u ⊆ s
hu₂ : sets τ u
hu₃ : a ∈ u
⊢ a ∈ s