∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C}
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct W X] [inst_2 : CategoryTheory.Limits.HasBinaryProduct Y Z]
  (f : W ≅ Y) (g : X ≅ Z), (CategoryTheory.Limits.prod.mapIso f g).hom = CategoryTheory.Limits.prod.map f.hom g.hom