Module: Mathlib.CategoryTheory.Monoidal.Arrow

Goal state before:
pp: 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
X Y Z : Arrow C
⊢ (tensorLeft X.right).map
        (pushout.inl (((curriedTensor C).map Y.hom).app Z.left) (((curriedTensor C).obj Y.left).map Z.hom)) ≫
      pushout.inl (((curriedTensor C).map X.hom).app (Y ⊗ Z).left) (((curriedTensor C).obj X.left).map (Y ⊗ Z).hom) ≫
        Arrow.Hom.left ((α_ X Y Z).inv ≫ (braiding (X ⊗ Y) Z).hom ≫ (α_ Z X Y).inv) =
    (tensorLeft X.right).map
        (pushout.inl (((curriedTensor C).map Y.hom).app Z.left) (((curriedTensor C).obj Y.left).map Z.hom)) ≫
      pushout.inl (((curriedTensor C).map X.hom).app (Y ⊗ Z).left) (((curriedTensor C).obj X.left).map (Y ⊗ Z).hom) ≫
        Arrow.Hom.left (X ◁ (braiding Y Z).hom ≫ (α_ X Z Y).inv ≫ (braiding X Z).hom ▷ Y)

pp: 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
X Y Z : Arrow C
⊢ (tensorLeft X.right).map
        (pushout.inr (((curriedTensor C).map Y.hom).app Z.left) (((curriedTensor C).obj Y.left).map Z.hom)) ≫
      pushout.inl (((curriedTensor C).map X.hom).app (Y ⊗ Z).left) (((curriedTensor C).obj X.left).map (Y ⊗ Z).hom) ≫
        Arrow.Hom.left ((α_ X Y Z).inv ≫ (braiding (X ⊗ Y) Z).hom ≫ (α_ Z X Y).inv) =
    (tensorLeft X.right).map
        (pushout.inr (((curriedTensor C).map Y.hom).app Z.left) (((curriedTensor C).obj Y.left).map Z.hom)) ≫
      pushout.inl (((curriedTensor C).map X.hom).app (Y ⊗ Z).left) (((curriedTensor C).obj X.left).map (Y ⊗ Z).hom) ≫
        Arrow.Hom.left (X ◁ (braiding Y Z).hom ≫ (α_ X Z Y).inv ≫ (braiding X Z).hom ▷ Y)

Tactic:
<;>

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
X Y Z : Arrow C
⊢ (tensorLeft X.right).map
        (pushout.inl (((curriedTensor C).map Y.hom).app Z.left) (((curriedTensor C).obj Y.left).map Z.hom)) ≫
      pushout.inl (((curriedTensor C).map X.hom).app (Y ⊗ Z).left) (((curriedTensor C).obj X.left).map (Y ⊗ Z).hom) ≫
        Arrow.Hom.left ((α_ X Y Z).inv ≫ (braiding (X ⊗ Y) Z).hom ≫ (α_ Z X Y).inv) =
    (tensorLeft X.right).map
        (pushout.inl (((curriedTensor C).map Y.hom).app Z.left) (((curriedTensor C).obj Y.left).map Z.hom)) ≫
      pushout.inl (((curriedTensor C).map X.hom).app (Y ⊗ Z).left) (((curriedTensor C).obj X.left).map (Y ⊗ Z).hom) ≫
        Arrow.Hom.left (X ◁ (braiding Y Z).hom ≫ (α_ X Z Y).inv ≫ (braiding X Z).hom ▷ Y)

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
X Y Z : Arrow C
⊢ (tensorLeft X.right).map
        (pushout.inr (((curriedTensor C).map Y.hom).app Z.left) (((curriedTensor C).obj Y.left).map Z.hom)) ≫
      pushout.inl (((curriedTensor C).map X.hom).app (Y ⊗ Z).left) (((curriedTensor C).obj X.left).map (Y ⊗ Z).hom) ≫
        Arrow.Hom.left ((α_ X Y Z).inv ≫ (braiding (X ⊗ Y) Z).hom ≫ (α_ Z X Y).inv) =
    (tensorLeft X.right).map
        (pushout.inr (((curriedTensor C).map Y.hom).app Z.left) (((curriedTensor C).obj Y.left).map Z.hom)) ≫
      pushout.inl (((curriedTensor C).map X.hom).app (Y ⊗ Z).left) (((curriedTensor C).obj X.left).map (Y ⊗ Z).hom) ≫
        Arrow.Hom.left (X ◁ (braiding Y Z).hom ≫ (α_ X Z Y).inv ≫ (braiding X Z).hom ▷ Y)