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
X₁ Y₁ Z₁ X₂ Y₂ Z₂ : Arrow.{v, u} C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
g₁ : Y₁ ⟶ Z₁
g₂ : Y₂ ⟶ Z₂
⊢ Eq (α := obj.{v, v, u, u} (obj (curriedTensor C) X₁.left) X₂.right ⟶ (tensorObj (𝒞 := instCategoryArrow) Z₁ Z₂).left)
    (CategoryStruct.comp (Y :=
      pushout (X := obj.{v, v, u, u} (obj (curriedTensor C) X₁.left) X₂.left)
        (NatTrans.app (map (curriedTensor C) X₁.hom) X₂.left) (map (obj (curriedTensor C) X₁.left) X₂.hom))
      (pushout.inr (NatTrans.app (map (curriedTensor C) X₁.hom) X₂.left) (map (obj (curriedTensor C) X₁.left) X₂.hom))
      (Arrow.Hom.left ((f₁ ⊗ₘ f₂) ≫ (g₁ ⊗ₘ g₂))))
    (CategoryStruct.comp (Y :=
      pushout (X := obj.{v, v, u, u} (obj (curriedTensor C) X₁.left) X₂.left)
        (NatTrans.app (map (curriedTensor C) X₁.hom) X₂.left) (map (obj (curriedTensor C) X₁.left) X₂.hom))
      (pushout.inr (NatTrans.app (map (curriedTensor C) X₁.hom) X₂.left) (map (obj (curriedTensor C) X₁.left) X₂.hom))
      (Arrow.Hom.left (f₁ ≫ g₁ ⊗ₘ f₂ ≫ g₂)))

Tactic:
simp [whisker_exchange_assoc]

Premises used: CategoryTheory.MonoidalCategory.whisker_exchange_assoc
-- 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₁ X₂ X₃ Y₁ Y₂ Y₃ : Arrow.{v, u} C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
⊢ Eq (α :=
    obj.{v, v, u, u} (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X₁ X₂).right) X₃.left ⟶
      (tensorObj (𝒞 := instCategoryArrow) Y₁ (tensorObj (𝒞 := instCategoryArrow) Y₂ Y₃)).left)
    (CategoryStruct.comp (Y :=
      pushout (X := obj.{v, v, u, u} (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X₁ X₂).left) X₃.left)
        (NatTrans.app (map (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X₁ X₂).hom) X₃.left)
        (map (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X₁ X₂).left) X₃.hom))
      (pushout.inl (NatTrans.app (map (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X₁ X₂).hom) X₃.left)
        (map (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X₁ X₂).left) X₃.hom))
      (Arrow.Hom.left (((f₁ ⊗ₘ f₂) ⊗ₘ f₃) ≫ Iso.hom (α_ Y₁ Y₂ Y₃))))
    (CategoryStruct.comp (Y :=
      pushout (X := obj.{v, v, u, u} (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X₁ X₂).left) X₃.left)
        (NatTrans.app (map (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X₁ X₂).hom) X₃.left)
        (map (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X₁ X₂).left) X₃.hom))
      (pushout.inl (NatTrans.app (map (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X₁ X₂).hom) X₃.left)
        (map (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X₁ X₂).left) X₃.hom))
      (Arrow.Hom.left (Iso.hom (α_ X₁ X₂ X₃) ≫ (f₁ ⊗ₘ f₂ ⊗ₘ f₃))))

Tactic:
simp [whisker_exchange_assoc]

Premises used: CategoryTheory.MonoidalCategory.whisker_exchange_assoc
-- 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₁ X₂ X₃ Y₁ Y₂ Y₃ : Arrow.{v, u} C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
⊢ Eq (α :=
    (tensorObj (𝒞 := instCategoryArrow) (tensorObj (𝒞 := instCategoryArrow) X₁ X₂) X₃).right ⟶
      (tensorObj (𝒞 := instCategoryArrow) Y₁ (tensorObj (𝒞 := instCategoryArrow) Y₂ Y₃)).right)
    (Arrow.Hom.right (((f₁ ⊗ₘ f₂) ⊗ₘ f₃) ≫ Iso.hom (α_ Y₁ Y₂ Y₃)))
    (Arrow.Hom.right (Iso.hom (α_ X₁ X₂ X₃) ≫ (f₁ ⊗ₘ f₂ ⊗ₘ f₃)))

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₁ X₂ X₃ Y₁ Y₂ Y₃ : Arrow.{v, u} C
f₁ : X₁ ⟶ Y₁
f₂ : X₂ ⟶ Y₂
f₃ : X₃ ⟶ Y₃
refine :
  Eq (α :=
    obj.{v, v, u, u} (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X₁ X₂).left) X₃.right ⟶
      (tensorObj (𝒞 := instCategoryArrow) Y₁ (tensorObj (𝒞 := instCategoryArrow) Y₂ Y₃)).left)
    (CategoryStruct.comp (Y :=
      pushout (X := obj.{v, v, u, u} (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X₁ X₂).left) X₃.left)
        (NatTrans.app (map (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X₁ X₂).hom) X₃.left)
        (map (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X₁ X₂).left) X₃.hom))
      (pushout.inr (NatTrans.app (map (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X₁ X₂).hom) X₃.left)
        (map (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X₁ X₂).left) X₃.hom))
      (Arrow.Hom.left (((f₁ ⊗ₘ f₂) ⊗ₘ f₃) ≫ Iso.hom (α_ Y₁ Y₂ Y₃))))
    (CategoryStruct.comp (Y :=
      pushout (X := obj.{v, v, u, u} (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X₁ X₂).left) X₃.left)
        (NatTrans.app (map (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X₁ X₂).hom) X₃.left)
        (map (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X₁ X₂).left) X₃.hom))
      (pushout.inr (NatTrans.app (map (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X₁ X₂).hom) X₃.left)
        (map (obj (curriedTensor C) (tensorObj (𝒞 := instCategoryArrow) X₁ X₂).left) X₃.hom))
      (Arrow.Hom.left (Iso.hom (α_ X₁ X₂ X₃) ≫ (f₁ ⊗ₘ f₂ ⊗ₘ f₃))))
⊢ Eq (α :=
    tensorObj (𝒞 := instCategoryArrow) (tensorObj (𝒞 := instCategoryArrow) X₁ X₂) X₃ ⟶
      tensorObj (𝒞 := instCategoryArrow) Y₁ (tensorObj (𝒞 := instCategoryArrow) Y₂ Y₃))
    (((f₁ ⊗ₘ f₂) ⊗ₘ f₃) ≫ Iso.hom (α_ Y₁ Y₂ Y₃)) (Iso.hom (α_ X₁ X₂ X₃) ≫ (f₁ ⊗ₘ f₂ ⊗ₘ f₃))

Tactic:
refine Arrow.hom_ext _ _ (pushout.hom_ext (by simp [whisker_exchange_assoc]) ?_) (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
f : X ⟶ Y
⊢ Eq (α :=
    obj.{v, v, u, u} (obj (curriedTensor C) (Arrow.right.{v, u} ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))))
        X.left ⟶
      Y.left)
    (CategoryStruct.comp (Y :=
      pushout (X :=
        obj.{v, v, u, u} (obj (curriedTensor C) (Arrow.left.{v, u} ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))))
          X.left)
        (NatTrans.app (map (curriedTensor C) (Arrow.hom ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow)))) X.left)
        (map (obj (curriedTensor C) (Arrow.left.{v, u} ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow)))) X.hom))
      (pushout.inl
        (NatTrans.app (map (curriedTensor C) (Arrow.hom ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow)))) X.left)
        (map (obj (curriedTensor C) (Arrow.left.{v, u} ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow)))) X.hom))
      (Arrow.Hom.left ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow) ◁ f ≫ Iso.hom (λ_ Y))))
    (CategoryStruct.comp (Y :=
      pushout (X :=
        obj.{v, v, u, u} (obj (curriedTensor C) (Arrow.left.{v, u} ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))))
          X.left)
        (NatTrans.app (map (curriedTensor C) (Arrow.hom ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow)))) X.left)
        (map (obj (curriedTensor C) (Arrow.left.{v, u} ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow)))) X.hom))
      (pushout.inl
        (NatTrans.app (map (curriedTensor C) (Arrow.hom ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow)))) X.left)
        (map (obj (curriedTensor C) (Arrow.left.{v, u} ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow)))) X.hom))
      (Arrow.Hom.left (Iso.hom (λ_ X) ≫ f)))

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
f : X ⟶ Y
⊢ Eq (α := (tensorObj (𝒞 := instCategoryArrow) ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow)) X).right ⟶ Y.right)
    (Arrow.Hom.right ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow) ◁ f ≫ Iso.hom (λ_ Y)))
    (Arrow.Hom.right (Iso.hom (λ_ X) ≫ f))

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
f : X ⟶ Y
refine :
  Eq (α :=
    obj.{v, v, u, u} (obj (curriedTensor C) (Arrow.left.{v, u} ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))))
        X.right ⟶
      Y.left)
    (CategoryStruct.comp (Y :=
      pushout (X :=
        obj.{v, v, u, u} (obj (curriedTensor C) (Arrow.left.{v, u} ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))))
          X.left)
        (NatTrans.app (map (curriedTensor C) (Arrow.hom ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow)))) X.left)
        (map (obj (curriedTensor C) (Arrow.left.{v, u} ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow)))) X.hom))
      (pushout.inr
        (NatTrans.app (map (curriedTensor C) (Arrow.hom ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow)))) X.left)
        (map (obj (curriedTensor C) (Arrow.left.{v, u} ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow)))) X.hom))
      (Arrow.Hom.left ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow) ◁ f ≫ Iso.hom (λ_ Y))))
    (CategoryStruct.comp (Y :=
      pushout (X :=
        obj.{v, v, u, u} (obj (curriedTensor C) (Arrow.left.{v, u} ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))))
          X.left)
        (NatTrans.app (map (curriedTensor C) (Arrow.hom ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow)))) X.left)
        (map (obj (curriedTensor C) (Arrow.left.{v, u} ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow)))) X.hom))
      (pushout.inr
        (NatTrans.app (map (curriedTensor C) (Arrow.hom ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow)))) X.left)
        (map (obj (curriedTensor C) (Arrow.left.{v, u} ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow)))) X.hom))
      (Arrow.Hom.left (Iso.hom (λ_ X) ≫ f)))
⊢ Eq (α := tensorObj (𝒞 := instCategoryArrow) ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow)) X ⟶ Y)
    ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow) ◁ f ≫ Iso.hom (λ_ Y)) (Iso.hom (λ_ X) ≫ f)

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
f : X ⟶ Y
⊢ Eq (α :=
    obj.{v, v, u, u} (obj (curriedTensor C) (Arrow.left.{v, u} ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))))
        X.right ⟶
      Y.left)
    (CategoryStruct.comp (Y :=
      pushout (X :=
        obj.{v, v, u, u} (obj (curriedTensor C) (Arrow.left.{v, u} ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))))
          X.left)
        (NatTrans.app (map (curriedTensor C) (Arrow.hom ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow)))) X.left)
        (map (obj (curriedTensor C) (Arrow.left.{v, u} ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow)))) X.hom))
      (pushout.inr
        (NatTrans.app (map (curriedTensor C) (Arrow.hom ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow)))) X.left)
        (map (obj (curriedTensor C) (Arrow.left.{v, u} ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow)))) X.hom))
      (Arrow.Hom.left ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow) ◁ f ≫ Iso.hom (λ_ Y))))
    (CategoryStruct.comp (Y :=
      pushout (X :=
        obj.{v, v, u, u} (obj (curriedTensor C) (Arrow.left.{v, u} ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))))
          X.left)
        (NatTrans.app (map (curriedTensor C) (Arrow.hom ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow)))) X.left)
        (map (obj (curriedTensor C) (Arrow.left.{v, u} ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow)))) X.hom))
      (pushout.inr
        (NatTrans.app (map (curriedTensor C) (Arrow.hom ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow)))) X.left)
        (map (obj (curriedTensor C) (Arrow.left.{v, u} ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow)))) X.hom))
      (Arrow.Hom.left (Iso.hom (λ_ X) ≫ f)))

Tactic:
apply (initialIsInitial.ofIso (mulZero initialIsInitial).symm).hom_ext

Premises used: CategoryTheory.Limits.IsInitial.hom_ext, CategoryTheory.Limits.initialIsInitial, CategoryTheory.mulZero, 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 : Arrow.{v, u} C
f : X ⟶ Y
⊢ Eq (α :=
    obj.{v, v, u, u} (obj (curriedTensor C) X.left)
        (Arrow.right.{v, u} ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))) ⟶
      Y.left)
    (CategoryStruct.comp (Y :=
      pushout (X :=
        obj.{v, v, u, u} (obj (curriedTensor C) X.left)
          (Arrow.left.{v, u} ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))))
        (NatTrans.app (map (curriedTensor C) X.hom)
          (Arrow.left.{v, u} ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))))
        (map (obj (curriedTensor C) X.left) (Arrow.hom ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow)))))
      (pushout.inr
        (NatTrans.app (map (curriedTensor C) X.hom)
          (Arrow.left.{v, u} ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))))
        (map (obj (curriedTensor C) X.left) (Arrow.hom ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow)))))
      (Arrow.Hom.left (f ▷ (𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow) ≫ Iso.hom (ρ_ Y))))
    (CategoryStruct.comp (Y :=
      pushout (X :=
        obj.{v, v, u, u} (obj (curriedTensor C) X.left)
          (Arrow.left.{v, u} ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))))
        (NatTrans.app (map (curriedTensor C) X.hom)
          (Arrow.left.{v, u} ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))))
        (map (obj (curriedTensor C) X.left) (Arrow.hom ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow)))))
      (pushout.inr
        (NatTrans.app (map (curriedTensor C) X.hom)
          (Arrow.left.{v, u} ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))))
        (map (obj (curriedTensor C) X.left) (Arrow.hom ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow)))))
      (Arrow.Hom.left (Iso.hom (ρ_ X) ≫ f)))

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
f : X ⟶ Y
⊢ Eq (α := (tensorObj (𝒞 := instCategoryArrow) X ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))).right ⟶ Y.right)
    (Arrow.Hom.right (f ▷ (𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow) ≫ Iso.hom (ρ_ Y)))
    (Arrow.Hom.right (Iso.hom (ρ_ X) ≫ f))

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
f : X ⟶ Y
refine :
  Eq (α :=
    obj.{v, v, u, u} (obj (curriedTensor C) X.right)
        (Arrow.left.{v, u} ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))) ⟶
      Y.left)
    (CategoryStruct.comp (Y :=
      pushout (X :=
        obj.{v, v, u, u} (obj (curriedTensor C) X.left)
          (Arrow.left.{v, u} ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))))
        (NatTrans.app (map (curriedTensor C) X.hom)
          (Arrow.left.{v, u} ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))))
        (map (obj (curriedTensor C) X.left) (Arrow.hom ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow)))))
      (pushout.inl
        (NatTrans.app (map (curriedTensor C) X.hom)
          (Arrow.left.{v, u} ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))))
        (map (obj (curriedTensor C) X.left) (Arrow.hom ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow)))))
      (Arrow.Hom.left (f ▷ (𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow) ≫ Iso.hom (ρ_ Y))))
    (CategoryStruct.comp (Y :=
      pushout (X :=
        obj.{v, v, u, u} (obj (curriedTensor C) X.left)
          (Arrow.left.{v, u} ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))))
        (NatTrans.app (map (curriedTensor C) X.hom)
          (Arrow.left.{v, u} ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))))
        (map (obj (curriedTensor C) X.left) (Arrow.hom ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow)))))
      (pushout.inl
        (NatTrans.app (map (curriedTensor C) X.hom)
          (Arrow.left.{v, u} ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))))
        (map (obj (curriedTensor C) X.left) (Arrow.hom ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow)))))
      (Arrow.Hom.left (Iso.hom (ρ_ X) ≫ f)))
⊢ Eq (α := tensorObj (𝒞 := instCategoryArrow) X ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow)) ⟶ Y)
    (f ▷ (𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow) ≫ Iso.hom (ρ_ Y)) (Iso.hom (ρ_ X) ≫ f)

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
f : X ⟶ Y
⊢ Eq (α :=
    obj.{v, v, u, u} (obj (curriedTensor C) X.right)
        (Arrow.left.{v, u} ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))) ⟶
      Y.left)
    (CategoryStruct.comp (Y :=
      pushout (X :=
        obj.{v, v, u, u} (obj (curriedTensor C) X.left)
          (Arrow.left.{v, u} ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))))
        (NatTrans.app (map (curriedTensor C) X.hom)
          (Arrow.left.{v, u} ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))))
        (map (obj (curriedTensor C) X.left) (Arrow.hom ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow)))))
      (pushout.inl
        (NatTrans.app (map (curriedTensor C) X.hom)
          (Arrow.left.{v, u} ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))))
        (map (obj (curriedTensor C) X.left) (Arrow.hom ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow)))))
      (Arrow.Hom.left (f ▷ (𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow) ≫ Iso.hom (ρ_ Y))))
    (CategoryStruct.comp (Y :=
      pushout (X :=
        obj.{v, v, u, u} (obj (curriedTensor C) X.left)
          (Arrow.left.{v, u} ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))))
        (NatTrans.app (map (curriedTensor C) X.hom)
          (Arrow.left.{v, u} ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))))
        (map (obj (curriedTensor C) X.left) (Arrow.hom ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow)))))
      (pushout.inl
        (NatTrans.app (map (curriedTensor C) X.hom)
          (Arrow.left.{v, u} ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow))))
        (map (obj (curriedTensor C) X.left) (Arrow.hom ((𝟙_ (Arrow.{v, u} C)) (𝒞 := instCategoryArrow)))))
      (Arrow.Hom.left (Iso.hom (ρ_ X) ≫ f)))

Tactic:
apply (initialIsInitial.ofIso (zeroMul initialIsInitial).symm).hom_ext

Premises used: CategoryTheory.Limits.IsInitial.hom_ext, 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
W X Y Z : Arrow.{v, u} C
⊢ 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.inl
        (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.inl
        (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
W X Y Z : Arrow.{v, u} C
⊢ Arrow.Hom.right
      (Iso.hom (α_ W X Y) ▷ Z ≫ Iso.hom (α_ W (tensorObj (𝒞 := instCategoryArrow) X Y) Z) ≫ W ◁ Iso.hom (α_ X Y Z)) =
    Arrow.Hom.right
      (Iso.hom (α_ (tensorObj (𝒞 := instCategoryArrow) W X) Y Z) ≫
        Iso.hom (α_ W X (tensorObj (𝒞 := instCategoryArrow) Y Z)))

Tactic:
simp