Module: Mathlib.CategoryTheory.Monoidal.PushoutProduct

Goal state before:
pp: case refine_1.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)
⊢ (X₁ □ X₂ □ X₃).left ⟶ ((X₁ □ X₂) □ X₃).left

pp: case refine_1.refine_3
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.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))
            ⋯)
        ⋯ ≫
      ?refine_1.refine_2 =
    𝟙 ((X₁ □ X₂) □ X₃).left

pp: case refine_1.refine_4
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)
⊢ ?refine_1.refine_2 ≫
      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))
            ⋯)
        ⋯ =
    𝟙 (X₁ □ X₂ □ X₃).left

Tactic:
· exact pushout.desc ((whiskerLeftIso _ _).hom.left ≫
          pushout.desc (pushout.inl _ _) ((pushout.inl _ _ ▷ _) ≫ pushout.inr _ _)
          (by simp [Limits.pushout.associator_inv_naturality_right_condition]))
        ((α_ _ _ _).inv ≫ (pushout.inr _ _) ▷ _ ≫ pushout.inr _ _)
        (((tensorLeft _).map_isPushout (IsPushout.of_hasPushout _ _)).hom_ext
          (by simp [whisker_exchange_assoc,
            Limits.pushout.associator_inv_naturality_right_condition, ← whiskerLeft_comp_assoc])
          (by simp [whisker_exchange_assoc, Limits.pushout.condition_whiskerRight_assoc,
            ← whiskerLeft_comp_assoc]))

Goal state after:
case refine_1.refine_3
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.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))
            ⋯)
        ⋯ ≫
      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))
        ⋯ =
    𝟙 ((X₁ □ X₂) □ X₃).left

case refine_1.refine_4
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.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))
        ⋯ ≫
      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))
            ⋯)
        ⋯ =
    𝟙 (X₁ □ X₂ □ X₃).left