no goals
α : Type u_1
β : Type ?u.22542
γ : Type ?u.22545
δ : Type ?u.22548
inst✝ : TopologicalSpace α
a : α
⊢ 𝓝[{a}ᶜ] a ⊔ pure a = 𝓝 a
rw [← nhdsWithin_singleton, ← nhdsWithin_union, compl_union_self, nhdsWithin_univ]