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) (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y) Y ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X))
    (Iso.inv (β_ Y X) ▷ Y ≫ Iso.hom (α_ Y X Y) ≫ Y ◁ Iso.hom (β_ X Y))
    (Iso.hom (α_ X Y Y) ≫
      X ◁ Iso.hom (β_ Y Y) ≫
        Iso.inv (α_ X Y Y) ≫
          Iso.hom (β_ X Y) ▷ Y ≫
            Iso.hom (α_ Y X Y) ≫ Y ◁ Iso.inv (β_ Y X) ≫ Iso.inv (α_ Y Y X) ≫ Iso.inv (β_ Y Y) ▷ X ≫ Iso.hom (α_ Y Y X))
⊢ 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))))))

Tactic:
simp only [monoidalComp, MonoidalCoherence.assoc_iso, MonoidalCoherence.whiskerRight_iso,
        MonoidalCoherence.refl_iso, whiskerRightIso_refl, Iso.trans_refl,
        MonoidalCoherence.assoc'_iso, Iso.refl_trans, Iso.symm_hom, comp_id, id_comp]

Premises used: CategoryTheory.monoidalComp, CategoryTheory.MonoidalCoherence.assoc'_iso, CategoryTheory.Iso.symm_hom, CategoryTheory.MonoidalCoherence.whiskerRight_iso, CategoryTheory.Iso.trans_refl, CategoryTheory.MonoidalCategory.whiskerRightIso_refl, CategoryTheory.Category.comp_id, CategoryTheory.Iso.refl_trans, CategoryTheory.MonoidalCoherence.refl_iso, CategoryTheory.MonoidalCoherence.assoc_iso, CategoryTheory.Category.id_comp
-- 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) (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X) Y ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X))
    (Iso.hom (α_ Y X Y) ≫ Y ◁ Iso.hom (β_ X Y))
    (inv (Iso.inv (β_ Y X) ▷ Y) ≫
      Iso.hom (α_ X Y Y) ≫
        X ◁ Iso.hom (β_ Y Y) ≫
          Iso.inv (α_ X Y Y) ≫
            Iso.hom (β_ X Y) ▷ Y ≫
              Iso.hom (α_ Y X Y) ≫
                Y ◁ Iso.inv (β_ Y X) ≫ Iso.inv (α_ Y Y X) ≫ Iso.inv (β_ Y Y) ▷ X ≫ Iso.hom (α_ Y Y X))
⊢ Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y) Y ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X))
    (Iso.inv (β_ Y X) ▷ Y ≫ Iso.hom (α_ Y X Y) ≫ Y ◁ Iso.hom (β_ X Y))
    (Iso.hom (α_ X Y Y) ≫
      X ◁ Iso.hom (β_ Y Y) ≫
        Iso.inv (α_ X Y Y) ≫
          Iso.hom (β_ X Y) ▷ Y ≫
            Iso.hom (α_ Y X Y) ≫ Y ◁ Iso.inv (β_ Y X) ≫ Iso.inv (α_ Y Y X) ≫ Iso.inv (β_ Y Y) ▷ X ≫ Iso.hom (α_ Y Y X))

Tactic:
rw [← IsIso.eq_inv_comp]

Premises used: CategoryTheory.IsIso.eq_inv_comp
-- 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) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y) ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X))
    (Y ◁ Iso.hom (β_ X Y))
    (inv (Iso.hom (α_ Y X Y)) ≫
      inv (Iso.inv (β_ Y X) ▷ Y) ≫
        Iso.hom (α_ X Y Y) ≫
          X ◁ Iso.hom (β_ Y Y) ≫
            Iso.inv (α_ X Y Y) ≫
              Iso.hom (β_ X Y) ▷ Y ≫
                Iso.hom (α_ Y X Y) ≫
                  Y ◁ Iso.inv (β_ Y X) ≫ Iso.inv (α_ Y Y X) ≫ Iso.inv (β_ Y Y) ▷ X ≫ Iso.hom (α_ Y Y X))
⊢ Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X) Y ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X))
    (Iso.hom (α_ Y X Y) ≫ Y ◁ Iso.hom (β_ X Y))
    (inv (Iso.inv (β_ Y X) ▷ Y) ≫
      Iso.hom (α_ X Y Y) ≫
        X ◁ Iso.hom (β_ Y Y) ≫
          Iso.inv (α_ X Y Y) ≫
            Iso.hom (β_ X Y) ▷ Y ≫
              Iso.hom (α_ Y X Y) ≫
                Y ◁ Iso.inv (β_ Y X) ≫ Iso.inv (α_ Y Y X) ≫ Iso.inv (β_ Y Y) ▷ X ≫ Iso.hom (α_ Y Y X))

Tactic:
rw [← IsIso.eq_inv_comp]

Premises used: CategoryTheory.IsIso.eq_inv_comp
-- 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) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y) ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X))
    (Y ◁ Iso.hom (β_ X Y))
    (inv (Iso.hom (α_ Y X Y)) ≫
      inv (Iso.inv (β_ Y X) ▷ Y) ≫
        Iso.hom (α_ X Y Y) ≫
          X ◁ Iso.hom (β_ Y Y) ≫
            Iso.inv (α_ X Y Y) ≫
              Iso.hom (β_ X Y) ▷ Y ≫
                Iso.hom (α_ Y X Y) ≫
                  Y ◁ Iso.inv (β_ Y X) ≫ Iso.inv (α_ Y Y X) ≫ Iso.inv (β_ Y Y) ▷ X ≫ Iso.hom (α_ Y Y X))
⊢ Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y) Y ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X))
    (Iso.inv (β_ Y X) ▷ Y ≫ Iso.hom (α_ Y X Y) ≫ Y ◁ Iso.hom (β_ X Y))
    (Iso.hom (α_ X Y Y) ≫
      X ◁ Iso.hom (β_ Y Y) ≫
        Iso.inv (α_ X Y Y) ≫
          Iso.hom (β_ X Y) ▷ Y ≫
            Iso.hom (α_ Y X Y) ≫ Y ◁ Iso.inv (β_ Y X) ≫ Iso.inv (α_ Y Y X) ≫ Iso.inv (β_ Y Y) ▷ X ≫ Iso.hom (α_ Y Y X))

Tactic:
iterate 2 rw [← IsIso.eq_inv_comp]

Premises used: CategoryTheory.IsIso.eq_inv_comp
-- 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) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y) ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X))
    (Y ◁ Iso.hom (β_ X Y))
    ((inv (Iso.hom (α_ Y X Y)) ≫ inv (Iso.inv (β_ Y X) ▷ Y)) ≫
      Iso.hom (α_ X Y Y) ≫
        X ◁ Iso.hom (β_ Y Y) ≫
          Iso.inv (α_ X Y Y) ≫
            Iso.hom (β_ X Y) ▷ Y ≫
              Iso.hom (α_ Y X Y) ≫
                Y ◁ Iso.inv (β_ Y X) ≫ Iso.inv (α_ Y Y X) ≫ Iso.inv (β_ Y Y) ▷ X ≫ Iso.hom (α_ Y Y X))
⊢ Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y) ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X))
    (Y ◁ Iso.hom (β_ X Y))
    (inv (Iso.hom (α_ Y X Y)) ≫
      inv (Iso.inv (β_ Y X) ▷ Y) ≫
        Iso.hom (α_ X Y Y) ≫
          X ◁ Iso.hom (β_ Y Y) ≫
            Iso.inv (α_ X Y Y) ≫
              Iso.hom (β_ X Y) ▷ Y ≫
                Iso.hom (α_ Y X Y) ≫
                  Y ◁ Iso.inv (β_ Y X) ≫ Iso.inv (α_ Y Y X) ≫ Iso.inv (β_ Y Y) ▷ X ≫ Iso.hom (α_ Y Y 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) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y) ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X))
    (Y ◁ Iso.hom (β_ X Y))
    (((inv (Iso.hom (α_ Y X Y)) ≫ inv (Iso.inv (β_ Y X) ▷ Y)) ≫ Iso.hom (α_ X Y Y)) ≫
      X ◁ Iso.hom (β_ Y Y) ≫
        Iso.inv (α_ X Y Y) ≫
          Iso.hom (β_ X Y) ▷ Y ≫
            Iso.hom (α_ Y X Y) ≫ Y ◁ Iso.inv (β_ Y X) ≫ Iso.inv (α_ Y Y X) ≫ Iso.inv (β_ Y Y) ▷ X ≫ Iso.hom (α_ Y Y X))
⊢ Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y) ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X))
    (Y ◁ Iso.hom (β_ X Y))
    ((inv (Iso.hom (α_ Y X Y)) ≫ inv (Iso.inv (β_ Y X) ▷ Y)) ≫
      Iso.hom (α_ X Y Y) ≫
        X ◁ Iso.hom (β_ Y Y) ≫
          Iso.inv (α_ X Y Y) ≫
            Iso.hom (β_ X Y) ▷ Y ≫
              Iso.hom (α_ Y X Y) ≫
                Y ◁ Iso.inv (β_ Y X) ≫ Iso.inv (α_ Y Y X) ≫ Iso.inv (β_ Y Y) ▷ X ≫ Iso.hom (α_ Y Y 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) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y) ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X))
    (Y ◁ Iso.hom (β_ X Y))
    ((((inv (Iso.hom (α_ Y X Y)) ≫ inv (Iso.inv (β_ Y X) ▷ Y)) ≫ Iso.hom (α_ X Y Y)) ≫ X ◁ Iso.hom (β_ Y Y)) ≫
      Iso.inv (α_ X Y Y) ≫
        Iso.hom (β_ X Y) ▷ Y ≫
          Iso.hom (α_ Y X Y) ≫ Y ◁ Iso.inv (β_ Y X) ≫ Iso.inv (α_ Y Y X) ≫ Iso.inv (β_ Y Y) ▷ X ≫ Iso.hom (α_ Y Y X))
⊢ Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y) ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X))
    (Y ◁ Iso.hom (β_ X Y))
    (((inv (Iso.hom (α_ Y X Y)) ≫ inv (Iso.inv (β_ Y X) ▷ Y)) ≫ Iso.hom (α_ X Y Y)) ≫
      X ◁ Iso.hom (β_ Y Y) ≫
        Iso.inv (α_ X Y Y) ≫
          Iso.hom (β_ X Y) ▷ Y ≫
            Iso.hom (α_ Y X Y) ≫ Y ◁ Iso.inv (β_ Y X) ≫ Iso.inv (α_ Y Y X) ≫ Iso.inv (β_ Y Y) ▷ X ≫ Iso.hom (α_ Y Y 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) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y) ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X))
    (Y ◁ Iso.hom (β_ X Y))
    (((((inv (Iso.hom (α_ Y X Y)) ≫ inv (Iso.inv (β_ Y X) ▷ Y)) ≫ Iso.hom (α_ X Y Y)) ≫ X ◁ Iso.hom (β_ Y Y)) ≫
        Iso.inv (α_ X Y Y)) ≫
      Iso.hom (β_ X Y) ▷ Y ≫
        Iso.hom (α_ Y X Y) ≫ Y ◁ Iso.inv (β_ Y X) ≫ Iso.inv (α_ Y Y X) ≫ Iso.inv (β_ Y Y) ▷ X ≫ Iso.hom (α_ Y Y X))
⊢ Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y) ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X))
    (Y ◁ Iso.hom (β_ X Y))
    ((((inv (Iso.hom (α_ Y X Y)) ≫ inv (Iso.inv (β_ Y X) ▷ Y)) ≫ Iso.hom (α_ X Y Y)) ≫ X ◁ Iso.hom (β_ Y Y)) ≫
      Iso.inv (α_ X Y Y) ≫
        Iso.hom (β_ X Y) ▷ Y ≫
          Iso.hom (α_ Y X Y) ≫ Y ◁ Iso.inv (β_ Y X) ≫ Iso.inv (α_ Y Y X) ≫ Iso.inv (β_ Y Y) ▷ X ≫ Iso.hom (α_ Y Y 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) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y) ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X))
    (Y ◁ Iso.hom (β_ X Y))
    ((((((inv (Iso.hom (α_ Y X Y)) ≫ inv (Iso.inv (β_ Y X) ▷ Y)) ≫ Iso.hom (α_ X Y Y)) ≫ X ◁ Iso.hom (β_ Y Y)) ≫
          Iso.inv (α_ X Y Y)) ≫
        Iso.hom (β_ X Y) ▷ Y) ≫
      Iso.hom (α_ Y X Y) ≫ Y ◁ Iso.inv (β_ Y X) ≫ Iso.inv (α_ Y Y X) ≫ Iso.inv (β_ Y Y) ▷ X ≫ Iso.hom (α_ Y Y X))
⊢ Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y) ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X))
    (Y ◁ Iso.hom (β_ X Y))
    (((((inv (Iso.hom (α_ Y X Y)) ≫ inv (Iso.inv (β_ Y X) ▷ Y)) ≫ Iso.hom (α_ X Y Y)) ≫ X ◁ Iso.hom (β_ Y Y)) ≫
        Iso.inv (α_ X Y Y)) ≫
      Iso.hom (β_ X Y) ▷ Y ≫
        Iso.hom (α_ Y X Y) ≫ Y ◁ Iso.inv (β_ Y X) ≫ Iso.inv (α_ Y Y X) ≫ Iso.inv (β_ Y Y) ▷ X ≫ Iso.hom (α_ Y Y 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) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y) ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X))
    (Y ◁ Iso.hom (β_ X Y))
    (((((((inv (Iso.hom (α_ Y X Y)) ≫ inv (Iso.inv (β_ Y X) ▷ Y)) ≫ Iso.hom (α_ X Y Y)) ≫ X ◁ Iso.hom (β_ Y Y)) ≫
            Iso.inv (α_ X Y Y)) ≫
          Iso.hom (β_ X Y) ▷ Y) ≫
        Iso.hom (α_ Y X Y)) ≫
      Y ◁ Iso.inv (β_ Y X) ≫ Iso.inv (α_ Y Y X) ≫ Iso.inv (β_ Y Y) ▷ X ≫ Iso.hom (α_ Y Y X))
⊢ Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y) ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X))
    (Y ◁ Iso.hom (β_ X Y))
    ((((((inv (Iso.hom (α_ Y X Y)) ≫ inv (Iso.inv (β_ Y X) ▷ Y)) ≫ Iso.hom (α_ X Y Y)) ≫ X ◁ Iso.hom (β_ Y Y)) ≫
          Iso.inv (α_ X Y Y)) ≫
        Iso.hom (β_ X Y) ▷ Y) ≫
      Iso.hom (α_ Y X Y) ≫ Y ◁ Iso.inv (β_ Y X) ≫ Iso.inv (α_ Y Y X) ≫ Iso.inv (β_ Y Y) ▷ X ≫ Iso.hom (α_ Y Y 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) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y) ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X))
    (Y ◁ Iso.hom (β_ X Y))
    ((((((((inv (Iso.hom (α_ Y X Y)) ≫ inv (Iso.inv (β_ Y X) ▷ Y)) ≫ Iso.hom (α_ X Y Y)) ≫ X ◁ Iso.hom (β_ Y Y)) ≫
              Iso.inv (α_ X Y Y)) ≫
            Iso.hom (β_ X Y) ▷ Y) ≫
          Iso.hom (α_ Y X Y)) ≫
        Y ◁ Iso.inv (β_ Y X)) ≫
      Iso.inv (α_ Y Y X) ≫ Iso.inv (β_ Y Y) ▷ X ≫ Iso.hom (α_ Y Y X))
⊢ Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y) ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X))
    (Y ◁ Iso.hom (β_ X Y))
    (((((((inv (Iso.hom (α_ Y X Y)) ≫ inv (Iso.inv (β_ Y X) ▷ Y)) ≫ Iso.hom (α_ X Y Y)) ≫ X ◁ Iso.hom (β_ Y Y)) ≫
            Iso.inv (α_ X Y Y)) ≫
          Iso.hom (β_ X Y) ▷ Y) ≫
        Iso.hom (α_ Y X Y)) ≫
      Y ◁ Iso.inv (β_ Y X) ≫ Iso.inv (α_ Y Y X) ≫ Iso.inv (β_ Y Y) ▷ X ≫ Iso.hom (α_ Y Y 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) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y) ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X))
    (Y ◁ Iso.hom (β_ X Y))
    (((((((((inv (Iso.hom (α_ Y X Y)) ≫ inv (Iso.inv (β_ Y X) ▷ Y)) ≫ Iso.hom (α_ X Y Y)) ≫ X ◁ Iso.hom (β_ Y Y)) ≫
                Iso.inv (α_ X Y Y)) ≫
              Iso.hom (β_ X Y) ▷ Y) ≫
            Iso.hom (α_ Y X Y)) ≫
          Y ◁ Iso.inv (β_ Y X)) ≫
        Iso.inv (α_ Y Y X)) ≫
      Iso.inv (β_ Y Y) ▷ X ≫ Iso.hom (α_ Y Y X))
⊢ Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y) ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X))
    (Y ◁ Iso.hom (β_ X Y))
    ((((((((inv (Iso.hom (α_ Y X Y)) ≫ inv (Iso.inv (β_ Y X) ▷ Y)) ≫ Iso.hom (α_ X Y Y)) ≫ X ◁ Iso.hom (β_ Y Y)) ≫
              Iso.inv (α_ X Y Y)) ≫
            Iso.hom (β_ X Y) ▷ Y) ≫
          Iso.hom (α_ Y X Y)) ≫
        Y ◁ Iso.inv (β_ Y X)) ≫
      Iso.inv (α_ Y Y X) ≫ Iso.inv (β_ Y Y) ▷ X ≫ Iso.hom (α_ Y Y 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) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y) ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X))
    (Y ◁ Iso.hom (β_ X Y))
    ((((((((((inv (Iso.hom (α_ Y X Y)) ≫ inv (Iso.inv (β_ Y X) ▷ Y)) ≫ Iso.hom (α_ X Y Y)) ≫ X ◁ Iso.hom (β_ Y Y)) ≫
                  Iso.inv (α_ X Y Y)) ≫
                Iso.hom (β_ X Y) ▷ Y) ≫
              Iso.hom (α_ Y X Y)) ≫
            Y ◁ Iso.inv (β_ Y X)) ≫
          Iso.inv (α_ Y Y X)) ≫
        Iso.inv (β_ Y Y) ▷ X) ≫
      Iso.hom (α_ Y Y X))
⊢ Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y) ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X))
    (Y ◁ Iso.hom (β_ X Y))
    (((((((((inv (Iso.hom (α_ Y X Y)) ≫ inv (Iso.inv (β_ Y X) ▷ Y)) ≫ Iso.hom (α_ X Y Y)) ≫ X ◁ Iso.hom (β_ Y Y)) ≫
                Iso.inv (α_ X Y Y)) ≫
              Iso.hom (β_ X Y) ▷ Y) ≫
            Iso.hom (α_ Y X Y)) ≫
          Y ◁ Iso.inv (β_ Y X)) ≫
        Iso.inv (α_ Y Y X)) ≫
      Iso.inv (β_ Y Y) ▷ X ≫ Iso.hom (α_ Y Y 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) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y) ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X))
    (Y ◁ Iso.hom (β_ X Y))
    ((((((((((inv (Iso.hom (α_ Y X Y)) ≫ inv (Iso.inv (β_ Y X) ▷ Y)) ≫ Iso.hom (α_ X Y Y)) ≫ X ◁ Iso.hom (β_ Y Y)) ≫
                  Iso.inv (α_ X Y Y)) ≫
                Iso.hom (β_ X Y) ▷ Y) ≫
              Iso.hom (α_ Y X Y)) ≫
            Y ◁ Iso.inv (β_ Y X)) ≫
          Iso.inv (α_ Y Y X)) ≫
        Iso.inv (β_ Y Y) ▷ X) ≫
      Iso.hom (α_ Y Y X))
⊢ Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y) ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X))
    (Y ◁ Iso.hom (β_ X Y))
    (inv (Iso.hom (α_ Y X Y)) ≫
      inv (Iso.inv (β_ Y X) ▷ Y) ≫
        Iso.hom (α_ X Y Y) ≫
          X ◁ Iso.hom (β_ Y Y) ≫
            Iso.inv (α_ X Y Y) ≫
              Iso.hom (β_ X Y) ▷ Y ≫
                Iso.hom (α_ Y X Y) ≫
                  Y ◁ Iso.inv (β_ Y X) ≫ Iso.inv (α_ Y Y X) ≫ Iso.inv (β_ Y Y) ▷ X ≫ Iso.hom (α_ Y Y 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) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y) ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y Y) X)
    (Y ◁ Iso.hom (β_ X Y) ≫ inv (Iso.hom (α_ Y Y X)))
    (((((((((inv (Iso.hom (α_ Y X Y)) ≫ inv (Iso.inv (β_ Y X) ▷ Y)) ≫ Iso.hom (α_ X Y Y)) ≫ X ◁ Iso.hom (β_ Y Y)) ≫
                Iso.inv (α_ X Y Y)) ≫
              Iso.hom (β_ X Y) ▷ Y) ≫
            Iso.hom (α_ Y X Y)) ≫
          Y ◁ Iso.inv (β_ Y X)) ≫
        Iso.inv (α_ Y Y X)) ≫
      Iso.inv (β_ Y Y) ▷ X)
⊢ Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y) ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X))
    (Y ◁ Iso.hom (β_ X Y))
    ((((((((((inv (Iso.hom (α_ Y X Y)) ≫ inv (Iso.inv (β_ Y X) ▷ Y)) ≫ Iso.hom (α_ X Y Y)) ≫ X ◁ Iso.hom (β_ Y Y)) ≫
                  Iso.inv (α_ X Y Y)) ≫
                Iso.hom (β_ X Y) ▷ Y) ≫
              Iso.hom (α_ Y X Y)) ≫
            Y ◁ Iso.inv (β_ Y X)) ≫
          Iso.inv (α_ Y Y X)) ≫
        Iso.inv (β_ Y Y) ▷ X) ≫
      Iso.hom (α_ Y 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) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y) ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y Y) X)
    ((Y ◁ Iso.hom (β_ X Y) ≫ inv (Iso.hom (α_ Y Y X))) ≫ inv (Iso.inv (β_ Y Y) ▷ X))
    ((((((((inv (Iso.hom (α_ Y X Y)) ≫ inv (Iso.inv (β_ Y X) ▷ Y)) ≫ Iso.hom (α_ X Y Y)) ≫ X ◁ Iso.hom (β_ Y Y)) ≫
              Iso.inv (α_ X Y Y)) ≫
            Iso.hom (β_ X Y) ▷ Y) ≫
          Iso.hom (α_ Y X Y)) ≫
        Y ◁ Iso.inv (β_ Y X)) ≫
      Iso.inv (α_ Y Y X))
⊢ Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y) ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y Y) X)
    (Y ◁ Iso.hom (β_ X Y) ≫ inv (Iso.hom (α_ Y Y X)))
    (((((((((inv (Iso.hom (α_ Y X Y)) ≫ inv (Iso.inv (β_ Y X) ▷ Y)) ≫ Iso.hom (α_ X Y Y)) ≫ X ◁ Iso.hom (β_ Y Y)) ≫
                Iso.inv (α_ X Y Y)) ≫
              Iso.hom (β_ X Y) ▷ Y) ≫
            Iso.hom (α_ Y X Y)) ≫
          Y ◁ Iso.inv (β_ Y X)) ≫
        Iso.inv (α_ Y Y X)) ≫
      Iso.inv (β_ Y 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) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y) ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X))
    (((Y ◁ Iso.hom (β_ X Y) ≫ inv (Iso.hom (α_ Y Y X))) ≫ inv (Iso.inv (β_ Y Y) ▷ X)) ≫ inv (Iso.inv (α_ Y Y X)))
    (((((((inv (Iso.hom (α_ Y X Y)) ≫ inv (Iso.inv (β_ Y X) ▷ Y)) ≫ Iso.hom (α_ X Y Y)) ≫ X ◁ Iso.hom (β_ Y Y)) ≫
            Iso.inv (α_ X Y Y)) ≫
          Iso.hom (β_ X Y) ▷ Y) ≫
        Iso.hom (α_ Y X Y)) ≫
      Y ◁ Iso.inv (β_ Y X))
⊢ Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y) ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y Y) X)
    ((Y ◁ Iso.hom (β_ X Y) ≫ inv (Iso.hom (α_ Y Y X))) ≫ inv (Iso.inv (β_ Y Y) ▷ X))
    ((((((((inv (Iso.hom (α_ Y X Y)) ≫ inv (Iso.inv (β_ Y X) ▷ Y)) ≫ Iso.hom (α_ X Y Y)) ≫ X ◁ Iso.hom (β_ Y Y)) ≫
              Iso.inv (α_ X Y Y)) ≫
            Iso.hom (β_ X Y) ▷ Y) ≫
          Iso.hom (α_ Y X Y)) ≫
        Y ◁ Iso.inv (β_ Y X)) ≫
      Iso.inv (α_ Y Y X))

Tactic:
rw [← IsIso.comp_inv_eq]

Premises used: CategoryTheory.IsIso.comp_inv_eq