no goals
α : Type u_1
β : Type u_2
γ : Type ?u.30205
δ : Type ?u.30208
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
e : LocalHomeomorph α β
e' : LocalHomeomorph β γ
x : α
hx : x ∈ e.source
⊢ Tendsto (↑(LocalHomeomorph.symm e)) (𝓝 (↑e x)) (𝓝 x)
simpa only [ContinuousAt, e.left_inv hx] using e.continuousAt_symm (e.map_source hx)