-- 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
X₁ X₂ X₃ Y₁ Y₂ Y₃ : Arrow.{v, u} C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
h₀ :
  Eq (α :=
    obj.{v, v, u, u} (tensorRight X₃.right) (obj.{v, v, u, u} (obj (curriedTensor C) X₁.right) X₂.left) ⟶
      (tensorObj (𝒞 := instCategoryArrow) Y₁ (tensorObj (𝒞 := instCategoryArrow) Y₂ Y₃)).left)
    (CategoryStruct.comp (Y :=
      obj.{v, v, u, u} (tensorRight X₃.right)
        (pushout (X := obj.{v, v, u, u} (obj (curriedTensor C) X₁.left) X₂.left)
          (NatTrans.app (map (curriedTensor C) X₁.hom) X₂.left) (map (obj (curriedTensor C) X₁.left) X₂.hom)))
      (map (tensorRight X₃.right)
        (pushout.inl (NatTrans.app (map (curriedTensor C) X₁.hom) X₂.left)
          (map (obj (curriedTensor C) X₁.left) X₂.hom)))
      (CategoryStruct.comp (Y :=
        pushout (X := obj.{v, v, u, u} (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X₁ X₂).left) X₃.left)
          (NatTrans.app (map (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X₁ X₂).hom) X₃.left)
          (map (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X₁ X₂).left) X₃.hom))
        (pushout.inr (NatTrans.app (map (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X₁ X₂).hom) X₃.left)
          (map (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X₁ X₂).left) X₃.hom))
        (Arrow.Hom.left (((f₁ ⊗ₘ f₂) ⊗ₘ f₃) ≫ Iso.hom (α_ Y₁ Y₂ Y₃)))))
    (CategoryStruct.comp (Y :=
      obj.{v, v, u, u} (tensorRight X₃.right)
        (pushout (X := obj.{v, v, u, u} (obj (curriedTensor C) X₁.left) X₂.left)
          (NatTrans.app (map (curriedTensor C) X₁.hom) X₂.left) (map (obj (curriedTensor C) X₁.left) X₂.hom)))
      (map (tensorRight X₃.right)
        (pushout.inl (NatTrans.app (map (curriedTensor C) X₁.hom) X₂.left)
          (map (obj (curriedTensor C) X₁.left) X₂.hom)))
      (CategoryStruct.comp (Y :=
        pushout (X := obj.{v, v, u, u} (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X₁ X₂).left) X₃.left)
          (NatTrans.app (map (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X₁ X₂).hom) X₃.left)
          (map (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X₁ X₂).left) X₃.hom))
        (pushout.inr (NatTrans.app (map (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X₁ X₂).hom) X₃.left)
          (map (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X₁ X₂).left) X₃.hom))
        (Arrow.Hom.left (Iso.hom (α_ X₁ X₂ X₃) ≫ (f₁ ⊗ₘ f₂ ⊗ₘ f₃)))))
⊢ Eq (α :=
    obj.{v, v, u, u} (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X₁ X₂).left) X₃.right ⟶
      (tensorObj (𝒞 := instCategoryArrow) Y₁ (tensorObj (𝒞 := instCategoryArrow) Y₂ Y₃)).left)
    (CategoryStruct.comp (Y :=
      pushout (X := obj.{v, v, u, u} (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X₁ X₂).left) X₃.left)
        (NatTrans.app (map (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X₁ X₂).hom) X₃.left)
        (map (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X₁ X₂).left) X₃.hom))
      (pushout.inr (NatTrans.app (map (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X₁ X₂).hom) X₃.left)
        (map (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X₁ X₂).left) X₃.hom))
      (Arrow.Hom.left (((f₁ ⊗ₘ f₂) ⊗ₘ f₃) ≫ Iso.hom (α_ Y₁ Y₂ Y₃))))
    (CategoryStruct.comp (Y :=
      pushout (X := obj.{v, v, u, u} (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X₁ X₂).left) X₃.left)
        (NatTrans.app (map (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X₁ X₂).hom) X₃.left)
        (map (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X₁ X₂).left) X₃.hom))
      (pushout.inr (NatTrans.app (map (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X₁ X₂).hom) X₃.left)
        (map (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X₁ X₂).left) X₃.hom))
      (Arrow.Hom.left (Iso.hom (α_ X₁ X₂ X₃) ≫ (f₁ ⊗ₘ f₂ ⊗ₘ f₃))))
have h₁ : Eq (α :=
  obj.{v, v, u, u} (tensorRight X₃.right) (obj.{v, v, u, u} (obj (curriedTensor C) X₁.left) X₂.right) ⟶
    (tensorObj (𝒞 := instCategoryArrow) Y₁ (tensorObj (𝒞 := instCategoryArrow) Y₂ Y₃)).left)
  (CategoryStruct.comp (Y :=
    obj.{v, v, u, u} (tensorRight X₃.right)
      (pushout (X := obj.{v, v, u, u} (obj (curriedTensor C) X₁.left) X₂.left)
        (NatTrans.app (map (curriedTensor C) X₁.hom) X₂.left) (map (obj (curriedTensor C) X₁.left) X₂.hom)))
    (map (tensorRight X₃.right)
      (pushout.inr (NatTrans.app (map (curriedTensor C) X₁.hom) X₂.left) (map (obj (curriedTensor C) X₁.left) X₂.hom)))
    (CategoryStruct.comp (Y :=
      pushout (X := obj.{v, v, u, u} (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X₁ X₂).left) X₃.left)
        (NatTrans.app (map (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X₁ X₂).hom) X₃.left)
        (map (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X₁ X₂).left) X₃.hom))
      (pushout.inr (NatTrans.app (map (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X₁ X₂).hom) X₃.left)
        (map (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X₁ X₂).left) X₃.hom))
      (Arrow.Hom.left (((f₁ ⊗ₘ f₂) ⊗ₘ f₃) ≫ Iso.hom (α_ Y₁ Y₂ Y₃)))))
  (CategoryStruct.comp (Y :=
    obj.{v, v, u, u} (tensorRight X₃.right)
      (pushout (X := obj.{v, v, u, u} (obj (curriedTensor C) X₁.left) X₂.left)
        (NatTrans.app (map (curriedTensor C) X₁.hom) X₂.left) (map (obj (curriedTensor C) X₁.left) X₂.hom)))
    (map (tensorRight X₃.right)
      (pushout.inr (NatTrans.app (map (curriedTensor C) X₁.hom) X₂.left) (map (obj (curriedTensor C) X₁.left) X₂.hom)))
    (CategoryStruct.comp (Y :=
      pushout (X := obj.{v, v, u, u} (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X₁ X₂).left) X₃.left)
        (NatTrans.app (map (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X₁ X₂).hom) X₃.left)
        (map (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X₁ X₂).left) X₃.hom))
      (pushout.inr (NatTrans.app (map (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X₁ X₂).hom) X₃.left)
        (map (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X₁ X₂).left) X₃.hom))
      (Arrow.Hom.left (Iso.hom (α_ X₁ X₂ X₃) ≫ (f₁ ⊗ₘ f₂ ⊗ₘ f₃)))))
Tactic: apply ((tensorRight _).map_isPushout (IsPushout.of_hasPushout _ _)).hom_ext