awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.Arrow
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : HasInitial.{v, u} C
inst_3 : CartesianMonoidalCategory.{v, u} C
inst_4 : MonoidalClosed.{v, u} C
inst_5 : BraidedCategory.{v, u} C
W X Y Z : Arrow.{v, u} C
refine :
  CategoryStruct.comp (Y :=
      pushout (X :=
        obj.{v, v, u, u}
          (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) (tensorObj (𝒞 := instCategoryArrow) W X) Y).left)
          Z.left)
        (NatTrans.app
          (map (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) (tensorObj (𝒞 := instCategoryArrow) W X) Y).hom)
          Z.left)
        (map
          (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) (tensorObj (𝒞 := instCategoryArrow) W X) Y).left)
          Z.hom))
      (pushout.inr
        (NatTrans.app
          (map (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) (tensorObj (𝒞 := instCategoryArrow) W X) Y).hom)
          Z.left)
        (map
          (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) (tensorObj (𝒞 := instCategoryArrow) W X) Y).left)
          Z.hom))
      (Arrow.Hom.left
        (Iso.hom (α_ W X Y) ▷ Z ≫ Iso.hom (α_ W (tensorObj (𝒞 := instCategoryArrow) X Y) Z) ≫ W ◁ Iso.hom (α_ X Y Z))) =
    pushout.inr
        (NatTrans.app
          (map (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) (tensorObj (𝒞 := instCategoryArrow) W X) Y).hom)
          Z.left)
        (map
          (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) (tensorObj (𝒞 := instCategoryArrow) W X) Y).left)
          Z.hom) ≫
      Arrow.Hom.left
        (Iso.hom (α_ (tensorObj (𝒞 := instCategoryArrow) W X) Y Z) ≫
          Iso.hom (α_ W X (tensorObj (𝒞 := instCategoryArrow) Y Z)))
⊢ Iso.hom (α_ W X Y) ▷ Z ≫ Iso.hom (α_ W (tensorObj (𝒞 := instCategoryArrow) X Y) Z) ≫ W ◁ Iso.hom (α_ X Y Z) =
    Iso.hom (α_ (tensorObj (𝒞 := instCategoryArrow) W X) Y Z) ≫
      Iso.hom (α_ W X (tensorObj (𝒞 := instCategoryArrow) Y Z))

Tactic:
refine Arrow.hom_ext _ _ (pushout.hom_ext (by simp) ?_) (by simp)

Premises used: CategoryTheory.Arrow.hom_ext
-- Module: Mathlib.CategoryTheory.Monoidal.Arrow
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : HasInitial.{v, u} C
inst_3 : CartesianMonoidalCategory.{v, u} C
inst_4 : MonoidalClosed.{v, u} C
inst_5 : BraidedCategory.{v, u} C
W X Y Z : Arrow.{v, u} C
⊢ Eq (α :=
    obj.{v, v, u, u} (tensorRight Z.right)
        (obj.{v, v, u, u} (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) W X).right) Y.left) ⟶
      (tensorObj (𝒞 := instCategoryArrow) W
          (tensorObj (𝒞 := instCategoryArrow) X (tensorObj (𝒞 := instCategoryArrow) Y Z))).left)
    (CategoryStruct.comp (Y :=
      obj.{v, v, u, u} (tensorRight Z.right)
        (pushout (X := obj.{v, v, u, u} (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) W X).left) Y.left)
          (NatTrans.app (map (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) W X).hom) Y.left)
          (map (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) W X).left) Y.hom)))
      (map (tensorRight Z.right)
        (pushout.inl (NatTrans.app (map (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) W X).hom) Y.left)
          (map (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) W X).left) Y.hom)))
      (CategoryStruct.comp (Y :=
        pushout (X :=
          obj.{v, v, u, u}
            (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) (tensorObj (𝒞 := instCategoryArrow) W X) Y).left)
            Z.left)
          (NatTrans.app
            (map (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) (tensorObj (𝒞 := instCategoryArrow) W X) Y).hom)
            Z.left)
          (map
            (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) (tensorObj (𝒞 := instCategoryArrow) W X) Y).left)
            Z.hom))
        (pushout.inr
          (NatTrans.app
            (map (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) (tensorObj (𝒞 := instCategoryArrow) W X) Y).hom)
            Z.left)
          (map
            (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) (tensorObj (𝒞 := instCategoryArrow) W X) Y).left)
            Z.hom))
        (Arrow.Hom.left
          (Iso.hom (α_ W X Y) ▷ Z ≫
            Iso.hom (α_ W (tensorObj (𝒞 := instCategoryArrow) X Y) Z) ≫ W ◁ Iso.hom (α_ X Y Z)))))
    (map (tensorRight Z.right)
        (pushout.inl (NatTrans.app (map (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) W X).hom) Y.left)
          (map (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) W X).left) Y.hom)) ≫
      pushout.inr
          (NatTrans.app
            (map (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) (tensorObj (𝒞 := instCategoryArrow) W X) Y).hom)
            Z.left)
          (map
            (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) (tensorObj (𝒞 := instCategoryArrow) W X) Y).left)
            Z.hom) ≫
        Arrow.Hom.left
          (Iso.hom (α_ (tensorObj (𝒞 := instCategoryArrow) W X) Y Z) ≫
            Iso.hom (α_ W X (tensorObj (𝒞 := instCategoryArrow) Y Z))))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Arrow
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : HasInitial.{v, u} C
inst_3 : CartesianMonoidalCategory.{v, u} C
inst_4 : MonoidalClosed.{v, u} C
inst_5 : BraidedCategory.{v, u} C
X Y : Arrow.{v, u} C
⊢ Eq (α :=
    obj.{v, v, u, u}
        (obj (curriedTensor C)
          (tensorObj (𝒞 := instCategoryArrow) X ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))).right)
        Y.left ⟶
      (tensorObj (𝒞 := instCategoryArrow) X Y).left)
    (CategoryStruct.comp (Y :=
      pushout (X :=
        obj.{v, v, u, u}
          (obj (curriedTensor C)
            (tensorObj (𝒞 := instCategoryArrow) X ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))).left)
          Y.left)
        (NatTrans.app
          (map (curriedTensor C)
            (tensorObj (𝒞 := instCategoryArrow) X ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))).hom)
          Y.left)
        (map
          (obj (curriedTensor C)
            (tensorObj (𝒞 := instCategoryArrow) X ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))).left)
          Y.hom))
      (pushout.inl
        (NatTrans.app
          (map (curriedTensor C)
            (tensorObj (𝒞 := instCategoryArrow) X ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))).hom)
          Y.left)
        (map
          (obj (curriedTensor C)
            (tensorObj (𝒞 := instCategoryArrow) X ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))).left)
          Y.hom))
      (Arrow.Hom.left (Iso.hom (α_ X ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow)) Y) ≫ X ◁ Iso.hom (λ_ Y))))
    (CategoryStruct.comp (Y :=
      pushout (X :=
        obj.{v, v, u, u}
          (obj (curriedTensor C)
            (tensorObj (𝒞 := instCategoryArrow) X ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))).left)
          Y.left)
        (NatTrans.app
          (map (curriedTensor C)
            (tensorObj (𝒞 := instCategoryArrow) X ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))).hom)
          Y.left)
        (map
          (obj (curriedTensor C)
            (tensorObj (𝒞 := instCategoryArrow) X ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))).left)
          Y.hom))
      (pushout.inl
        (NatTrans.app
          (map (curriedTensor C)
            (tensorObj (𝒞 := instCategoryArrow) X ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))).hom)
          Y.left)
        (map
          (obj (curriedTensor C)
            (tensorObj (𝒞 := instCategoryArrow) X ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))).left)
          Y.hom))
      (Arrow.Hom.left (Iso.hom (ρ_ X) ▷ Y)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Arrow
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : HasInitial.{v, u} C
inst_3 : CartesianMonoidalCategory.{v, u} C
inst_4 : MonoidalClosed.{v, u} C
inst_5 : BraidedCategory.{v, u} C
X Y : Arrow.{v, u} C
⊢ Eq (α :=
    (tensorObj (𝒞 := instCategoryArrow)
          (tensorObj (𝒞 := instCategoryArrow) X ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))) Y).right ⟶
      (tensorObj (𝒞 := instCategoryArrow) X Y).right)
    (Arrow.Hom.right (Iso.hom (α_ X ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow)) Y) ≫ X ◁ Iso.hom (λ_ Y)))
    (Arrow.Hom.right (Iso.hom (ρ_ X) ▷ Y))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Arrow
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : HasInitial.{v, u} C
inst_3 : CartesianMonoidalCategory.{v, u} C
inst_4 : MonoidalClosed.{v, u} C
inst_5 : BraidedCategory.{v, u} C
X Y : Arrow.{v, u} C
refine :
  Eq (α :=
    obj.{v, v, u, u}
        (obj (curriedTensor C)
          (tensorObj (𝒞 := instCategoryArrow) X ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))).left)
        Y.right ⟶
      (tensorObj (𝒞 := instCategoryArrow) X Y).left)
    (CategoryStruct.comp (Y :=
      pushout (X :=
        obj.{v, v, u, u}
          (obj (curriedTensor C)
            (tensorObj (𝒞 := instCategoryArrow) X ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))).left)
          Y.left)
        (NatTrans.app
          (map (curriedTensor C)
            (tensorObj (𝒞 := instCategoryArrow) X ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))).hom)
          Y.left)
        (map
          (obj (curriedTensor C)
            (tensorObj (𝒞 := instCategoryArrow) X ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))).left)
          Y.hom))
      (pushout.inr
        (NatTrans.app
          (map (curriedTensor C)
            (tensorObj (𝒞 := instCategoryArrow) X ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))).hom)
          Y.left)
        (map
          (obj (curriedTensor C)
            (tensorObj (𝒞 := instCategoryArrow) X ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))).left)
          Y.hom))
      (Arrow.Hom.left (Iso.hom (α_ X ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow)) Y) ≫ X ◁ Iso.hom (λ_ Y))))
    (CategoryStruct.comp (Y :=
      pushout (X :=
        obj.{v, v, u, u}
          (obj (curriedTensor C)
            (tensorObj (𝒞 := instCategoryArrow) X ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))).left)
          Y.left)
        (NatTrans.app
          (map (curriedTensor C)
            (tensorObj (𝒞 := instCategoryArrow) X ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))).hom)
          Y.left)
        (map
          (obj (curriedTensor C)
            (tensorObj (𝒞 := instCategoryArrow) X ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))).left)
          Y.hom))
      (pushout.inr
        (NatTrans.app
          (map (curriedTensor C)
            (tensorObj (𝒞 := instCategoryArrow) X ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))).hom)
          Y.left)
        (map
          (obj (curriedTensor C)
            (tensorObj (𝒞 := instCategoryArrow) X ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))).left)
          Y.hom))
      (Arrow.Hom.left (Iso.hom (ρ_ X) ▷ Y)))
⊢ Eq (α :=
    tensorObj (𝒞 := instCategoryArrow)
        (tensorObj (𝒞 := instCategoryArrow) X ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))) Y ⟶
      tensorObj (𝒞 := instCategoryArrow) X Y)
    (Iso.hom (α_ X ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow)) Y) ≫ X ◁ Iso.hom (λ_ Y)) (Iso.hom (ρ_ X) ▷ Y)

Tactic:
refine Arrow.hom_ext _ _ (pushout.hom_ext (by simp) ?_) (by simp)

Premises used: CategoryTheory.Arrow.hom_ext
-- Module: Mathlib.CategoryTheory.Monoidal.Arrow
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : HasInitial.{v, u} C
inst_3 : CartesianMonoidalCategory.{v, u} C
inst_4 : MonoidalClosed.{v, u} C
inst_5 : BraidedCategory.{v, u} C
X Y : Arrow.{v, u} C
⊢ IsInitial.{v, u}
    (obj.{v, v, u, u} (obj (curriedTensor C) X.right)
      (Arrow.left.{v, u} ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))))

Tactic:
exact initialIsInitial.ofIso (zeroMul initialIsInitial).symm

Premises used: CategoryTheory.zeroMul, CategoryTheory.Limits.initialIsInitial, CategoryTheory.Iso.symm, CategoryTheory.Limits.IsInitial.ofIso
-- Module: Mathlib.CategoryTheory.Monoidal.Arrow
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : HasInitial.{v, u} C
inst_3 : CartesianMonoidalCategory.{v, u} C
inst_4 : MonoidalClosed.{v, u} C
inst_5 : BraidedCategory.{v, u} C
X Y Z : Arrow.{v, u} C
⊢ Eq (α :=
    obj.{v, v, u, u} (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X Y).right) Z.left ⟶
      (tensorObj (𝒞 := instCategoryArrow) Y (tensorObj (𝒞 := instCategoryArrow) Z X)).left)
    (CategoryStruct.comp (Y :=
      pushout (X := obj.{v, v, u, u} (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X Y).left) Z.left)
        (NatTrans.app (map (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X Y).hom) Z.left)
        (map (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X Y).left) Z.hom))
      (pushout.inl (NatTrans.app (map (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X Y).hom) Z.left)
        (map (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X Y).left) Z.hom))
      (Arrow.Hom.left
        (Iso.hom (α_ X Y Z) ≫ Iso.hom (braiding X (tensorObj (𝒞 := instCategoryArrow) Y Z)) ≫ Iso.hom (α_ Y Z X))))
    (CategoryStruct.comp (Y :=
      pushout (X := obj.{v, v, u, u} (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X Y).left) Z.left)
        (NatTrans.app (map (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X Y).hom) Z.left)
        (map (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X Y).left) Z.hom))
      (pushout.inl (NatTrans.app (map (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X Y).hom) Z.left)
        (map (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X Y).left) Z.hom))
      (Arrow.Hom.left (Iso.hom (braiding X Y) ▷ Z ≫ Iso.hom (α_ Y X Z) ≫ Y ◁ Iso.hom (braiding X Z))))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Arrow
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : HasInitial.{v, u} C
inst_3 : CartesianMonoidalCategory.{v, u} C
inst_4 : MonoidalClosed.{v, u} C
inst_5 : BraidedCategory.{v, u} C
X Y Z : Arrow.{v, u} C
⊢ Eq (α :=
    (tensorObj (𝒞 := instCategoryArrow) (tensorObj (𝒞 := instCategoryArrow) X Y) Z).right ⟶
      (tensorObj (𝒞 := instCategoryArrow) Y (tensorObj (𝒞 := instCategoryArrow) Z X)).right)
    (Arrow.Hom.right
      (Iso.hom (α_ X Y Z) ≫ Iso.hom (braiding X (tensorObj (𝒞 := instCategoryArrow) Y Z)) ≫ Iso.hom (α_ Y Z X)))
    (Arrow.Hom.right (Iso.hom (braiding X Y) ▷ Z ≫ Iso.hom (α_ Y X Z) ≫ Y ◁ Iso.hom (braiding X Z)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Arrow
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : HasInitial.{v, u} C
inst_3 : CartesianMonoidalCategory.{v, u} C
inst_4 : MonoidalClosed.{v, u} C
inst_5 : BraidedCategory.{v, u} C
X Y Z : Arrow.{v, u} C
refine :
  Eq (α :=
    obj.{v, v, u, u} (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X Y).left) Z.right ⟶
      (tensorObj (𝒞 := instCategoryArrow) Y (tensorObj (𝒞 := instCategoryArrow) Z X)).left)
    (CategoryStruct.comp (Y :=
      pushout (X := obj.{v, v, u, u} (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X Y).left) Z.left)
        (NatTrans.app (map (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X Y).hom) Z.left)
        (map (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X Y).left) Z.hom))
      (pushout.inr (NatTrans.app (map (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X Y).hom) Z.left)
        (map (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X Y).left) Z.hom))
      (Arrow.Hom.left
        (Iso.hom (α_ X Y Z) ≫ Iso.hom (braiding X (tensorObj (𝒞 := instCategoryArrow) Y Z)) ≫ Iso.hom (α_ Y Z X))))
    (CategoryStruct.comp (Y :=
      pushout (X := obj.{v, v, u, u} (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X Y).left) Z.left)
        (NatTrans.app (map (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X Y).hom) Z.left)
        (map (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X Y).left) Z.hom))
      (pushout.inr (NatTrans.app (map (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X Y).hom) Z.left)
        (map (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X Y).left) Z.hom))
      (Arrow.Hom.left (Iso.hom (braiding X Y) ▷ Z ≫ Iso.hom (α_ Y X Z) ≫ Y ◁ Iso.hom (braiding X Z))))
⊢ Eq (α :=
    tensorObj (𝒞 := instCategoryArrow) (tensorObj (𝒞 := instCategoryArrow) X Y) Z ⟶
      tensorObj (𝒞 := instCategoryArrow) Y (tensorObj (𝒞 := instCategoryArrow) Z X))
    (Iso.hom (α_ X Y Z) ≫ Iso.hom (braiding X (tensorObj (𝒞 := instCategoryArrow) Y Z)) ≫ Iso.hom (α_ Y Z X))
    (Iso.hom (braiding X Y) ▷ Z ≫ Iso.hom (α_ Y X Z) ≫ Y ◁ Iso.hom (braiding X Z))

Tactic:
refine Arrow.hom_ext _ _ (pushout.hom_ext (by simp) ?_) (by simp)

Premises used: CategoryTheory.Arrow.hom_ext
-- Module: Mathlib.CategoryTheory.Monoidal.Arrow
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : HasInitial.{v, u} C
inst_3 : CartesianMonoidalCategory.{v, u} C
inst_4 : MonoidalClosed.{v, u} C
inst_5 : BraidedCategory.{v, u} C
X Y Z : Arrow.{v, u} C
⊢ Eq (α :=
    obj.{v, v, u, u} (tensorRight Z.right) (obj.{v, v, u, u} (obj (curriedTensor C) X.right) Y.left) ⟶
      (tensorObj (𝒞 := instCategoryArrow) Y (tensorObj (𝒞 := instCategoryArrow) Z X)).left)
    (CategoryStruct.comp (Y :=
      obj.{v, v, u, u} (tensorRight Z.right)
        (pushout (X := obj.{v, v, u, u} (obj (curriedTensor C) X.left) Y.left)
          (NatTrans.app (map (curriedTensor C) X.hom) Y.left) (map (obj (curriedTensor C) X.left) Y.hom)))
      (map (tensorRight Z.right)
        (pushout.inl (NatTrans.app (map (curriedTensor C) X.hom) Y.left) (map (obj (curriedTensor C) X.left) Y.hom)))
      (CategoryStruct.comp (Y :=
        pushout (X := obj.{v, v, u, u} (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X Y).left) Z.left)
          (NatTrans.app (map (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X Y).hom) Z.left)
          (map (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X Y).left) Z.hom))
        (pushout.inr (NatTrans.app (map (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X Y).hom) Z.left)
          (map (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X Y).left) Z.hom))
        (Arrow.Hom.left
          (Iso.hom (α_ X Y Z) ≫ Iso.hom (braiding X (tensorObj (𝒞 := instCategoryArrow) Y Z)) ≫ Iso.hom (α_ Y Z X)))))
    (CategoryStruct.comp (Y :=
      obj.{v, v, u, u} (tensorRight Z.right)
        (pushout (X := obj.{v, v, u, u} (obj (curriedTensor C) X.left) Y.left)
          (NatTrans.app (map (curriedTensor C) X.hom) Y.left) (map (obj (curriedTensor C) X.left) Y.hom)))
      (map (tensorRight Z.right)
        (pushout.inl (NatTrans.app (map (curriedTensor C) X.hom) Y.left) (map (obj (curriedTensor C) X.left) Y.hom)))
      (CategoryStruct.comp (Y :=
        pushout (X := obj.{v, v, u, u} (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X Y).left) Z.left)
          (NatTrans.app (map (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X Y).hom) Z.left)
          (map (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X Y).left) Z.hom))
        (pushout.inr (NatTrans.app (map (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X Y).hom) Z.left)
          (map (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X Y).left) Z.hom))
        (Arrow.Hom.left (Iso.hom (braiding X Y) ▷ Z ≫ Iso.hom (α_ Y X Z) ≫ Y ◁ Iso.hom (braiding X Z)))))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Arrow
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : HasInitial.{v, u} C
inst_3 : CartesianMonoidalCategory.{v, u} C
inst_4 : MonoidalClosed.{v, u} C
inst_5 : BraidedCategory.{v, u} C
X Y Z : Arrow.{v, u} C
⊢ Eq (α :=
    obj.{v, v, u, u} (tensorRight Z.right) (obj.{v, v, u, u} (obj (curriedTensor C) X.left) Y.right) ⟶
      (tensorObj (𝒞 := instCategoryArrow) Y (tensorObj (𝒞 := instCategoryArrow) Z X)).left)
    (CategoryStruct.comp (Y :=
      obj.{v, v, u, u} (tensorRight Z.right)
        (pushout (X := obj.{v, v, u, u} (obj (curriedTensor C) X.left) Y.left)
          (NatTrans.app (map (curriedTensor C) X.hom) Y.left) (map (obj (curriedTensor C) X.left) Y.hom)))
      (map (tensorRight Z.right)
        (pushout.inr (NatTrans.app (map (curriedTensor C) X.hom) Y.left) (map (obj (curriedTensor C) X.left) Y.hom)))
      (CategoryStruct.comp (Y :=
        pushout (X := obj.{v, v, u, u} (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X Y).left) Z.left)
          (NatTrans.app (map (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X Y).hom) Z.left)
          (map (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X Y).left) Z.hom))
        (pushout.inr (NatTrans.app (map (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X Y).hom) Z.left)
          (map (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X Y).left) Z.hom))
        (Arrow.Hom.left
          (Iso.hom (α_ X Y Z) ≫ Iso.hom (braiding X (tensorObj (𝒞 := instCategoryArrow) Y Z)) ≫ Iso.hom (α_ Y Z X)))))
    (CategoryStruct.comp (Y :=
      obj.{v, v, u, u} (tensorRight Z.right)
        (pushout (X := obj.{v, v, u, u} (obj (curriedTensor C) X.left) Y.left)
          (NatTrans.app (map (curriedTensor C) X.hom) Y.left) (map (obj (curriedTensor C) X.left) Y.hom)))
      (map (tensorRight Z.right)
        (pushout.inr (NatTrans.app (map (curriedTensor C) X.hom) Y.left) (map (obj (curriedTensor C) X.left) Y.hom)))
      (CategoryStruct.comp (Y :=
        pushout (X := obj.{v, v, u, u} (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X Y).left) Z.left)
          (NatTrans.app (map (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X Y).hom) Z.left)
          (map (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X Y).left) Z.hom))
        (pushout.inr (NatTrans.app (map (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X Y).hom) Z.left)
          (map (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X Y).left) Z.hom))
        (Arrow.Hom.left (Iso.hom (braiding X Y) ▷ Z ≫ Iso.hom (α_ Y X Z) ≫ Y ◁ Iso.hom (braiding X Z)))))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Arrow
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : HasPushouts.{v, u} C
inst_2 : HasInitial.{v, u} C
inst_3 : CartesianMonoidalCategory.{v, u} C
inst_4 : MonoidalClosed.{v, u} C
inst_5 : BraidedCategory.{v, u} C
X Y Z : Arrow.{v, u} C
⊢ Eq (α :=
    obj.{v, v, u, u} (obj (curriedTensor C) X.left) (tensorObj (𝒞 := instCategoryArrow) Y Z).right ⟶
      (tensorObj (𝒞 := instCategoryArrow) (tensorObj (𝒞 := instCategoryArrow) Z X) Y).left)
    (CategoryStruct.comp (Y :=
      pushout (X := obj.{v, v, u, u} (obj (curriedTensor C) X.left) (tensorObj (𝒞 := instCategoryArrow) Y Z).left)
        (NatTrans.app (map (curriedTensor C) X.hom) (tensorObj (𝒞 := instCategoryArrow) Y Z).left)
        (map (obj (curriedTensor C) X.left) (tensorObj (𝒞 := instCategoryArrow) Y Z).hom))
      (pushout.inr (NatTrans.app (map (curriedTensor C) X.hom) (tensorObj (𝒞 := instCategoryArrow) Y Z).left)
        (map (obj (curriedTensor C) X.left) (tensorObj (𝒞 := instCategoryArrow) Y Z).hom))
      (Arrow.Hom.left
        (Iso.inv (α_ X Y Z) ≫ Iso.hom (braiding (tensorObj (𝒞 := instCategoryArrow) X Y) Z) ≫ Iso.inv (α_ Z X Y))))
    (CategoryStruct.comp (Y :=
      pushout (X := obj.{v, v, u, u} (obj (curriedTensor C) X.left) (tensorObj (𝒞 := instCategoryArrow) Y Z).left)
        (NatTrans.app (map (curriedTensor C) X.hom) (tensorObj (𝒞 := instCategoryArrow) Y Z).left)
        (map (obj (curriedTensor C) X.left) (tensorObj (𝒞 := instCategoryArrow) Y Z).hom))
      (pushout.inr (NatTrans.app (map (curriedTensor C) X.hom) (tensorObj (𝒞 := instCategoryArrow) Y Z).left)
        (map (obj (curriedTensor C) X.left) (tensorObj (𝒞 := instCategoryArrow) Y Z).hom))
      (Arrow.Hom.left (X ◁ Iso.hom (braiding Y Z) ≫ Iso.inv (α_ X Z Y) ≫ Iso.hom (braiding X Z) ▷ Y)))

Tactic:
simp