no goals
α : Type u
β : Type v
γ : Type u_1
δ : Type u_2
ε : Type ?u.64695
ζ : Type ?u.64698
inst✝⁵ : TopologicalSpace α
inst✝⁴ : TopologicalSpace β
inst✝³ : TopologicalSpace γ
inst✝² : TopologicalSpace δ
inst✝¹ : TopologicalSpace ε
inst✝ : TopologicalSpace ζ
f : α → β
g : γ → δ
hf : Inducing f
hg : Inducing g
x✝ : α × γ
a : α
b : γ
⊢ 𝓝 (a, b) = comap (Prod.map f g) (𝓝 (Prod.map f g (a, b)))
simp_rw [Prod.map, nhds_prod_eq, hf.nhds_eq_comap,
hg.nhds_eq_comap, prod_comap_comap_eq]