∀ (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 : C₁ × C₂} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Prod.mkHom
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft
          (CategoryTheory.MonoidalCategoryStruct.tensorUnit C₁, CategoryTheory.MonoidalCategoryStruct.tensorUnit C₂).1
          f.1)
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft
          (CategoryTheory.MonoidalCategoryStruct.tensorUnit C₁, CategoryTheory.MonoidalCategoryStruct.tensorUnit C₂).2
          f.2))
      (match Y with
        | (X₁, X₂) =>
          (CategoryTheory.MonoidalCategoryStruct.leftUnitor X₁).prod
            (CategoryTheory.MonoidalCategoryStruct.leftUnitor X₂)).hom =
    CategoryTheory.CategoryStruct.comp
      (match X with
        | (X₁, X₂) =>
          (CategoryTheory.MonoidalCategoryStruct.leftUnitor X₁).prod
            (CategoryTheory.MonoidalCategoryStruct.leftUnitor X₂)).hom
      f