-- 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 Z : Arrow.{v, u} C
h₀ :
  Eq (α :=
    obj.{v, v, u, u} (tensorLeft X.right) (obj.{v, v, u, u} (obj (curriedTensor C) Y.right) Z.left) ⟶
      (tensorObj (𝒞 := instCategoryArrow) (tensorObj (𝒞 := instCategoryArrow) Z X) Y).left)
    (map (tensorLeft X.right)
        (pushout.inl (NatTrans.app (map (curriedTensor C) Y.hom) Z.left) (map (obj (curriedTensor C) Y.left) Z.hom)) ≫
      CategoryStruct.comp (Y :=
        pushout (X := obj.{v, v, u, u} (obj (curriedTensor C) X.left) (tensorObj (𝒞 := instCategoryArrow) Y Z).left)
          (NatTrans.app (map (curriedTensor C) X.hom) (tensorObj (𝒞 := instCategoryArrow) Y Z).left)
          (map (obj (curriedTensor C) X.left) (tensorObj (𝒞 := instCategoryArrow) Y Z).hom))
        (pushout.inl (NatTrans.app (map (curriedTensor C) X.hom) (tensorObj (𝒞 := instCategoryArrow) Y Z).left)
          (map (obj (curriedTensor C) X.left) (tensorObj (𝒞 := instCategoryArrow) Y Z).hom))
        (Arrow.Hom.left
          (Iso.inv (α_ X Y Z) ≫ Iso.hom (braiding (tensorObj (𝒞 := instCategoryArrow) X Y) Z) ≫ Iso.inv (α_ Z X Y))))
    (map (tensorLeft X.right)
        (pushout.inl (NatTrans.app (map (curriedTensor C) Y.hom) Z.left) (map (obj (curriedTensor C) Y.left) Z.hom)) ≫
      CategoryStruct.comp (Y :=
        pushout (X := obj.{v, v, u, u} (obj (curriedTensor C) X.left) (tensorObj (𝒞 := instCategoryArrow) Y Z).left)
          (NatTrans.app (map (curriedTensor C) X.hom) (tensorObj (𝒞 := instCategoryArrow) Y Z).left)
          (map (obj (curriedTensor C) X.left) (tensorObj (𝒞 := instCategoryArrow) Y Z).hom))
        (pushout.inl (NatTrans.app (map (curriedTensor C) X.hom) (tensorObj (𝒞 := instCategoryArrow) Y Z).left)
          (map (obj (curriedTensor C) X.left) (tensorObj (𝒞 := instCategoryArrow) Y Z).hom))
        (Arrow.Hom.left (X ◁ Iso.hom (braiding Y Z) ≫ Iso.inv (α_ X Z Y) ≫ Iso.hom (braiding X Z) ▷ Y)))
h₁ :
  Eq (α :=
    obj.{v, v, u, u} (tensorLeft X.right) (obj.{v, v, u, u} (obj (curriedTensor C) Y.left) Z.right) ⟶
      (tensorObj (𝒞 := instCategoryArrow) (tensorObj (𝒞 := instCategoryArrow) Z X) Y).left)
    (map (tensorLeft X.right)
        (pushout.inr (NatTrans.app (map (curriedTensor C) Y.hom) Z.left) (map (obj (curriedTensor C) Y.left) Z.hom)) ≫
      CategoryStruct.comp (Y :=
        pushout (X := obj.{v, v, u, u} (obj (curriedTensor C) X.left) (tensorObj (𝒞 := instCategoryArrow) Y Z).left)
          (NatTrans.app (map (curriedTensor C) X.hom) (tensorObj (𝒞 := instCategoryArrow) Y Z).left)
          (map (obj (curriedTensor C) X.left) (tensorObj (𝒞 := instCategoryArrow) Y Z).hom))
        (pushout.inl (NatTrans.app (map (curriedTensor C) X.hom) (tensorObj (𝒞 := instCategoryArrow) Y Z).left)
          (map (obj (curriedTensor C) X.left) (tensorObj (𝒞 := instCategoryArrow) Y Z).hom))
        (Arrow.Hom.left
          (Iso.inv (α_ X Y Z) ≫ Iso.hom (braiding (tensorObj (𝒞 := instCategoryArrow) X Y) Z) ≫ Iso.inv (α_ Z X Y))))
    (map (tensorLeft X.right)
        (pushout.inr (NatTrans.app (map (curriedTensor C) Y.hom) Z.left) (map (obj (curriedTensor C) Y.left) Z.hom)) ≫
      CategoryStruct.comp (Y :=
        pushout (X := obj.{v, v, u, u} (obj (curriedTensor C) X.left) (tensorObj (𝒞 := instCategoryArrow) Y Z).left)
          (NatTrans.app (map (curriedTensor C) X.hom) (tensorObj (𝒞 := instCategoryArrow) Y Z).left)
          (map (obj (curriedTensor C) X.left) (tensorObj (𝒞 := instCategoryArrow) Y Z).hom))
        (pushout.inl (NatTrans.app (map (curriedTensor C) X.hom) (tensorObj (𝒞 := instCategoryArrow) Y Z).left)
          (map (obj (curriedTensor C) X.left) (tensorObj (𝒞 := instCategoryArrow) Y Z).hom))
        (Arrow.Hom.left (X ◁ Iso.hom (braiding Y Z) ≫ Iso.inv (α_ X Z Y) ≫ Iso.hom (braiding X Z) ▷ Y)))
⊢ Eq (α :=
    obj.{v, v, u, u} (obj (curriedTensor C) X.right) (tensorObj (𝒞 := instCategoryArrow) Y Z).left ⟶
      (tensorObj (𝒞 := instCategoryArrow) (tensorObj (𝒞 := instCategoryArrow) Z X) Y).left)
    (CategoryStruct.comp (Y :=
      pushout (X := obj.{v, v, u, u} (obj (curriedTensor C) X.left) (tensorObj (𝒞 := instCategoryArrow) Y Z).left)
        (NatTrans.app (map (curriedTensor C) X.hom) (tensorObj (𝒞 := instCategoryArrow) Y Z).left)
        (map (obj (curriedTensor C) X.left) (tensorObj (𝒞 := instCategoryArrow) Y Z).hom))
      (pushout.inl (NatTrans.app (map (curriedTensor C) X.hom) (tensorObj (𝒞 := instCategoryArrow) Y Z).left)
        (map (obj (curriedTensor C) X.left) (tensorObj (𝒞 := instCategoryArrow) Y Z).hom))
      (Arrow.Hom.left
        (Iso.inv (α_ X Y Z) ≫ Iso.hom (braiding (tensorObj (𝒞 := instCategoryArrow) X Y) Z) ≫ Iso.inv (α_ Z X Y))))
    (CategoryStruct.comp (Y :=
      pushout (X := obj.{v, v, u, u} (obj (curriedTensor C) X.left) (tensorObj (𝒞 := instCategoryArrow) Y Z).left)
        (NatTrans.app (map (curriedTensor C) X.hom) (tensorObj (𝒞 := instCategoryArrow) Y Z).left)
        (map (obj (curriedTensor C) X.left) (tensorObj (𝒞 := instCategoryArrow) Y Z).hom))
      (pushout.inl (NatTrans.app (map (curriedTensor C) X.hom) (tensorObj (𝒞 := instCategoryArrow) Y Z).left)
        (map (obj (curriedTensor C) X.left) (tensorObj (𝒞 := instCategoryArrow) Y Z).hom))
      (Arrow.Hom.left (X ◁ Iso.hom (braiding Y Z) ≫ Iso.inv (α_ X Z Y) ≫ Iso.hom (braiding X Z) ▷ Y)))

Tactic:
apply ((tensorLeft _).map_isPushout (IsPushout.of_hasPushout _ _)).hom_ext

Premises used: CategoryTheory.IsPushout.of_hasPushout, CategoryTheory.MonoidalCategory.tensorLeft, CategoryTheory.IsPushout.hom_ext, CategoryTheory.Functor.map_isPushout