-- Module: Mathlib.CategoryTheory.Monoidal.PushoutProduct
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : CartesianMonoidalCategory.{v, u} C
inst_3 : MonoidalClosed.{v, u} C
inst_4 : HasInitial.{v, u} C
X : Arrow.{v, u} C
refine_2 :
  CategoryStruct.comp (Y :=
      pushout (X :=
        obj.{v, v, u, u} (obj (curriedTensor C) X.left)
          (Arrow.left.{v, u} (Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst))))))
        (NatTrans.app (map (curriedTensor C) X.hom)
          (Arrow.left.{v, u} (Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst))))))
        (map (obj (curriedTensor C) X.left)
          (Arrow.hom (Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst)))))))
      (pushout.inl
          (NatTrans.app (map (curriedTensor C) X.hom)
            (Arrow.left.{v, u} (Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst))))))
          (map (obj (curriedTensor C) X.left)
            (Arrow.hom (Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst)))))) :
        obj.{v, v, u, u} (obj (curriedTensor C) X.right)
            (Arrow.left.{v, u} (Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst))))) ⟶
          pushout (X :=
            obj.{v, v, u, u} (obj (curriedTensor C) X.left)
              (Arrow.left.{v, u} (Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst))))))
            (NatTrans.app (map (curriedTensor C) X.hom)
              (Arrow.left.{v, u} (Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst))))))
            (map (obj (curriedTensor C) X.left)
              (Arrow.hom (Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst)))))))
      (Iso.hom
            {
              hom :=
                pushout.desc
                  (IsInitial.to (IsInitial.ofIso initialIsInitial (Iso.symm (zeroMul initialIsInitial))) X.left)
                  (Iso.hom (ρ_ X.left)) ⋯,
              inv :=
                CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) X.left (tensorUnit.{v, u} C (𝒞 := inst)))
                  (Iso.inv (ρ_ X.left))
                  (pushout.inr
                    (NatTrans.app (map (curriedTensor C) X.hom)
                      (Arrow.left.{v, u}
                        (Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst))))))
                    (map (obj (curriedTensor C) X.left)
                      (Arrow.hom (Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst))))))),
              hom_inv_id := ⋯, inv_hom_id := ⋯ } ≫
          X.hom :
        (X □ Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst)))).left ⟶ X.right) =
    pushout.inl
        (NatTrans.app (map (curriedTensor C) X.hom)
          (Arrow.left.{v, u} (Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst))))))
        (map (obj (curriedTensor C) X.left)
          (Arrow.hom (Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst)))))) ≫
      (X □ Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst)))).hom ≫ Iso.hom (ρ_ X.right)
⊢ Iso.hom
        {
          hom :=
            pushout.desc (IsInitial.to (IsInitial.ofIso initialIsInitial (Iso.symm (zeroMul initialIsInitial))) X.left)
              (Iso.hom (ρ_ X.left)) ⋯,
          inv :=
            CategoryStruct.comp (Y := tensorObj.{v, u} (𝒞 := inst) X.left (tensorUnit.{v, u} C (𝒞 := inst)))
              (Iso.inv (ρ_ X.left))
              (pushout.inr
                (NatTrans.app (map (curriedTensor C) X.hom)
                  (Arrow.left.{v, u} (Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst))))))
                (map (obj (curriedTensor C) X.left)
                  (Arrow.hom (Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst))))))),
          hom_inv_id := ⋯, inv_hom_id := ⋯ } ≫
      X.hom =
    (X □ Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst)))).hom ≫ Iso.hom (ρ_ X.right)

Tactic:
refine pushout.hom_ext ?_ (by simp)

Premises used: CategoryTheory.Limits.pushout.hom_ext