-- 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_1 : (X □ Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst)))).left ⟶ X.left
refine_1₁ :
  Eq (α :=
    (X □ Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst)))).left ⟶
      (X □ Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst)))).left)
    (pushout.desc (IsInitial.to (IsInitial.ofIso initialIsInitial (Iso.symm (zeroMul initialIsInitial))) X.left)
          (Iso.hom (ρ_ X.left)) ⋯ ≫
        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))))))) :
      (X □ Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst)))).left ⟶
        (X □ Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst)))).left)
    (𝟙 (X □ Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst)))).left :
      (X □ Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst)))).left ⟶
        (X □ Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst)))).left)
refine_1₂ :
  Eq.{v + 1} (α := X.left ⟶ X.left)
    (CategoryStruct.comp (Y :=
      (X □ Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst)))).left)
      (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))))))) :
        X.left ⟶ (X □ Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst)))).left)
      (pushout.desc (IsInitial.to (IsInitial.ofIso initialIsInitial (Iso.symm (zeroMul initialIsInitial))) X.left)
          (Iso.hom (ρ_ X.left)) ⋯ :
        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)))))) ⟶
          X.left))
    (𝟙 X.left)
⊢ (X □ Arrow.mk (X := initial.{v, u} C) (initial.to (tensorUnit.{v, u} C (𝒞 := inst)))).left ≅ X.left

Tactic:
refine Iso.mk ?_ ((ρ_ X.left).inv ≫ pushout.inr _ _) ?_ ?_

Premises used: CategoryTheory.MonoidalCategoryStruct.rightUnitor, CategoryTheory.Arrow.left, CategoryTheory.Iso.mk, CategoryTheory.CategoryStruct.comp, CategoryTheory.Iso.inv, CategoryTheory.Limits.pushout.inr