-- Module: Mathlib.CategoryTheory.Monoidal.Limits.Cokernels
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : Preadditive.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalPreadditive.{v_1, u_1} C
X₁ Y₁ : C
f₁ : X₁ ⟶ Y₁
c₁ : CokernelCofork f₁
hc₁ : IsColimit c₁
X₂ Y₂ : C
f₂ : X₂ ⟶ Y₂
c₂ : CokernelCofork f₂
hc₂ : IsColimit c₂
inst_4 : HasBinaryCoproduct.{v_1, u_1} (tensorObj.{v_1, u_1} (𝒞 := inst) X₁ Y₂) (tensorObj.{v_1, u_1} (𝒞 := inst) Y₁ X₂)
inst_5 : PreservesColimit (parallelPair f₂ 0) (tensorLeft c₁.pt)
inst_6 : PreservesColimit (parallelPair f₁ 0) (tensorRight Y₂)
inst_7 : PreservesColimit (parallelPair f₁ 0) (tensorRight X₂)
this :
  HasBinaryCoproduct.{v_1, u_1} (Functor.obj.{v_1, v_1, u_1, u_1} (Functor.obj (curriedTensor C) X₁) Y₂)
    (Functor.obj.{v_1, v_1, u_1, u_1} (Functor.obj (curriedTensor C) Y₁) X₂)
⊢ Eq (α :=
    Functor.obj.{v_1, v_1, u_1, u_1} (Functor.obj (curriedTensor C) Y₁) Y₂ ⟶
      Cocone.pt (F :=
        parallelPair (X :=
          coprod.{v_1, u_1} (Functor.obj.{v_1, v_1, u_1, u_1} (Functor.obj (curriedTensor C) X₁) Y₂)
            (Functor.obj.{v_1, v_1, u_1, u_1} (Functor.obj (curriedTensor C) Y₁) X₂))
          (coprod.desc (NatTrans.app (Functor.map (curriedTensor C) f₁) Y₂)
            (Functor.map (Functor.obj (curriedTensor C) Y₁) f₂))
          0)
        (c₁.tensor c₂))
    (CategoryStruct.comp (Y :=
        Cocone.pt (F :=
          parallelPair (X :=
            coprod.{v_1, u_1} (Functor.obj.{v_1, v_1, u_1, u_1} (Functor.obj (curriedTensor C) X₁) Y₂)
              (Functor.obj.{v_1, v_1, u_1, u_1} (Functor.obj (curriedTensor C) Y₁) X₂))
            (coprod.desc (NatTrans.app (Functor.map (curriedTensor C) f₁) Y₂)
              (Functor.map (Functor.obj (curriedTensor C) Y₁) f₂))
            0)
          (c₁.mapBifunctor c₂ (curriedTensor C)))
        (NatTrans.app (Cocone.ι (c₁.mapBifunctor c₂ (curriedTensor C))) WalkingParallelPair.one :
          (parallelPair (X :=
                  coprod.{v_1, u_1} (Functor.obj.{v_1, v_1, u_1, u_1} (Functor.obj (curriedTensor C) X₁) Y₂)
                    (Functor.obj.{v_1, v_1, u_1, u_1} (Functor.obj (curriedTensor C) Y₁) X₂))
                  (coprod.desc (NatTrans.app (Functor.map (curriedTensor C) f₁) Y₂)
                    (Functor.map (Functor.obj (curriedTensor C) Y₁) f₂))
                  0).obj
              WalkingParallelPair.one ⟶
            Functor.obj.{0, v_1, 0, u_1}
              (Functor.obj (Functor.const WalkingParallelPair)
                (Cocone.pt (F :=
                  parallelPair (X :=
                    coprod.{v_1, u_1} (Functor.obj.{v_1, v_1, u_1, u_1} (Functor.obj (curriedTensor C) X₁) Y₂)
                      (Functor.obj.{v_1, v_1, u_1, u_1} (Functor.obj (curriedTensor C) Y₁) X₂))
                    (coprod.desc (NatTrans.app (Functor.map (curriedTensor C) f₁) Y₂)
                      (Functor.map (Functor.obj (curriedTensor C) Y₁) f₂))
                    0)
                  (c₁.mapBifunctor c₂ (curriedTensor C))))
              WalkingParallelPair.one)
        (Iso.hom
          (Iso.refl
            (Cocone.pt (F :=
              parallelPair (X :=
                coprod.{v_1, u_1} (Functor.obj.{v_1, v_1, u_1, u_1} (Functor.obj (curriedTensor C) X₁) Y₂)
                  (Functor.obj.{v_1, v_1, u_1, u_1} (Functor.obj (curriedTensor C) Y₁) X₂))
                (coprod.desc (NatTrans.app (Functor.map (curriedTensor C) f₁) Y₂)
                  (Functor.map (Functor.obj (curriedTensor C) Y₁) f₂))
                0)
              (c₁.mapBifunctor c₂ (curriedTensor C))))) :
      Functor.obj.{v_1, v_1, u_1, u_1} (Functor.obj (curriedTensor C) Y₁) Y₂ ⟶
        Cocone.pt (F :=
          parallelPair (X :=
            coprod.{v_1, u_1} (Functor.obj.{v_1, v_1, u_1, u_1} (Functor.obj (curriedTensor C) X₁) Y₂)
              (Functor.obj.{v_1, v_1, u_1, u_1} (Functor.obj (curriedTensor C) Y₁) X₂))
            (coprod.desc (NatTrans.app (Functor.map (curriedTensor C) f₁) Y₂)
              (Functor.map (Functor.obj (curriedTensor C) Y₁) f₂))
            0)
          (c₁.tensor c₂))
    (NatTrans.app (Cocone.ι (c₁.tensor c₂)) WalkingParallelPair.one :
      (parallelPair (X :=
              coprod.{v_1, u_1} (Functor.obj.{v_1, v_1, u_1, u_1} (Functor.obj (curriedTensor C) X₁) Y₂)
                (Functor.obj.{v_1, v_1, u_1, u_1} (Functor.obj (curriedTensor C) Y₁) X₂))
              (coprod.desc (NatTrans.app (Functor.map (curriedTensor C) f₁) Y₂)
                (Functor.map (Functor.obj (curriedTensor C) Y₁) f₂))
              0).obj
          WalkingParallelPair.one ⟶
        Functor.obj.{0, v_1, 0, u_1}
          (Functor.obj (Functor.const WalkingParallelPair)
            (Cocone.pt (F :=
              parallelPair (X :=
                coprod.{v_1, u_1} (Functor.obj.{v_1, v_1, u_1, u_1} (Functor.obj (curriedTensor C) X₁) Y₂)
                  (Functor.obj.{v_1, v_1, u_1, u_1} (Functor.obj (curriedTensor C) Y₁) X₂))
                (coprod.desc (NatTrans.app (Functor.map (curriedTensor C) f₁) Y₂)
                  (Functor.map (Functor.obj (curriedTensor C) Y₁) f₂))
                0)
              (c₁.tensor c₂)))
          WalkingParallelPair.one)

Tactic:
simp [tensorHom_def]

Premises used: CategoryTheory.MonoidalCategory.tensorHom_def