no goals
α : Type u_1
β : Type ?u.19057
γ : Type ?u.19060
δ : Type ?u.19063
inst✝ : TopologicalSpace α
a : α
s : Set α
⊢ 𝓝[insert a s] a = pure a ⊔ 𝓝[s] a
rw [← singleton_union, nhdsWithin_union, nhdsWithin_singleton]