-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Arrow (goal)
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
⊢ 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))) =
    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)))
have apply : 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 _).map_isPushout (IsPushout.of_hasPushout _ _)).hom_ext (by simp)