Module: Mathlib.CategoryTheory.Monoidal.Arrow

Goal state before:
pp: C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasPushouts C
inst✝³ : HasInitial C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
W X Y Z : Arrow C
⊢ (tensorRight Z.right).map
        (pushout.inr (((curriedTensor C).map (W ⊗ X).hom).app Y.left)
          (((curriedTensor C).obj (W ⊗ X).left).map Y.hom)) ≫
      pushout.inr (((curriedTensor C).map ((W ⊗ X) ⊗ Y).hom).app Z.left)
          (((curriedTensor C).obj ((W ⊗ X) ⊗ Y).left).map Z.hom) ≫
        Arrow.Hom.left ((α_ W X Y).hom ▷ Z ≫ (α_ W (X ⊗ Y) Z).hom ≫ W ◁ (α_ X Y Z).hom) =
    (tensorRight Z.right).map
        (pushout.inr (((curriedTensor C).map (W ⊗ X).hom).app Y.left)
          (((curriedTensor C).obj (W ⊗ X).left).map Y.hom)) ≫
      pushout.inr (((curriedTensor C).map ((W ⊗ X) ⊗ Y).hom).app Z.left)
          (((curriedTensor C).obj ((W ⊗ X) ⊗ Y).left).map Z.hom) ≫
        Arrow.Hom.left ((α_ (W ⊗ X) Y Z).hom ≫ (α_ W X (Y ⊗ Z)).hom)

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

Goal state after:
case h₀
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasPushouts C
inst✝³ : HasInitial C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
W X Y Z : Arrow C
⊢ (tensorRight Y.right ⋙ tensorRight Z.right).map
        (pushout.inl (((curriedTensor C).map W.hom).app X.left) (((curriedTensor C).obj W.left).map X.hom)) ≫
      (tensorRight Z.right).map
          (pushout.inr (((curriedTensor C).map (W ⊗ X).hom).app Y.left)
            (((curriedTensor C).obj (W ⊗ X).left).map Y.hom)) ≫
        pushout.inr (((curriedTensor C).map ((W ⊗ X) ⊗ Y).hom).app Z.left)
            (((curriedTensor C).obj ((W ⊗ X) ⊗ Y).left).map Z.hom) ≫
          Arrow.Hom.left ((α_ W X Y).hom ▷ Z ≫ (α_ W (X ⊗ Y) Z).hom ≫ W ◁ (α_ X Y Z).hom) =
    (tensorRight Y.right ⋙ tensorRight Z.right).map
        (pushout.inl (((curriedTensor C).map W.hom).app X.left) (((curriedTensor C).obj W.left).map X.hom)) ≫
      (tensorRight Z.right).map
          (pushout.inr (((curriedTensor C).map (W ⊗ X).hom).app Y.left)
            (((curriedTensor C).obj (W ⊗ X).left).map Y.hom)) ≫
        pushout.inr (((curriedTensor C).map ((W ⊗ X) ⊗ Y).hom).app Z.left)
            (((curriedTensor C).obj ((W ⊗ X) ⊗ Y).left).map Z.hom) ≫
          Arrow.Hom.left ((α_ (W ⊗ X) Y Z).hom ≫ (α_ W X (Y ⊗ Z)).hom)

case h₁
C : Type u
inst✝⁵ : Category.{v, u} C
inst✝⁴ : HasPushouts C
inst✝³ : HasInitial C
inst✝² : CartesianMonoidalCategory C
inst✝¹ : MonoidalClosed C
inst✝ : BraidedCategory C
W X Y Z : Arrow C
⊢ (tensorRight Y.right ⋙ tensorRight Z.right).map
        (pushout.inr (((curriedTensor C).map W.hom).app X.left) (((curriedTensor C).obj W.left).map X.hom)) ≫
      (tensorRight Z.right).map
          (pushout.inr (((curriedTensor C).map (W ⊗ X).hom).app Y.left)
            (((curriedTensor C).obj (W ⊗ X).left).map Y.hom)) ≫
        pushout.inr (((curriedTensor C).map ((W ⊗ X) ⊗ Y).hom).app Z.left)
            (((curriedTensor C).obj ((W ⊗ X) ⊗ Y).left).map Z.hom) ≫
          Arrow.Hom.left ((α_ W X Y).hom ▷ Z ≫ (α_ W (X ⊗ Y) Z).hom ≫ W ◁ (α_ X Y Z).hom) =
    (tensorRight Y.right ⋙ tensorRight Z.right).map
        (pushout.inr (((curriedTensor C).map W.hom).app X.left) (((curriedTensor C).obj W.left).map X.hom)) ≫
      (tensorRight Z.right).map
          (pushout.inr (((curriedTensor C).map (W ⊗ X).hom).app Y.left)
            (((curriedTensor C).obj (W ⊗ X).left).map Y.hom)) ≫
        pushout.inr (((curriedTensor C).map ((W ⊗ X) ⊗ Y).hom).app Z.left)
            (((curriedTensor C).obj ((W ⊗ X) ⊗ Y).left).map Z.hom) ≫
          Arrow.Hom.left ((α_ (W ⊗ X) Y Z).hom ≫ (α_ W X (Y ⊗ Z)).hom)