no goals
α : Type u_1
β : Type u_2
γ : Type ?u.69386
δ : Type ?u.69389
inst✝³ : TopologicalSpace α
inst✝² : TopologicalSpace β
inst✝¹ : TopologicalSpace γ
inst✝ : TopologicalSpace δ
h : α ≃ₜ β
y : β
⊢ comap (↑h) (𝓝 y) = 𝓝 (↑(Homeomorph.symm h) y)
rw [h.nhds_eq_comap, h.apply_symm_apply]