Module: Mathlib.CategoryTheory.Monoidal.PushoutProduct

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

Tactic:
· exact pushout.desc ((α_ _ _ _).hom ≫ _ ◁ pushout.inl _ _ ≫ pushout.inl _ _)
        ((whiskerRightIso _ _).hom.left ≫
          pushout.desc (_ ◁ pushout.inr _ _ ≫ pushout.inl _ _) (pushout.inr _ _)
          (by simp [Limits.pushout.associator_naturality_left_condition]))
        (((tensorRight _).map_isPushout (IsPushout.of_hasPushout _ _)).hom_ext
          (by simp [Limits.pushout.whiskerLeft_condition_assoc, ← whisker_exchange_assoc,
            ← comp_whiskerRight_assoc])
          (by simp [← whisker_exchange_assoc, Limits.pushout.associator_naturality_left_condition,
            ← comp_whiskerRight_assoc]))

Goal state after:
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

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

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