-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Limits.Cokernels (goal)
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₂)
⊢ Cofork.π (c₁.mapBifunctor c₂ (curriedTensor C)) ≫
      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)))) =
    Cofork.π (c₁.tensor c₂)
have dsimp : 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: dsimp only [Cofork.π]