no goals
α : Type ?u.127326
β : Type ?u.127329
γ : Type ?u.127332
δ : Type ?u.127335
inst✝⁴ : TopologicalSpace α
inst✝³ : TopologicalSpace β
inst✝² : TopologicalSpace γ
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
tY : TopologicalSpace Y
inst✝ : DiscreteTopology Y
f : X → Y
hf : _root_.Embedding f
x : X
⊢ 𝓝 x = pure x
rw [hf.nhds_eq_comap, nhds_discrete, comap_pure, ← image_singleton, hf.inj.preimage_image,
  principal_singleton]