∀ (J₁ : Type u_2) (C : Type u_4) [inst : CategoryTheory.Category.{u_1, u_2} J₁]
  [inst_1 : CategoryTheory.Category.{u_3, u_4} C] [inst_2 : CategoryTheory.MonoidalCategory C]
  (x : CategoryTheory.Functor J₁ C × CategoryTheory.Functor J₁ C) {X Y : J₁} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp
      ((((CategoryTheory.MonoidalCategory.externalProductBifunctor J₁ J₁ C).comp
                ((CategoryTheory.Functor.whiskeringLeft J₁ (J₁ × J₁) C).obj (CategoryTheory.Functor.diag J₁))).obj
            x).map
        f)
      ((fun x_1 =>
            CategoryTheory.Iso.refl
              ((((CategoryTheory.MonoidalCategory.externalProductBifunctor J₁ J₁ C).comp
                        ((CategoryTheory.Functor.whiskeringLeft J₁ (J₁ × J₁) C).obj
                          (CategoryTheory.Functor.diag J₁))).obj
                    x).obj
                x_1))
          Y).hom =
    CategoryTheory.CategoryStruct.comp
      ((fun x_1 =>
            CategoryTheory.Iso.refl
              ((((CategoryTheory.MonoidalCategory.externalProductBifunctor J₁ J₁ C).comp
                        ((CategoryTheory.Functor.whiskeringLeft J₁ (J₁ × J₁) C).obj
                          (CategoryTheory.Functor.diag J₁))).obj
                    x).obj
                x_1))
          X).hom
      (((CategoryTheory.MonoidalCategory.tensor (CategoryTheory.Functor J₁ C)).obj x).map f)