awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.Bimon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
M : Bimon.{v₁, u₁} C
rw :
  Eq (α := M.X.X ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) M.X.X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) M.X.X M.X.X)
      (Mon.Hom.hom Δ : M.X.X ⟶ (tensorObj (𝒞 := Mon.instCategory) M.X M.X).X) (M.X.X ◁ ε))
    (Iso.inv (ρ_ M.X.X))
rw₁ :
  Eq.{v₁ + 1} (α := M.X.X ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) M.X.X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) (Δ ≫ M.X.X ◁ ε)
    (Iso.inv (ρ_ M.X.X))
rw₂ rw₃ :
  Eq.{v₁ + 1} (α := M.X.X ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) M.X.X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (Iso.inv (ρ_ M.X.X)) (Iso.inv (ρ_ M.X.X))
⊢ Eq (α := M.X.X ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) M.X.X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) M.X.X M.X.X)
      (Mon.Hom.hom Δ : M.X.X ⟶ (tensorObj (𝒞 := Mon.instCategory) M.X M.X).X) (M.X.X ◁ Mon.Hom.hom ε))
    (Iso.inv (ρ_ M.X.X))

Tactic:
rw [← BimonObjAux_counit, ← BimonObjAux_comul, ComonObj.comul_counit]

Premises used: CategoryTheory.ComonObj.comul_counit, CategoryTheory.Bimon.BimonObjAux_counit, CategoryTheory.Bimon.BimonObjAux_comul
-- Module: Mathlib.CategoryTheory.Monoidal.Bimon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
M : Bimon.{v₁, u₁} C
simp_rw :
  Eq.{v₁ + 1} (α := M.X.X ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) M.X.X (tensorObj.{v₁, u₁} (𝒞 := inst) M.X.X M.X.X))
    (Δ ≫ M.X.X ◁ Δ) (Δ ≫ Δ ▷ M.X.X ≫ Iso.hom (α_ M.X.X M.X.X M.X.X))
⊢ Eq.{v₁ + 1} (α := M.X.X ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) M.X.X (tensorObj.{v₁, u₁} (𝒞 := inst) M.X.X M.X.X))
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) M.X.X M.X.X)
      (Mon.Hom.hom Δ : M.X.X ⟶ (tensorObj (𝒞 := Mon.instCategory) M.X M.X).X) (M.X.X ◁ Mon.Hom.hom Δ))
    (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) M.X.X M.X.X)
      (Mon.Hom.hom Δ : M.X.X ⟶ (tensorObj (𝒞 := Mon.instCategory) M.X M.X).X)
      (CategoryStruct.comp (Y := tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) M.X.X M.X.X) M.X.X)
        (Mon.Hom.hom Δ ▷ M.X.X :
          tensorObj.{v₁, u₁} (𝒞 := inst) M.X.X M.X.X ⟶
            tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) M.X.X M.X.X) M.X.X)
        (Iso.hom (α_ M.X.X M.X.X M.X.X) :
          tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) M.X.X M.X.X) M.X.X ⟶
            tensorObj.{v₁, u₁} (𝒞 := inst) M.X.X (tensorObj.{v₁, u₁} (𝒞 := inst) M.X.X M.X.X))))

Tactic:
simp_rw [← BimonObjAux_comul, ComonObj.comul_assoc]

Premises used: CategoryTheory.Bimon.BimonObjAux_comul, CategoryTheory.ComonObj.comul_assoc
-- Module: Mathlib.CategoryTheory.Monoidal.Bimon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
M : C
inst_3 : BimonObj M
⊢ Eq (α := tensorUnit.{v₁, u₁} C (𝒞 := inst) ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) M M) (η ≫ Δ)
    (Iso.inv (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ (η ⊗ₘ η))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Bimon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
M : C
inst_3 : BimonObj M
⊢ Eq (α := tensorObj.{v₁, u₁} (𝒞 := inst) M M ⟶ tensorUnit.{v₁, u₁} C (𝒞 := inst)) (μ ≫ ε)
    ((ε ⊗ₘ ε) ≫ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Bimon_
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
inst_2 : BraidedCategory.{v₁, u₁} C
M : C
inst_3 : BimonObj M
⊢ Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) M M ⟶ tensorObj.{v₁, u₁} (𝒞 := inst) M M)
    ((Δ ⊗ₘ Δ) ≫
      Iso.hom (α_ M M (tensorObj.{v₁, u₁} (𝒞 := inst) M M)) ≫
        M ◁ Iso.inv (α_ M M M) ≫
          M ◁ Iso.hom (β_ M M) ▷ M ≫
            M ◁ Iso.hom (α_ M M M) ≫ Iso.inv (α_ M M (tensorObj.{v₁, u₁} (𝒞 := inst) M M)) ≫ (μ ⊗ₘ μ))
    (μ ≫ Δ)

Tactic:
simp only [BimonObj.mul_comul, tensorμ, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.MonoidalCategory.tensorμ, CategoryTheory.BimonObj.mul_comul
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
X Y Z : C
apply :
  Iso.inv (α_ X Y Z) ≫ Iso.hom (β_ (tensorObj.{v, u} (𝒞 := inst) X Y) Z) =
    Iso.inv (α_ X Y Z) ≫
      Iso.hom (α_ X Y Z) ≫ X ◁ Iso.hom (β_ Y Z) ≫ Iso.inv (α_ X Z Y) ≫ Iso.hom (β_ X Z) ▷ Y ≫ Iso.hom (α_ Z X Y)
⊢ Iso.hom (β_ (tensorObj.{v, u} (𝒞 := inst) X Y) Z) =
    Iso.hom (α_ X Y Z) ≫ X ◁ Iso.hom (β_ Y Z) ≫ Iso.inv (α_ X Z Y) ≫ Iso.hom (β_ X Z) ▷ Y ≫ Iso.hom (α_ Z X Y)

Tactic:
apply (cancel_epi (α_ X Y Z).inv).1

Premises used: Iff.mp, CategoryTheory.MonoidalCategoryStruct.associator, CategoryTheory.cancel_epi, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
X Y Z : C
apply :
  (Iso.inv (α_ X Y Z) ≫ Iso.hom (β_ (tensorObj.{v, u} (𝒞 := inst) X Y) Z)) ≫ Iso.inv (α_ Z X Y) =
    (Iso.inv (α_ X Y Z) ≫
        Iso.hom (α_ X Y Z) ≫ X ◁ Iso.hom (β_ Y Z) ≫ Iso.inv (α_ X Z Y) ≫ Iso.hom (β_ X Z) ▷ Y ≫ Iso.hom (α_ Z X Y)) ≫
      Iso.inv (α_ Z X Y)
⊢ Iso.inv (α_ X Y Z) ≫ Iso.hom (β_ (tensorObj.{v, u} (𝒞 := inst) X Y) Z) =
    Iso.inv (α_ X Y Z) ≫
      Iso.hom (α_ X Y Z) ≫ X ◁ Iso.hom (β_ Y Z) ≫ Iso.inv (α_ X Z Y) ≫ Iso.hom (β_ X Z) ▷ Y ≫ Iso.hom (α_ Z X Y)

Tactic:
apply (cancel_mono (α_ Z X Y).inv).1

Premises used: CategoryTheory.cancel_mono, Iff.mp, CategoryTheory.MonoidalCategoryStruct.associator, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
X Y Z : C
⊢ (Iso.inv (α_ X Y Z) ≫ Iso.hom (β_ (tensorObj.{v, u} (𝒞 := inst) X Y) Z)) ≫ Iso.inv (α_ Z X Y) =
    (Iso.inv (α_ X Y Z) ≫
        Iso.hom (α_ X Y Z) ≫ X ◁ Iso.hom (β_ Y Z) ≫ Iso.inv (α_ X Z Y) ≫ Iso.hom (β_ X Z) ▷ Y ≫ Iso.hom (α_ Z X Y)) ≫
      Iso.inv (α_ Z X Y)

Tactic:
simp [hexagon_reverse]

Premises used: CategoryTheory.BraidedCategory.hexagon_reverse
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
X Y Z : C
apply :
  Eq.{v + 1} (α :=
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) X Y) Z ⟶
      tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Y Z) X)
    (Iso.hom (α_ X Y Z) ≫ Iso.hom (β_ X (tensorObj.{v, u} (𝒞 := inst) Y Z)))
    (Iso.hom (α_ X Y Z) ≫
      Iso.inv (α_ X Y Z) ≫ Iso.hom (β_ X Y) ▷ Z ≫ Iso.hom (α_ Y X Z) ≫ Y ◁ Iso.hom (β_ X Z) ≫ Iso.inv (α_ Y Z X))
⊢ Eq.{v + 1} (α :=
    tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z) ⟶
      tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Y Z) X)
    (Iso.hom (β_ X (tensorObj.{v, u} (𝒞 := inst) Y Z)))
    (Iso.inv (α_ X Y Z) ≫ Iso.hom (β_ X Y) ▷ Z ≫ Iso.hom (α_ Y X Z) ≫ Y ◁ Iso.hom (β_ X Z) ≫ Iso.inv (α_ Y Z X))

Tactic:
apply (cancel_epi (α_ X Y Z).hom).1

Premises used: Iff.mp, CategoryTheory.MonoidalCategoryStruct.associator, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
X Y Z : C
apply :
  Eq.{v + 1} (α :=
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) X Y) Z ⟶
      tensorObj.{v, u} (𝒞 := inst) Y (tensorObj.{v, u} (𝒞 := inst) Z X))
    ((Iso.hom (α_ X Y Z) ≫ Iso.hom (β_ X (tensorObj.{v, u} (𝒞 := inst) Y Z))) ≫ Iso.hom (α_ Y Z X))
    ((Iso.hom (α_ X Y Z) ≫
        Iso.inv (α_ X Y Z) ≫ Iso.hom (β_ X Y) ▷ Z ≫ Iso.hom (α_ Y X Z) ≫ Y ◁ Iso.hom (β_ X Z) ≫ Iso.inv (α_ Y Z X)) ≫
      Iso.hom (α_ Y Z X))
⊢ Eq.{v + 1} (α :=
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) X Y) Z ⟶
      tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Y Z) X)
    (Iso.hom (α_ X Y Z) ≫ Iso.hom (β_ X (tensorObj.{v, u} (𝒞 := inst) Y Z)))
    (Iso.hom (α_ X Y Z) ≫
      Iso.inv (α_ X Y Z) ≫ Iso.hom (β_ X Y) ▷ Z ≫ Iso.hom (α_ Y X Z) ≫ Y ◁ Iso.hom (β_ X Z) ≫ Iso.inv (α_ Y Z X))

Tactic:
apply (cancel_mono (α_ Y Z X).hom).1

Premises used: CategoryTheory.cancel_mono, Iff.mp, CategoryTheory.MonoidalCategoryStruct.associator, CategoryTheory.Iso.hom
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
X Y Z : C
⊢ Eq.{v + 1} (α :=
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) X Y) Z ⟶
      tensorObj.{v, u} (𝒞 := inst) Y (tensorObj.{v, u} (𝒞 := inst) Z X))
    ((Iso.hom (α_ X Y Z) ≫ Iso.hom (β_ X (tensorObj.{v, u} (𝒞 := inst) Y Z))) ≫ Iso.hom (α_ Y Z X))
    ((Iso.hom (α_ X Y Z) ≫
        Iso.inv (α_ X Y Z) ≫ Iso.hom (β_ X Y) ▷ Z ≫ Iso.hom (α_ Y X Z) ≫ Y ◁ Iso.hom (β_ X Z) ≫ Iso.inv (α_ Y Z X)) ≫
      Iso.hom (α_ Y Z X))

Tactic:
simp [hexagon_forward]

Premises used: CategoryTheory.BraidedCategory.hexagon_forward
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
X Y Z : C
⊢ inv (Iso.inv (β_ (tensorObj.{v, u} (𝒞 := inst) X Y) Z)) =
    inv (Iso.inv (α_ Z X Y) ≫ Iso.inv (β_ X Z) ▷ Y ≫ Iso.hom (α_ X Z Y) ≫ X ◁ Iso.inv (β_ Y Z) ≫ Iso.inv (α_ X Y Z))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
X Y Z : C
⊢ Eq.{v + 1} (α :=
    tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z) ⟶
      tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Y Z) X)
    (inv (Iso.inv (β_ X (tensorObj.{v, u} (𝒞 := inst) Y Z))))
    (inv (Iso.hom (α_ Y Z X) ≫ Y ◁ Iso.inv (β_ X Z) ≫ Iso.inv (α_ Y X Z) ≫ Iso.inv (β_ X Y) ▷ Z ≫ Iso.hom (α_ X Y Z)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
X X' Y Y' : C
f : X ⟶ Y
g : X' ⟶ Y'
rw :
  Eq (α := tensorObj.{v, u} (𝒞 := inst) X X' ⟶ tensorObj.{v, u} (𝒞 := inst) Y' Y) ((X ◁ g ≫ f ▷ Y') ≫ Iso.hom (β_ Y Y'))
    (Iso.hom (β_ X X') ≫ g ▷ X ≫ Y' ◁ f)
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) X X' ⟶ tensorObj.{v, u} (𝒞 := inst) Y' Y) ((f ⊗ₘ g) ≫ Iso.hom (β_ Y Y'))
    (Iso.hom (β_ X X') ≫ (g ⊗ₘ f))

Tactic:
rw [tensorHom_def' f g, tensorHom_def g f]

Premises used: CategoryTheory.MonoidalCategory.tensorHom_def, CategoryTheory.MonoidalCategory.tensorHom_def'
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
X X' Y Y' : C
f : X ⟶ Y
g : X' ⟶ Y'
simp_rw :
  Eq (α := tensorObj.{v, u} (𝒞 := inst) X X' ⟶ tensorObj.{v, u} (𝒞 := inst) Y' Y) (X ◁ g ≫ f ▷ Y' ≫ Iso.hom (β_ Y Y'))
    (Iso.hom (β_ X X') ≫ g ▷ X ≫ Y' ◁ f)
simp_rw₁ :
  Eq (α := tensorObj.{v, u} (𝒞 := inst) X X' ⟶ tensorObj.{v, u} (𝒞 := inst) Y' Y) (X ◁ g ≫ Iso.hom (β_ X Y') ≫ Y' ◁ f)
    (Iso.hom (β_ X X') ≫ g ▷ X ≫ Y' ◁ f)
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) X X' ⟶ tensorObj.{v, u} (𝒞 := inst) Y' Y) ((X ◁ g ≫ f ▷ Y') ≫ Iso.hom (β_ Y Y'))
    (Iso.hom (β_ X X') ≫ g ▷ X ≫ Y' ◁ f)

Tactic:
simp_rw [Category.assoc, braiding_naturality_left, braiding_naturality_right_assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.BraidedCategory.braiding_naturality_left, CategoryTheory.BraidedCategory.braiding_naturality_right_assoc
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
X Y Z : C
f : Y ⟶ Z
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) X Y ⟶ tensorObj.{v, u} (𝒞 := inst) Z X) (X ◁ f ≫ Iso.inv (β_ Z X))
    (Iso.inv (β_ Y X) ≫ f ▷ X)

Tactic:
CommSq.w <| .vert_inv <| .mk <| braiding_naturality_left f X

Premises used: CategoryTheory.CommSq.vert_inv, CategoryTheory.BraidedCategory.braiding_naturality_left, CategoryTheory.CommSq.mk, CategoryTheory.CommSq.w
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) X Z ⟶ tensorObj.{v, u} (𝒞 := inst) Z Y) (f ▷ Z ≫ Iso.inv (β_ Z Y))
    (Iso.inv (β_ Z X) ≫ Z ◁ f)

Tactic:
CommSq.w <| .vert_inv <| .mk <| braiding_naturality_right Z f

Premises used: CategoryTheory.BraidedCategory.braiding_naturality_right, CategoryTheory.CommSq.vert_inv, CategoryTheory.CommSq.mk, CategoryTheory.CommSq.w
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
X X' Y Y' : C
f : X ⟶ Y
g : X' ⟶ Y'
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) X X' ⟶ tensorObj.{v, u} (𝒞 := inst) Y' Y) ((f ⊗ₘ g) ≫ Iso.inv (β_ Y' Y))
    (Iso.inv (β_ X' X) ≫ (g ⊗ₘ f))

Tactic:
CommSq.w <| .vert_inv <| .mk <| braiding_naturality g f

Premises used: CategoryTheory.CommSq.vert_inv, CategoryTheory.BraidedCategory.braiding_naturality, CategoryTheory.CommSq.mk, CategoryTheory.CommSq.w
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
X Y Z : C
rw :
  Eq.{v + 1} (α :=
    tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z) ⟶
      tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Z Y) X)
    ((Iso.hom (β_ X (tensorObj.{v, u} (𝒞 := inst) Y Z)) ≫ Iso.hom (β_ Y Z) ▷ X ≫ Iso.hom (α_ Z Y X)) ≫
      Iso.inv (α_ Z Y X))
    ((X ◁ Iso.hom (β_ Y Z) ≫ Iso.inv (α_ X Z Y) ≫ Iso.hom (β_ X Z) ▷ Y ≫ Iso.hom (α_ Z X Y) ≫ Z ◁ Iso.hom (β_ X Y)) ≫
      Iso.inv (α_ Z Y X))
⊢ Eq.{v + 1} (α :=
    tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z) ⟶
      tensorObj.{v, u} (𝒞 := inst) Z (tensorObj.{v, u} (𝒞 := inst) Y X))
    (Iso.inv (α_ X Y Z) ≫
      Iso.hom (β_ X Y) ▷ Z ≫
        Iso.hom (α_ Y X Z) ≫ Y ◁ Iso.hom (β_ X Z) ≫ Iso.inv (α_ Y Z X) ≫ Iso.hom (β_ Y Z) ▷ X ≫ Iso.hom (α_ Z Y X))
    (X ◁ Iso.hom (β_ Y Z) ≫ Iso.inv (α_ X Z Y) ≫ Iso.hom (β_ X Z) ▷ Y ≫ Iso.hom (α_ Z X Y) ≫ Z ◁ Iso.hom (β_ X Y))

Tactic:
rw [← braiding_tensor_right_hom_assoc X Y Z, ← cancel_mono (α_ Z Y X).inv]

Premises used: CategoryTheory.BraidedCategory.braiding_tensor_right_hom_assoc, CategoryTheory.cancel_mono, CategoryTheory.MonoidalCategoryStruct.associator, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
X Y Z : C
rw :
  Eq.{v + 1} (α :=
    tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z) ⟶
      tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Z Y) X)
    (Iso.hom (β_ X (tensorObj.{v, u} (𝒞 := inst) Y Z)) ≫
      (Iso.hom (β_ Y Z) ▷ X ≫ Iso.hom (α_ Z Y X)) ≫ Iso.inv (α_ Z Y X))
    ((X ◁ Iso.hom (β_ Y Z) ≫ Iso.inv (α_ X Z Y) ≫ Iso.hom (β_ X Z) ▷ Y ≫ Iso.hom (α_ Z X Y) ≫ Z ◁ Iso.hom (β_ X Y)) ≫
      Iso.inv (α_ Z Y X))
⊢ Eq.{v + 1} (α :=
    tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z) ⟶
      tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Z Y) X)
    ((Iso.hom (β_ X (tensorObj.{v, u} (𝒞 := inst) Y Z)) ≫ Iso.hom (β_ Y Z) ▷ X ≫ Iso.hom (α_ Z Y X)) ≫
      Iso.inv (α_ Z Y X))
    ((X ◁ Iso.hom (β_ Y Z) ≫ Iso.inv (α_ X Z Y) ≫ Iso.hom (β_ X Z) ▷ Y ≫ Iso.hom (α_ Z X Y) ≫ Z ◁ Iso.hom (β_ X Y)) ≫
      Iso.inv (α_ Z Y X))

Tactic:
rw [assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
X Y Z : C
rw :
  Eq.{v + 1} (α :=
    tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z) ⟶
      tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Z Y) X)
    (Iso.hom (β_ X (tensorObj.{v, u} (𝒞 := inst) Y Z)) ≫ Iso.hom (β_ Y Z) ▷ X ≫ Iso.hom (α_ Z Y X) ≫ Iso.inv (α_ Z Y X))
    ((X ◁ Iso.hom (β_ Y Z) ≫ Iso.inv (α_ X Z Y) ≫ Iso.hom (β_ X Z) ▷ Y ≫ Iso.hom (α_ Z X Y) ≫ Z ◁ Iso.hom (β_ X Y)) ≫
      Iso.inv (α_ Z Y X))
⊢ Eq.{v + 1} (α :=
    tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z) ⟶
      tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Z Y) X)
    (Iso.hom (β_ X (tensorObj.{v, u} (𝒞 := inst) Y Z)) ≫
      (Iso.hom (β_ Y Z) ▷ X ≫ Iso.hom (α_ Z Y X)) ≫ Iso.inv (α_ Z Y X))
    ((X ◁ Iso.hom (β_ Y Z) ≫ Iso.inv (α_ X Z Y) ≫ Iso.hom (β_ X Z) ▷ Y ≫ Iso.hom (α_ Z X Y) ≫ Z ◁ Iso.hom (β_ X Y)) ≫
      Iso.inv (α_ Z Y X))

Tactic:
rw [assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
X Y Z : C
rw :
  Eq.{v + 1} (α :=
    tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z) ⟶
      tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Z Y) X)
    (Iso.hom (β_ X (tensorObj.{v, u} (𝒞 := inst) Y Z)) ≫ Iso.hom (β_ Y Z) ▷ X ≫ Iso.hom (α_ Z Y X) ≫ Iso.inv (α_ Z Y X))
    (X ◁ Iso.hom (β_ Y Z) ≫
      (Iso.inv (α_ X Z Y) ≫ Iso.hom (β_ X Z) ▷ Y ≫ Iso.hom (α_ Z X Y) ≫ Z ◁ Iso.hom (β_ X Y)) ≫ Iso.inv (α_ Z Y X))
⊢ Eq.{v + 1} (α :=
    tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z) ⟶
      tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Z Y) X)
    (Iso.hom (β_ X (tensorObj.{v, u} (𝒞 := inst) Y Z)) ≫ Iso.hom (β_ Y Z) ▷ X ≫ Iso.hom (α_ Z Y X) ≫ Iso.inv (α_ Z Y X))
    ((X ◁ Iso.hom (β_ Y Z) ≫ Iso.inv (α_ X Z Y) ≫ Iso.hom (β_ X Z) ▷ Y ≫ Iso.hom (α_ Z X Y) ≫ Z ◁ Iso.hom (β_ X Y)) ≫
      Iso.inv (α_ Z Y X))

Tactic:
rw [assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
X Y Z : C
rw :
  Eq.{v + 1} (α :=
    tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z) ⟶
      tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Z Y) X)
    (Iso.hom (β_ X (tensorObj.{v, u} (𝒞 := inst) Y Z)) ≫ Iso.hom (β_ Y Z) ▷ X ≫ Iso.hom (α_ Z Y X) ≫ Iso.inv (α_ Z Y X))
    (X ◁ Iso.hom (β_ Y Z) ≫
      Iso.inv (α_ X Z Y) ≫ (Iso.hom (β_ X Z) ▷ Y ≫ Iso.hom (α_ Z X Y) ≫ Z ◁ Iso.hom (β_ X Y)) ≫ Iso.inv (α_ Z Y X))
⊢ Eq.{v + 1} (α :=
    tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z) ⟶
      tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Z Y) X)
    (Iso.hom (β_ X (tensorObj.{v, u} (𝒞 := inst) Y Z)) ≫ Iso.hom (β_ Y Z) ▷ X ≫ Iso.hom (α_ Z Y X) ≫ Iso.inv (α_ Z Y X))
    (X ◁ Iso.hom (β_ Y Z) ≫
      (Iso.inv (α_ X Z Y) ≫ Iso.hom (β_ X Z) ▷ Y ≫ Iso.hom (α_ Z X Y) ≫ Z ◁ Iso.hom (β_ X Y)) ≫ Iso.inv (α_ Z Y X))

Tactic:
rw [assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
X Y Z : C
rw :
  Eq.{v + 1} (α :=
    tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z) ⟶
      tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Z Y) X)
    (Iso.hom (β_ X (tensorObj.{v, u} (𝒞 := inst) Y Z)) ≫ Iso.hom (β_ Y Z) ▷ X ≫ Iso.hom (α_ Z Y X) ≫ Iso.inv (α_ Z Y X))
    (X ◁ Iso.hom (β_ Y Z) ≫
      Iso.inv (α_ X Z Y) ≫ Iso.hom (β_ X Z) ▷ Y ≫ (Iso.hom (α_ Z X Y) ≫ Z ◁ Iso.hom (β_ X Y)) ≫ Iso.inv (α_ Z Y X))
⊢ Eq.{v + 1} (α :=
    tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z) ⟶
      tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Z Y) X)
    (Iso.hom (β_ X (tensorObj.{v, u} (𝒞 := inst) Y Z)) ≫ Iso.hom (β_ Y Z) ▷ X ≫ Iso.hom (α_ Z Y X) ≫ Iso.inv (α_ Z Y X))
    (X ◁ Iso.hom (β_ Y Z) ≫
      Iso.inv (α_ X Z Y) ≫ (Iso.hom (β_ X Z) ▷ Y ≫ Iso.hom (α_ Z X Y) ≫ Z ◁ Iso.hom (β_ X Y)) ≫ Iso.inv (α_ Z Y X))

Tactic:
rw [assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
X Y Z : C
rw :
  Eq.{v + 1} (α :=
    tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z) ⟶
      tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Z Y) X)
    (Iso.hom (β_ X (tensorObj.{v, u} (𝒞 := inst) Y Z)) ≫ Iso.hom (β_ Y Z) ▷ X ≫ Iso.hom (α_ Z Y X) ≫ Iso.inv (α_ Z Y X))
    (X ◁ Iso.hom (β_ Y Z) ≫
      Iso.inv (α_ X Z Y) ≫ Iso.hom (β_ X Z) ▷ Y ≫ Iso.hom (α_ Z X Y) ≫ Z ◁ Iso.hom (β_ X Y) ≫ Iso.inv (α_ Z Y X))
⊢ Eq.{v + 1} (α :=
    tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z) ⟶
      tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Z Y) X)
    (Iso.hom (β_ X (tensorObj.{v, u} (𝒞 := inst) Y Z)) ≫ Iso.hom (β_ Y Z) ▷ X ≫ Iso.hom (α_ Z Y X) ≫ Iso.inv (α_ Z Y X))
    (X ◁ Iso.hom (β_ Y Z) ≫
      Iso.inv (α_ X Z Y) ≫ Iso.hom (β_ X Z) ▷ Y ≫ (Iso.hom (α_ Z X Y) ≫ Z ◁ Iso.hom (β_ X Y)) ≫ Iso.inv (α_ Z Y X))

Tactic:
rw [assoc]

Premises used: CategoryTheory.Category.assoc
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
X Y Z : C
repeat :
  Eq.{v + 1} (α :=
    tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z) ⟶
      tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Z Y) X)
    (Iso.hom (β_ X (tensorObj.{v, u} (𝒞 := inst) Y Z)) ≫ Iso.hom (β_ Y Z) ▷ X ≫ Iso.hom (α_ Z Y X) ≫ Iso.inv (α_ Z Y X))
    (X ◁ Iso.hom (β_ Y Z) ≫
      Iso.inv (α_ X Z Y) ≫ Iso.hom (β_ X Z) ▷ Y ≫ Iso.hom (α_ Z X Y) ≫ Z ◁ Iso.hom (β_ X Y) ≫ Iso.inv (α_ Z Y X))
⊢ Eq.{v + 1} (α :=
    tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z) ⟶
      tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Z Y) X)
    ((Iso.hom (β_ X (tensorObj.{v, u} (𝒞 := inst) Y Z)) ≫ Iso.hom (β_ Y Z) ▷ X ≫ Iso.hom (α_ Z Y X)) ≫
      Iso.inv (α_ Z Y X))
    ((X ◁ Iso.hom (β_ Y Z) ≫ Iso.inv (α_ X Z Y) ≫ Iso.hom (β_ X Z) ▷ Y ≫ Iso.hom (α_ Z X Y) ≫ Z ◁ Iso.hom (β_ X Y)) ≫
      Iso.inv (α_ Z Y X))

Tactic:
repeat rw [assoc]

Premises used: CategoryTheory.Category.assoc