∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {X' : Type u_3}
  {Y' : Type u_4} [inst_2 : TopologicalSpace X'] [inst_3 : TopologicalSpace Y'] (h₁ : X ≃ₜ X') (h₂ : Y ≃ₜ Y'),
  Continuous (h₁.prodCongr h₂.toEquiv).toFun