no goals
α : Type u_1
β : Type u_2
γ : Type ?u.360626
δ : Type ?u.360629
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
f : α → β
hf : _root_.Embedding f
s : Set α
x : α
⊢ map f (𝓝[s] x) = 𝓝[f '' s] f x
rw [nhdsWithin, Filter.map_inf hf.inj, hf.map_nhds_eq, map_principal, ← nhdsWithin_inter',
  inter_eq_self_of_subset_right (image_subset_range _ _)]