awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided
Goal:
C : Type u_1
inst_1 : Category.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : BraidedCategory.{v_1, u_1} C
X Y : C
inst : ExactPairing X Y
e_g :
  Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst_1) X (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X) ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X) X)
    (Iso.inv (α_ X Y X) ≫ Iso.hom (β_ X Y) ▷ X)
    ((((((((inv (X ◁ Iso.inv (β_ Y X)) ≫ Iso.inv (α_ X X Y)) ≫ Iso.hom (β_ X X) ▷ Y) ≫ Iso.hom (α_ X X Y)) ≫
              X ◁ Iso.hom (β_ X Y)) ≫
            Iso.inv (α_ X Y X)) ≫
          Iso.inv (β_ Y X) ▷ X) ≫
        Iso.hom (α_ Y X X)) ≫
      Y ◁ Iso.inv (β_ X X) ≫ Iso.inv (α_ Y X X))
⊢ Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst_1) X (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X) ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X) X)
    (Iso.inv (α_ X Y X) ≫ Iso.hom (β_ X Y) ▷ X)
    (((((((inv (X ◁ Iso.inv (β_ Y X)) ≫ Iso.inv (α_ X X Y)) ≫ Iso.hom (β_ X X) ▷ Y) ≫ Iso.hom (α_ X X Y)) ≫
            X ◁ Iso.hom (β_ X Y)) ≫
          Iso.inv (α_ X Y X)) ≫
        Iso.inv (β_ Y X) ▷ X) ≫
      Iso.hom (α_ Y X X) ≫ Y ◁ Iso.inv (β_ X X) ≫ Iso.inv (α_ Y X X))

Tactic:
rw [← assoc]

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

Tactic:
rw [← assoc]

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

Tactic:
repeat rw [← assoc]

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

Tactic:
rw [← IsIso.comp_inv_eq]

Premises used: CategoryTheory.IsIso.comp_inv_eq
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided
Goal:
C : Type u_1
inst_1 : Category.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : BraidedCategory.{v_1, u_1} C
X Y : C
inst : ExactPairing X Y
e_g :
  Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst_1) X (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X) ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) X X))
    (((Iso.inv (α_ X Y X) ≫ Iso.hom (β_ X Y) ▷ X) ≫ inv (Iso.inv (α_ Y X X))) ≫ inv (Y ◁ Iso.inv (β_ X X)))
    (((((((inv (X ◁ Iso.inv (β_ Y X)) ≫ Iso.inv (α_ X X Y)) ≫ Iso.hom (β_ X X) ▷ Y) ≫ Iso.hom (α_ X X Y)) ≫
            X ◁ Iso.hom (β_ X Y)) ≫
          Iso.inv (α_ X Y X)) ≫
        Iso.inv (β_ Y X) ▷ X) ≫
      Iso.hom (α_ Y X X))
⊢ Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst_1) X (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X) ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) X X))
    ((Iso.inv (α_ X Y X) ≫ Iso.hom (β_ X Y) ▷ X) ≫ inv (Iso.inv (α_ Y X X)))
    ((((((((inv (X ◁ Iso.inv (β_ Y X)) ≫ Iso.inv (α_ X X Y)) ≫ Iso.hom (β_ X X) ▷ Y) ≫ Iso.hom (α_ X X Y)) ≫
              X ◁ Iso.hom (β_ X Y)) ≫
            Iso.inv (α_ X Y X)) ≫
          Iso.inv (β_ Y X) ▷ X) ≫
        Iso.hom (α_ Y X X)) ≫
      Y ◁ Iso.inv (β_ X X))

Tactic:
rw [← IsIso.comp_inv_eq]

Premises used: CategoryTheory.IsIso.comp_inv_eq
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided
Goal:
C : Type u_1
inst_1 : Category.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : BraidedCategory.{v_1, u_1} C
X Y : C
inst : ExactPairing X Y
e_g :
  Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst_1) X (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X) ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X) X)
    ((((Iso.inv (α_ X Y X) ≫ Iso.hom (β_ X Y) ▷ X) ≫ inv (Iso.inv (α_ Y X X))) ≫ inv (Y ◁ Iso.inv (β_ X X))) ≫
      inv (Iso.hom (α_ Y X X)))
    ((((((inv (X ◁ Iso.inv (β_ Y X)) ≫ Iso.inv (α_ X X Y)) ≫ Iso.hom (β_ X X) ▷ Y) ≫ Iso.hom (α_ X X Y)) ≫
          X ◁ Iso.hom (β_ X Y)) ≫
        Iso.inv (α_ X Y X)) ≫
      Iso.inv (β_ Y X) ▷ X)
⊢ Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst_1) X (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X) ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) X X))
    (((Iso.inv (α_ X Y X) ≫ Iso.hom (β_ X Y) ▷ X) ≫ inv (Iso.inv (α_ Y X X))) ≫ inv (Y ◁ Iso.inv (β_ X X)))
    (((((((inv (X ◁ Iso.inv (β_ Y X)) ≫ Iso.inv (α_ X X Y)) ≫ Iso.hom (β_ X X) ▷ Y) ≫ Iso.hom (α_ X X Y)) ≫
            X ◁ Iso.hom (β_ X Y)) ≫
          Iso.inv (α_ X Y X)) ≫
        Iso.inv (β_ Y X) ▷ X) ≫
      Iso.hom (α_ Y X X))

Tactic:
rw [← IsIso.comp_inv_eq]

Premises used: CategoryTheory.IsIso.comp_inv_eq
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided
Goal:
C : Type u_1
inst_1 : Category.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : BraidedCategory.{v_1, u_1} C
X Y : C
inst : ExactPairing X Y
e_g :
  Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst_1) X (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X) ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y) X)
    (((((Iso.inv (α_ X Y X) ≫ Iso.hom (β_ X Y) ▷ X) ≫ inv (Iso.inv (α_ Y X X))) ≫ inv (Y ◁ Iso.inv (β_ X X))) ≫
        inv (Iso.hom (α_ Y X X))) ≫
      inv (Iso.inv (β_ Y X) ▷ X))
    (((((inv (X ◁ Iso.inv (β_ Y X)) ≫ Iso.inv (α_ X X Y)) ≫ Iso.hom (β_ X X) ▷ Y) ≫ Iso.hom (α_ X X Y)) ≫
        X ◁ Iso.hom (β_ X Y)) ≫
      Iso.inv (α_ X Y X))
⊢ Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst_1) X (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X) ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X) X)
    ((((Iso.inv (α_ X Y X) ≫ Iso.hom (β_ X Y) ▷ X) ≫ inv (Iso.inv (α_ Y X X))) ≫ inv (Y ◁ Iso.inv (β_ X X))) ≫
      inv (Iso.hom (α_ Y X X)))
    ((((((inv (X ◁ Iso.inv (β_ Y X)) ≫ Iso.inv (α_ X X Y)) ≫ Iso.hom (β_ X X) ▷ Y) ≫ Iso.hom (α_ X X Y)) ≫
          X ◁ Iso.hom (β_ X Y)) ≫
        Iso.inv (α_ X Y X)) ≫
      Iso.inv (β_ Y X) ▷ X)

Tactic:
rw [← IsIso.comp_inv_eq]

Premises used: CategoryTheory.IsIso.comp_inv_eq
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided
Goal:
C : Type u_1
inst_1 : Category.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : BraidedCategory.{v_1, u_1} C
X Y : C
inst : ExactPairing X Y
e_g :
  Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst_1) X (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X) ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst_1) X (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X))
    ((((((Iso.inv (α_ X Y X) ≫ Iso.hom (β_ X Y) ▷ X) ≫ inv (Iso.inv (α_ Y X X))) ≫ inv (Y ◁ Iso.inv (β_ X X))) ≫
          inv (Iso.hom (α_ Y X X))) ≫
        inv (Iso.inv (β_ Y X) ▷ X)) ≫
      inv (Iso.inv (α_ X Y X)))
    ((((inv (X ◁ Iso.inv (β_ Y X)) ≫ Iso.inv (α_ X X Y)) ≫ Iso.hom (β_ X X) ▷ Y) ≫ Iso.hom (α_ X X Y)) ≫
      X ◁ Iso.hom (β_ X Y))
⊢ Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst_1) X (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X) ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y) X)
    (((((Iso.inv (α_ X Y X) ≫ Iso.hom (β_ X Y) ▷ X) ≫ inv (Iso.inv (α_ Y X X))) ≫ inv (Y ◁ Iso.inv (β_ X X))) ≫
        inv (Iso.hom (α_ Y X X))) ≫
      inv (Iso.inv (β_ Y X) ▷ X))
    (((((inv (X ◁ Iso.inv (β_ Y X)) ≫ Iso.inv (α_ X X Y)) ≫ Iso.hom (β_ X X) ▷ Y) ≫ Iso.hom (α_ X X Y)) ≫
        X ◁ Iso.hom (β_ X Y)) ≫
      Iso.inv (α_ X Y X))

Tactic:
rw [← IsIso.comp_inv_eq]

Premises used: CategoryTheory.IsIso.comp_inv_eq
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided
Goal:
C : Type u_1
inst_1 : Category.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : BraidedCategory.{v_1, u_1} C
X Y : C
inst : ExactPairing X Y
e_g :
  Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst_1) X (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X) ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst_1) X (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X))
    ((((((Iso.inv (α_ X Y X) ≫ Iso.hom (β_ X Y) ▷ X) ≫ inv (Iso.inv (α_ Y X X))) ≫ inv (Y ◁ Iso.inv (β_ X X))) ≫
          inv (Iso.hom (α_ Y X X))) ≫
        inv (Iso.inv (β_ Y X) ▷ X)) ≫
      inv (Iso.inv (α_ X Y X)))
    ((((inv (X ◁ Iso.inv (β_ Y X)) ≫ Iso.inv (α_ X X Y)) ≫ Iso.hom (β_ X X) ▷ Y) ≫ Iso.hom (α_ X X Y)) ≫
      X ◁ Iso.hom (β_ X Y))
⊢ Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst_1) X (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X) ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X) X)
    (Iso.inv (α_ X Y X) ≫ Iso.hom (β_ X Y) ▷ X)
    (((((((((inv (X ◁ Iso.inv (β_ Y X)) ≫ Iso.inv (α_ X X Y)) ≫ Iso.hom (β_ X X) ▷ Y) ≫ Iso.hom (α_ X X Y)) ≫
                X ◁ Iso.hom (β_ X Y)) ≫
              Iso.inv (α_ X Y X)) ≫
            Iso.inv (β_ Y X) ▷ X) ≫
          Iso.hom (α_ Y X X)) ≫
        Y ◁ Iso.inv (β_ X X)) ≫
      Iso.inv (α_ Y X X))

Tactic:
iterate 5 rw [← IsIso.comp_inv_eq]

Premises used: CategoryTheory.IsIso.comp_inv_eq
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided
Goal:
C : Type u_1
inst_1 : Category.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : BraidedCategory.{v_1, u_1} C
X Y : C
inst : ExactPairing X Y
⊢ Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst_1) X (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X) ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst_1) X (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X))
    ((((((Iso.inv (α_ X Y X) ≫ Iso.hom (β_ X Y) ▷ X) ≫ inv (Iso.inv (α_ Y X X))) ≫ inv (Y ◁ Iso.inv (β_ X X))) ≫
          inv (Iso.hom (α_ Y X X))) ≫
        inv (Iso.inv (β_ Y X) ▷ X)) ≫
      inv (Iso.inv (α_ X Y X)))
    ((((inv (X ◁ Iso.inv (β_ Y X)) ≫ Iso.inv (α_ X X Y)) ≫ Iso.hom (β_ X X) ▷ Y) ≫ Iso.hom (α_ X X Y)) ≫
      X ◁ Iso.hom (β_ X Y))

Tactic:
simpa using yang_baxter X Y X

Premises used: CategoryTheory.BraidedCategory.yang_baxter
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided
Goal:
C : Type u_1
inst_1 : Category.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : BraidedCategory.{v_1, u_1} C
X Y : C
inst : ExactPairing X Y
⊢ monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) X (tensorUnit.{v_1, u_1} C (𝒞 := inst_1))) (𝟙 X)
      (X ◁ η_ X Y ⊗≫
        monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X) X)
          (monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorObj.{v_1, u_1} (𝒞 := inst_1) X X) Y)
            (𝟙 (tensorObj.{v_1, u_1} (𝒞 := inst_1) X (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y)))
            (monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) X (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y))
              (Iso.hom (β_ X X) ▷ Y)
              (monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y) X)
                (X ◁ Iso.hom (β_ X Y))
                (monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) X X))
                  (Iso.inv (β_ Y X) ▷ X)
                  (Y ◁ Iso.inv (β_ X X) ⊗≫
                    𝟙 (tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X) X))))))
          (ε_ X Y ▷ X ⊗≫ 𝟙 X)) =
    monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) X (tensorUnit.{v_1, u_1} C (𝒞 := inst_1))) (𝟙 X)
      (monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) X (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X))
        (X ◁ η_ X Y ≫ Iso.hom (β_ X (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y)))
        ((Iso.inv (β_ (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X) X) ≫ ε_ X Y ▷ X) ⊗≫ 𝟙 X))

Tactic:
simp [monoidalComp, braiding_tensor_right_hom, braiding_tensor_left_inv]

Premises used: CategoryTheory.BraidedCategory.braiding_tensor_right_hom, CategoryTheory.BraidedCategory.braiding_tensor_left_inv, CategoryTheory.monoidalComp
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided
Goal:
C : Type u_1
inst_1 : Category.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : BraidedCategory.{v_1, u_1} C
X Y : C
inst : ExactPairing X Y
rw :
  monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) X (tensorUnit.{v_1, u_1} C (𝒞 := inst_1))) (𝟙 X)
      (monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) X (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X))
        (Iso.hom (β_ X (tensorUnit.{v_1, u_1} C (𝒞 := inst_1))) ≫ η_ X Y ▷ X)
        ((X ◁ ε_ X Y ≫ Iso.inv (β_ (tensorUnit.{v_1, u_1} C (𝒞 := inst_1)) X)) ⊗≫ 𝟙 X)) =
    𝟙 X
⊢ monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) X (tensorUnit.{v_1, u_1} C (𝒞 := inst_1))) (𝟙 X)
      (monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) X (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X))
        (X ◁ η_ X Y ≫ Iso.hom (β_ X (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y)))
        ((Iso.inv (β_ (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X) X) ≫ ε_ X Y ▷ X) ⊗≫ 𝟙 X)) =
    𝟙 X

Tactic:
rw [braiding_naturality_right, ← braiding_inv_naturality_right]

Premises used: CategoryTheory.BraidedCategory.braiding_naturality_right, CategoryTheory.BraidedCategory.braiding_inv_naturality_right
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided
Goal:
C : Type u_1
inst_1 : Category.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : BraidedCategory.{v_1, u_1} C
X Y : C
inst : ExactPairing X Y
⊢ monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) X (tensorUnit.{v_1, u_1} C (𝒞 := inst_1))) (𝟙 X)
      (monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) X (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X))
        (Iso.hom (β_ X (tensorUnit.{v_1, u_1} C (𝒞 := inst_1))) ≫ η_ X Y ▷ X)
        ((X ◁ ε_ X Y ≫ Iso.inv (β_ (tensorUnit.{v_1, u_1} C (𝒞 := inst_1)) X)) ⊗≫ 𝟙 X)) =
    𝟙 X

Tactic:
simp [monoidalComp]

Premises used: CategoryTheory.monoidalComp
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided
Goal:
C : Type u_1
inst_1 : Category.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : BraidedCategory.{v_1, u_1} C
X Y : C
inst : ExactPairing X Y
rw :
  Eq.{v_1 + 1} (α := Y ⟶ Y)
    (CategoryStruct.comp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorUnit.{v_1, u_1} C (𝒞 := inst_1)) Y)
      (Iso.inv (λ_ Y))
      (((η_ X Y ≫ Iso.inv (β_ Y X)) ▷ Y ≫ Iso.hom (α_ Y X Y) ≫ Y ◁ (Iso.hom (β_ X Y) ≫ ε_ X Y)) ≫ Iso.hom (ρ_ Y)))
    (𝟙 Y)
⊢ Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorUnit.{v_1, u_1} C (𝒞 := inst_1)) Y ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorUnit.{v_1, u_1} C (𝒞 := inst_1)))
    ((η_ X Y ≫ Iso.inv (β_ Y X)) ▷ Y ≫ Iso.hom (α_ Y X Y) ≫ Y ◁ (Iso.hom (β_ X Y) ≫ ε_ X Y))
    (Iso.hom (λ_ Y) ≫ Iso.inv (ρ_ Y))

Tactic:
rw [Iso.eq_comp_inv, ← Iso.inv_comp_eq_id]

Premises used: CategoryTheory.Iso.inv_comp_eq_id, CategoryTheory.Iso.eq_comp_inv
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided
Goal:
C : Type u_1
inst_1 : Category.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : BraidedCategory.{v_1, u_1} C
X Y : C
inst : ExactPairing X Y
⊢ Eq.{v_1 + 1} (α := Y ⟶ Y)
    (CategoryStruct.comp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorUnit.{v_1, u_1} C (𝒞 := inst_1)) Y)
      (Iso.inv (λ_ Y))
      (((η_ X Y ≫ Iso.inv (β_ Y X)) ▷ Y ≫ Iso.hom (α_ Y X Y) ≫ Y ◁ (Iso.hom (β_ X Y) ≫ ε_ X Y)) ≫ Iso.hom (ρ_ Y)))
    (monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorUnit.{v_1, u_1} C (𝒞 := inst_1)) Y) (𝟙 Y)
      (monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y) Y) (η_ X Y ▷ Y)
        (CategoryStruct.comp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X))
          (Iso.inv (β_ Y X) ▷ Y ⊗≫ Y ◁ Iso.hom (β_ X Y)) (Y ◁ ε_ X Y ⊗≫ 𝟙 Y))))

Tactic:
monoidal
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided
Goal:
C : Type u_1
inst_1 : Category.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : BraidedCategory.{v_1, u_1} C
X Y : C
inst : ExactPairing X Y
e_g :
  Iso.inv (β_ Y X) ▷ Y ⊗≫ Y ◁ Iso.hom (β_ X Y) =
    monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) X (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y Y))
      (𝟙 (tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y) Y))
      (monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y) Y)
        (X ◁ Iso.hom (β_ Y Y))
        (monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y))
          (Iso.hom (β_ X Y) ▷ Y)
          (monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y Y) X)
            (Y ◁ Iso.inv (β_ Y X))
            (Iso.inv (β_ Y Y) ▷ X ⊗≫
              𝟙 (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X))))))
e_g₁ :
  Eq.{v_1 + 1} (α := tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X) ⟶ Y)
    (Y ◁ ε_ X Y ⊗≫ 𝟙 Y)
    (CategoryStruct.comp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X))
      (Iso.hom ⊗𝟙 ) (Y ◁ ε_ X Y ⊗≫ 𝟙 Y))
⊢ Eq.{v_1 + 1} (α := Y ⟶ Y)
    (monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorUnit.{v_1, u_1} C (𝒞 := inst_1)) Y) (𝟙 Y)
      (monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y) Y) (η_ X Y ▷ Y)
        (CategoryStruct.comp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X))
          (Iso.inv (β_ Y X) ▷ Y ⊗≫ Y ◁ Iso.hom (β_ X Y)) (Y ◁ ε_ X Y ⊗≫ 𝟙 Y))))
    (monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorUnit.{v_1, u_1} C (𝒞 := inst_1)) Y) (𝟙 Y)
      (η_ X Y ▷ Y ⊗≫
        monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X))
          (monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) X (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y Y))
            (𝟙 (tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y) Y))
            (monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y) Y)
              (X ◁ Iso.hom (β_ Y Y))
              (monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y))
                (Iso.hom (β_ X Y) ▷ Y)
                (monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y Y) X)
                  (Y ◁ Iso.inv (β_ Y X))
                  (Iso.inv (β_ Y Y) ▷ X ⊗≫
                    𝟙 (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X)))))))
          (Y ◁ ε_ X Y ⊗≫ 𝟙 Y)))

Tactic:
congr 3
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided
Goal:
C : Type u_1
inst_1 : Category.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : BraidedCategory.{v_1, u_1} C
X Y : C
inst : ExactPairing X Y
⊢ Eq.{v_1 + 1} (α := tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X) ⟶ Y)
    (Y ◁ ε_ X Y ⊗≫ 𝟙 Y)
    (CategoryStruct.comp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X))
      (Iso.hom ⊗𝟙 ) (Y ◁ ε_ X Y ⊗≫ 𝟙 Y))

Tactic:
simp [monoidalComp]

Premises used: CategoryTheory.monoidalComp
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Braided
Goal:
C : Type u_1
inst_1 : Category.{v_1, u_1} C
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : BraidedCategory.{v_1, u_1} C
X Y : C
inst : ExactPairing X Y
⊢ Eq.{v_1 + 1} (α := tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X) ⟶ Y)
    (Y ◁ ε_ X Y ⊗≫ 𝟙 Y)
    (CategoryStruct.comp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X))
      (Iso.hom ⊗𝟙 ) (Y ◁ ε_ X Y ⊗≫ 𝟙 Y))

Tactic:
on_goal 2 => simp [monoidalComp]

Premises used: CategoryTheory.monoidalComp