Module: Mathlib.CategoryTheory.Monoidal.PushoutProduct

Goal state before:
pp: case refine_2
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasPushouts C
inst✝⁴ : MonoidalCategory C
X₁ X₂ X₃ : Arrow C
W : C
inst✝³ : PreservesColimit (span (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom)) (tensorRight X₃.left)
inst✝² : PreservesColimit (span (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom)) (tensorRight X₃.right)
inst✝¹ : PreservesColimit (span (X₂.hom ▷ X₃.left) (X₂.left ◁ X₃.hom)) (tensorLeft X₁.left)
inst✝ : PreservesColimit (span (X₂.hom ▷ X₃.left) (X₂.left ◁ X₃.hom)) (tensorLeft X₁.right)
⊢ {
          hom :=
            pushout.desc
              ((α_ X₁.right X₂.right X₃.left).hom ≫
                X₁.right ◁
                    pushout.inl (((curriedTensor C).map X₂.hom).app X₃.left)
                      (((curriedTensor C).obj X₂.left).map X₃.hom) ≫
                  pushout.inl (((curriedTensor C).map X₁.hom).app (X₂ □ X₃).left)
                    (((curriedTensor C).obj X₁.left).map (X₂ □ X₃).hom))
              (Arrow.Hom.left (whiskerRightIso X₁ X₂).hom ≫
                pushout.desc
                  (X₁.right ◁
                      pushout.inr (((curriedTensor C).map X₂.hom).app X₃.left)
                        (((curriedTensor C).obj X₂.left).map X₃.hom) ≫
                    pushout.inl (((curriedTensor C).map X₁.hom).app (X₂ □ X₃).left)
                      (((curriedTensor C).obj X₁.left).map (X₂ □ X₃).hom))
                  (pushout.inr (((curriedTensor C).map X₁.hom).app (X₂ □ X₃).left)
                    (((curriedTensor C).obj X₁.left).map (X₂ □ X₃).hom))
                  ⋯)
              ⋯,
          inv :=
            pushout.desc
              (Arrow.Hom.left (whiskerLeftIso X₂ X₃).hom ≫
                pushout.desc
                  (pushout.inl (((curriedTensor C).map (X₁ □ X₂).hom).app X₃.left)
                    (((curriedTensor C).obj (X₁ □ X₂).left).map X₃.hom))
                  (pushout.inl (((curriedTensor C).map X₁.hom).app X₂.left)
                        (((curriedTensor C).obj X₁.left).map X₂.hom) ▷
                      X₃.right ≫
                    pushout.inr (((curriedTensor C).map (X₁ □ X₂).hom).app X₃.left)
                      (((curriedTensor C).obj (X₁ □ X₂).left).map X₃.hom))
                  ⋯)
              ((α_ X₁.left X₂.right X₃.right).inv ≫
                pushout.inr (((curriedTensor C).map X₁.hom).app X₂.left) (((curriedTensor C).obj X₁.left).map X₂.hom) ▷
                    X₃.right ≫
                  pushout.inr (((curriedTensor C).map (X₁ □ X₂).hom).app X₃.left)
                    (((curriedTensor C).obj (X₁ □ X₂).left).map X₃.hom))
              ⋯,
          hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom ≫
      (X₁ □ X₂ □ X₃).hom =
    ((X₁ □ X₂) □ X₃).hom ≫ (α_ X₁.right X₂.right X₃.right).hom

Tactic:
apply pushout.hom_ext (by simp [← MonoidalCategory.whiskerLeft_comp])

Goal state after:
case refine_2
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasPushouts C
inst✝⁴ : MonoidalCategory C
X₁ X₂ X₃ : Arrow C
W : C
inst✝³ : PreservesColimit (span (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom)) (tensorRight X₃.left)
inst✝² : PreservesColimit (span (X₁.hom ▷ X₂.left) (X₁.left ◁ X₂.hom)) (tensorRight X₃.right)
inst✝¹ : PreservesColimit (span (X₂.hom ▷ X₃.left) (X₂.left ◁ X₃.hom)) (tensorLeft X₁.left)
inst✝ : PreservesColimit (span (X₂.hom ▷ X₃.left) (X₂.left ◁ X₃.hom)) (tensorLeft X₁.right)
⊢ pushout.inr (((curriedTensor C).map (X₁ □ X₂).hom).app X₃.left) (((curriedTensor C).obj (X₁ □ X₂).left).map X₃.hom) ≫
      {
            hom :=
              pushout.desc
                ((α_ X₁.right X₂.right X₃.left).hom ≫
                  X₁.right ◁
                      pushout.inl (((curriedTensor C).map X₂.hom).app X₃.left)
                        (((curriedTensor C).obj X₂.left).map X₃.hom) ≫
                    pushout.inl (((curriedTensor C).map X₁.hom).app (X₂ □ X₃).left)
                      (((curriedTensor C).obj X₁.left).map (X₂ □ X₃).hom))
                (Arrow.Hom.left (whiskerRightIso X₁ X₂).hom ≫
                  pushout.desc
                    (X₁.right ◁
                        pushout.inr (((curriedTensor C).map X₂.hom).app X₃.left)
                          (((curriedTensor C).obj X₂.left).map X₃.hom) ≫
                      pushout.inl (((curriedTensor C).map X₁.hom).app (X₂ □ X₃).left)
                        (((curriedTensor C).obj X₁.left).map (X₂ □ X₃).hom))
                    (pushout.inr (((curriedTensor C).map X₁.hom).app (X₂ □ X₃).left)
                      (((curriedTensor C).obj X₁.left).map (X₂ □ X₃).hom))
                    ⋯)
                ⋯,
            inv :=
              pushout.desc
                (Arrow.Hom.left (whiskerLeftIso X₂ X₃).hom ≫
                  pushout.desc
                    (pushout.inl (((curriedTensor C).map (X₁ □ X₂).hom).app X₃.left)
                      (((curriedTensor C).obj (X₁ □ X₂).left).map X₃.hom))
                    (pushout.inl (((curriedTensor C).map X₁.hom).app X₂.left)
                          (((curriedTensor C).obj X₁.left).map X₂.hom) ▷
                        X₃.right ≫
                      pushout.inr (((curriedTensor C).map (X₁ □ X₂).hom).app X₃.left)
                        (((curriedTensor C).obj (X₁ □ X₂).left).map X₃.hom))
                    ⋯)
                ((α_ X₁.left X₂.right X₃.right).inv ≫
                  pushout.inr (((curriedTensor C).map X₁.hom).app X₂.left)
                        (((curriedTensor C).obj X₁.left).map X₂.hom) ▷
                      X₃.right ≫
                    pushout.inr (((curriedTensor C).map (X₁ □ X₂).hom).app X₃.left)
                      (((curriedTensor C).obj (X₁ □ X₂).left).map X₃.hom))
                ⋯,
            hom_inv_id := ⋯, inv_hom_id := ⋯ }.hom ≫
        (X₁ □ X₂ □ X₃).hom =
    pushout.inr (((curriedTensor C).map (X₁ □ X₂).hom).app X₃.left)
        (((curriedTensor C).obj (X₁ □ X₂).left).map X₃.hom) ≫
      ((X₁ □ X₂) □ X₃).hom ≫ (α_ X₁.right X₂.right X₃.right).hom