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)
⊢ 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

Tactic:
apply ((tensorRight _).map_isPushout (IsPushout.of_hasPushout _ _)).hom_ext

Goal state after:
case refine_2.h₀
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)
⊢ (tensorRight X₃.right).map
        (pushout.inl (((curriedTensor C).map X₁.hom).app X₂.left) (((curriedTensor C).obj X₁.left).map X₂.hom)) ≫
      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 =
    (tensorRight X₃.right).map
        (pushout.inl (((curriedTensor C).map X₁.hom).app X₂.left) (((curriedTensor C).obj X₁.left).map 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

case refine_2.h₁
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)
⊢ (tensorRight X₃.right).map
        (pushout.inr (((curriedTensor C).map X₁.hom).app X₂.left) (((curriedTensor C).obj X₁.left).map X₂.hom)) ≫
      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 =
    (tensorRight X₃.right).map
        (pushout.inr (((curriedTensor C).map X₁.hom).app X₂.left) (((curriedTensor C).obj X₁.left).map 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