no goals
α : Type u_1
β : Type u_2
γ : Type ?u.44482
δ : Type ?u.44485
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
s : Set α
t : Set β
x : α
y : β
h : IsImage e s t
hx : x ∈ e.source
⊢ map (↑e) (𝓝[s] x) = 𝓝[t] ↑e x
rw [e.map_nhdsWithin_eq hx, h.image_eq, e.nhdsWithin_target_inter (e.map_source hx)]