-- Module: Mathlib.CategoryTheory.Monoidal.Arrow
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : HasInitial.{v, u} C
inst_3 : CartesianMonoidalCategory.{v, u} C
inst_4 : MonoidalClosed.{v, u} C
inst_5 : BraidedCategory.{v, u} C
X Y : Arrow.{v, u} C
apply apply₁ :
  IsInitial.{v, u}
    (obj.{v, v, u, u} (obj (curriedTensor C) X.right)
      (Arrow.left.{v, u} ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))))
⊢ Eq (α :=
    obj.{v, v, u, u} (tensorRight Y.right)
        (obj.{v, v, u, u} (obj (curriedTensor C) X.right)
          (Arrow.left.{v, u} ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow)))) ⟶
      (tensorObj (𝒞 := instCategoryArrow) X Y).left)
    (CategoryStruct.comp (Y :=
      obj.{v, v, u, u} (tensorRight Y.right)
        (pushout (X :=
          obj.{v, v, u, u} (obj (curriedTensor C) X.left)
            (Arrow.left.{v, u} ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))))
          (NatTrans.app (map (curriedTensor C) X.hom)
            (Arrow.left.{v, u} ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))))
          (map (obj (curriedTensor C) X.left) (Arrow.hom ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))))))
      (map (tensorRight Y.right)
        (pushout.inl
          (NatTrans.app (map (curriedTensor C) X.hom)
            (Arrow.left.{v, u} ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))))
          (map (obj (curriedTensor C) X.left) (Arrow.hom ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))))))
      (CategoryStruct.comp (Y :=
        pushout (X :=
          obj.{v, v, u, u}
            (obj (curriedTensor C)
              (tensorObj (𝒞 := instCategoryArrow) X ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))).left)
            Y.left)
          (NatTrans.app
            (map (curriedTensor C)
              (tensorObj (𝒞 := instCategoryArrow) X ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))).hom)
            Y.left)
          (map
            (obj (curriedTensor C)
              (tensorObj (𝒞 := instCategoryArrow) X ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))).left)
            Y.hom))
        (pushout.inr
          (NatTrans.app
            (map (curriedTensor C)
              (tensorObj (𝒞 := instCategoryArrow) X ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))).hom)
            Y.left)
          (map
            (obj (curriedTensor C)
              (tensorObj (𝒞 := instCategoryArrow) X ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))).left)
            Y.hom))
        (Arrow.Hom.left (Iso.hom (α_ X ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow)) Y) ≫ X ◁ Iso.hom (λ_ Y)))))
    (CategoryStruct.comp (Y :=
      obj.{v, v, u, u} (tensorRight Y.right)
        (pushout (X :=
          obj.{v, v, u, u} (obj (curriedTensor C) X.left)
            (Arrow.left.{v, u} ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))))
          (NatTrans.app (map (curriedTensor C) X.hom)
            (Arrow.left.{v, u} ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))))
          (map (obj (curriedTensor C) X.left) (Arrow.hom ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))))))
      (map (tensorRight Y.right)
        (pushout.inl
          (NatTrans.app (map (curriedTensor C) X.hom)
            (Arrow.left.{v, u} ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))))
          (map (obj (curriedTensor C) X.left) (Arrow.hom ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))))))
      (CategoryStruct.comp (Y :=
        pushout (X :=
          obj.{v, v, u, u}
            (obj (curriedTensor C)
              (tensorObj (𝒞 := instCategoryArrow) X ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))).left)
            Y.left)
          (NatTrans.app
            (map (curriedTensor C)
              (tensorObj (𝒞 := instCategoryArrow) X ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))).hom)
            Y.left)
          (map
            (obj (curriedTensor C)
              (tensorObj (𝒞 := instCategoryArrow) X ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))).left)
            Y.hom))
        (pushout.inr
          (NatTrans.app
            (map (curriedTensor C)
              (tensorObj (𝒞 := instCategoryArrow) X ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))).hom)
            Y.left)
          (map
            (obj (curriedTensor C)
              (tensorObj (𝒞 := instCategoryArrow) X ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))).left)
            Y.hom))
        (Arrow.Hom.left (Iso.hom (ρ_ X) ▷ Y))))

Tactic:
apply (initialIsInitial.ofIso ((initialIsoIsInitial ?_) ≪≫ (mulZero ?_).symm)).hom_ext

Premises used: CategoryTheory.Limits.IsInitial.hom_ext, CategoryTheory.Limits.initialIsInitial, CategoryTheory.Limits.initialIsoIsInitial, CategoryTheory.mulZero, CategoryTheory.Iso.trans, CategoryTheory.Iso.symm, CategoryTheory.Limits.IsInitial.ofIso