-- 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
h₀ :
  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))))
h₁ :
  Eq (α :=
    obj.{v, v, u, u} (tensorRight Y.right)
        (obj.{v, v, u, u} (obj (curriedTensor C) X.left)
          (Arrow.right.{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.inr
          (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.inr
          (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))))
⊢ Eq (α :=
    obj.{v, v, u, u}
        (obj (curriedTensor C)
          (tensorObj (𝒞 := instCategoryArrow) X ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))).left)
        Y.right ⟶
      (tensorObj (𝒞 := instCategoryArrow) X Y).left)
    (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 :=
      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 ((tensorRight _).map_isPushout (IsPushout.of_hasPushout _ _)).hom_ext

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