∀ (C₁ : Type u_1) [inst : CategoryTheory.Category.{u_3, u_1} C₁] [inst_1 : CategoryTheory.MonoidalCategory C₁]
  (C₂ : Type u_2) [inst_2 : CategoryTheory.Category.{u_4, u_2} C₂] [inst_3 : CategoryTheory.MonoidalCategory C₂]
  {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C₁ × C₂} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Prod.mkHom (CategoryTheory.MonoidalCategoryStruct.tensorHom f₁.1 f₂.1)
        (CategoryTheory.MonoidalCategoryStruct.tensorHom f₁.2 f₂.2))
      (CategoryTheory.Prod.mkHom (CategoryTheory.MonoidalCategoryStruct.tensorHom g₁.1 g₂.1)
        (CategoryTheory.MonoidalCategoryStruct.tensorHom g₁.2 g₂.2)) =
    CategoryTheory.Prod.mkHom
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.comp f₁ g₁).1
        (CategoryTheory.CategoryStruct.comp f₂ g₂).1)
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.comp f₁ g₁).2
        (CategoryTheory.CategoryStruct.comp f₂ g₂).2)