no goals
X : Type u_1
Y : Type u_2
Z : Type ?u.81131
α : Type ?u.81134
ι : Type ?u.81137
π : ι → Type ?u.81142
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : (i : ι) → TopologicalSpace (π i)
x✝ y✝ z : X
s : Set X
f : X → Y
t : Set (SeparationQuotient X)
x : X
y : Y
⊢ Filter.map (Prod.map mk mk) (𝓝 (x, y)) = 𝓝 (mk x, mk y)
rw [nhds_prod_eq, ← prod_map_map_eq', map_mk_nhds, map_mk_nhds, nhds_prod_eq]