-- Module: Mathlib.CategoryTheory.Monoidal.PushoutProduct
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)
⊢ Eq (α :=
    obj.{v, v, u, u} (tensorRight X₃.left) (obj.{v, v, u, u} (obj (curriedTensor C) X₁.right) X₂.left) ⟶
      (X₁ □ X₂ □ X₃).left)
    (CategoryStruct.comp (Y :=
        obj.{v, v, u, u} (tensorRight X₃.left)
          (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₃.left)
          (pushout.inl (NatTrans.app (map (curriedTensor C) X₁.hom) X₂.left)
            (map (obj (curriedTensor C) X₁.left) X₂.hom)))
        (NatTrans.app (map (curriedTensor C) (X₁ □ X₂).hom) X₃.left ≫
          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)) :
      obj.{v, v, u, u} (tensorRight X₃.left) (obj.{v, v, u, u} (obj (curriedTensor C) X₁.right) X₂.left) ⟶
        (X₁ □ X₂ □ X₃).left)
    (CategoryStruct.comp (Y :=
        obj.{v, v, u, u} (tensorRight X₃.left)
          (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₃.left)
          (pushout.inl (NatTrans.app (map (curriedTensor C) X₁.hom) X₂.left)
            (map (obj (curriedTensor C) X₁.left) X₂.hom)))
        (map (obj (curriedTensor C) (X₁ □ X₂).left) 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))
              ⋯) :
      obj.{v, v, u, u} (tensorRight X₃.left) (obj.{v, v, u, u} (obj (curriedTensor C) X₁.right) X₂.left) ⟶
        (X₁ □ X₂ □ X₃).left)

Tactic:
simp [Limits.pushout.whiskerLeft_condition_assoc, ← whisker_exchange_assoc]

Premises used: CategoryTheory.MonoidalCategory.whisker_exchange_assoc, CategoryTheory.MonoidalCategory.Limits.pushout.whiskerLeft_condition_assoc