-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.PushoutProduct (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : MonoidalCategory.{v, u} C
X₁ X₂ X₃ : Arrow.{v, u} C
W : C
inst_3 :
  PreservesColimit (span (X := tensorObj.{v, u} (𝒞 := inst) X₁.left X₂.left) (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom))
    (tensorRight X₃.left)
inst_4 :
  PreservesColimit (span (X := tensorObj.{v, u} (𝒞 := inst) X₁.left X₂.left) (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom))
    (tensorRight X₃.right)
inst_5 :
  PreservesColimit (span (X := tensorObj.{v, u} (𝒞 := inst) X₂.left X₃.left) (X₂.hom ▷ X₃.left) (X₂.left ◁ X₃.hom))
    (tensorLeft X₁.left)
inst_6 :
  PreservesColimit (span (X := tensorObj.{v, u} (𝒞 := inst) X₂.left X₃.left) (X₂.hom ▷ X₃.left) (X₂.left ◁ X₃.hom))
    (tensorLeft X₁.right)
refine_1 : ((X₁ □ X₂) □ X₃).left ⟶ (X₁ □ X₂ □ X₃).left
refine_1₁ : (X₁ □ X₂ □ X₃).left ⟶ ((X₁ □ X₂) □ X₃).left
refine_1₂ :
  pushout.desc
        (Iso.hom (α_ X₁.right X₂.right X₃.left) ≫
          X₁.right ◁
              pushout.inl (NatTrans.app (map (curriedTensor C) X₂.hom) X₃.left)
                (map (obj (curriedTensor C) X₂.left) X₃.hom) ≫
            pushout.inl (NatTrans.app (map (curriedTensor C) X₁.hom) (X₂ □ X₃).left)
              (map (obj (curriedTensor C) X₁.left) (X₂ □ X₃).hom))
        (Arrow.Hom.left (Iso.hom (whiskerRightIso X₁ X₂)) ≫
          pushout.desc
            (X₁.right ◁
                pushout.inr (NatTrans.app (map (curriedTensor C) X₂.hom) X₃.left)
                  (map (obj (curriedTensor C) X₂.left) X₃.hom) ≫
              pushout.inl (NatTrans.app (map (curriedTensor C) X₁.hom) (X₂ □ X₃).left)
                (map (obj (curriedTensor C) X₁.left) (X₂ □ X₃).hom))
            (pushout.inr (NatTrans.app (map (curriedTensor C) X₁.hom) (X₂ □ X₃).left)
              (map (obj (curriedTensor C) X₁.left) (X₂ □ X₃).hom))
            ⋯)
        ⋯ ≫
      pushout.desc
        (Arrow.Hom.left (Iso.hom (whiskerLeftIso X₂ X₃)) ≫
          pushout.desc
            (pushout.inl (NatTrans.app (map (curriedTensor C) (X₁ □ X₂).hom) X₃.left)
              (map (obj (curriedTensor C) (X₁ □ X₂).left) X₃.hom))
            (pushout.inl (NatTrans.app (map (curriedTensor C) X₁.hom) X₂.left)
                  (map (obj (curriedTensor C) X₁.left) X₂.hom) ▷
                X₃.right ≫
              pushout.inr (NatTrans.app (map (curriedTensor C) (X₁ □ X₂).hom) X₃.left)
                (map (obj (curriedTensor C) (X₁ □ X₂).left) X₃.hom))
            ⋯)
        (Iso.inv (α_ X₁.left X₂.right X₃.right) ≫
          pushout.inr (NatTrans.app (map (curriedTensor C) X₁.hom) X₂.left)
                (map (obj (curriedTensor C) X₁.left) X₂.hom) ▷
              X₃.right ≫
            pushout.inr (NatTrans.app (map (curriedTensor C) (X₁ □ X₂).hom) X₃.left)
              (map (obj (curriedTensor C) (X₁ □ X₂).left) X₃.hom))
        ⋯ =
    𝟙 ((X₁ □ X₂) □ X₃).left
⊢ ((X₁ □ X₂) □ X₃).left ≅ (X₁ □ X₂ □ X₃).left
have refine_1₃ : pushout.desc
      (Arrow.Hom.left (Iso.hom (whiskerLeftIso X₂ X₃)) ≫
        pushout.desc
          (pushout.inl (NatTrans.app (map (curriedTensor C) (X₁ □ X₂).hom) X₃.left)
            (map (obj (curriedTensor C) (X₁ □ X₂).left) X₃.hom))
          (pushout.inl (NatTrans.app (map (curriedTensor C) X₁.hom) X₂.left)
                (map (obj (curriedTensor C) X₁.left) X₂.hom) ▷
              X₃.right ≫
            pushout.inr (NatTrans.app (map (curriedTensor C) (X₁ □ X₂).hom) X₃.left)
              (map (obj (curriedTensor C) (X₁ □ X₂).left) X₃.hom))
          sorry)
      (Iso.inv (α_ X₁.left X₂.right X₃.right) ≫
        pushout.inr (NatTrans.app (map (curriedTensor C) X₁.hom) X₂.left) (map (obj (curriedTensor C) X₁.left) X₂.hom) ▷
            X₃.right ≫
          pushout.inr (NatTrans.app (map (curriedTensor C) (X₁ □ X₂).hom) X₃.left)
            (map (obj (curriedTensor C) (X₁ □ X₂).left) X₃.hom))
      sorry ≫
    pushout.desc
      (Iso.hom (α_ X₁.right X₂.right X₃.left) ≫
        X₁.right ◁
            pushout.inl (NatTrans.app (map (curriedTensor C) X₂.hom) X₃.left)
              (map (obj (curriedTensor C) X₂.left) X₃.hom) ≫
          pushout.inl (NatTrans.app (map (curriedTensor C) X₁.hom) (X₂ □ X₃).left)
            (map (obj (curriedTensor C) X₁.left) (X₂ □ X₃).hom))
      (Arrow.Hom.left (Iso.hom (whiskerRightIso X₁ X₂)) ≫
        pushout.desc
          (X₁.right ◁
              pushout.inr (NatTrans.app (map (curriedTensor C) X₂.hom) X₃.left)
                (map (obj (curriedTensor C) X₂.left) X₃.hom) ≫
            pushout.inl (NatTrans.app (map (curriedTensor C) X₁.hom) (X₂ □ X₃).left)
              (map (obj (curriedTensor C) X₁.left) (X₂ □ X₃).hom))
          (pushout.inr (NatTrans.app (map (curriedTensor C) X₁.hom) (X₂ □ X₃).left)
            (map (obj (curriedTensor C) X₁.left) (X₂ □ X₃).hom))
          sorry)
      sorry =
  𝟙 (X₁ □ X₂ □ X₃).left
Tactic: refine Iso.mk ?_ ?_ ?_ ?_