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

Tactic:
apply ((tensorRight _ ⋙ tensorRight _).map_isPushout (IsPushout.of_hasPushout _ _)).hom_ext

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