no goals
α : Type u_1
β : Type ?u.21904
γ : Type ?u.21907
δ : Type ?u.21910
inst✝ : TopologicalSpace α
a : α
s : Set α
⊢ insert a s ∈ 𝓝 a ↔ s ∈ 𝓝[{a}ᶜ] a
simp only [nhdsWithin, mem_inf_principal, mem_compl_iff, mem_singleton_iff, or_iff_not_imp_left,
  insert_def]