no goals
α : Type u_1
β : Type u_2
γ : Type ?u.68858
δ : Type ?u.68861
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
h : α ≃ₜ β
x : α
⊢ map (↑(Homeomorph.symm h)) (𝓝 (↑h x)) = 𝓝 x
rw [h.symm.map_nhds_eq, h.symm_apply_apply]