no goals
α : Type ua
β : Type ub
γ : Type uc
δ : Type ud
ι : Sort ?u.154039
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
⊢ 𝓤 (α × β) = map (fun p => ((p.fst.fst, p.snd.fst), p.fst.snd, p.snd.snd)) (𝓤 α ×ˢ 𝓤 β)
rw [map_swap4_eq_comap, uniformity_prod_eq_comap_prod]