awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y Y' : C
inst_2 : ExactPairing X Y'
i : Y ≅ Y'
rw :
  Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (Iso.hom ⊗𝟙 ) (Iso.hom (λ_ X) ≫ Iso.inv (ρ_ X))
⊢ Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (η_ X Y' ▷ X ⊗≫ X ◁ ε_ X Y') (Iso.hom (λ_ X) ≫ Iso.inv (ρ_ X))

Tactic:
rw [evaluation_coevaluation'']

Premises used: CategoryTheory.ExactPairing.evaluation_coevaluation''
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y Y' : C
inst_2 : ExactPairing X Y'
i : Y ≅ Y'
⊢ Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (Iso.hom ⊗𝟙 ) (Iso.hom (λ_ X) ≫ Iso.inv (ρ_ X))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y Y' : C
inst_2 : ExactPairing X Y'
i : Y ≅ Y'
_ :
  Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    ((η_ X Y' ≫ X ◁ i.inv) ▷ X ≫ Iso.hom (α_ X Y X) ≫ X ◁ (i.hom ▷ X ≫ ε_ X Y'))
    (η_ X Y' ▷ X ⊗≫ X ◁ (i.inv ≫ i.hom) ▷ X ≫ X ◁ ε_ X Y')
_₁ :
  Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (η_ X Y' ▷ X ⊗≫ X ◁ (i.inv ≫ i.hom) ▷ X ≫ X ◁ ε_ X Y') (η_ X Y' ▷ X ⊗≫ X ◁ ε_ X Y')
_₂ :
  Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (η_ X Y' ▷ X ⊗≫ X ◁ ε_ X Y') (Iso.hom (λ_ X) ≫ Iso.inv (ρ_ X))
⊢ Eq (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    ((η_ X Y' ≫ X ◁ i.inv) ▷ X ≫ Iso.hom (α_ X Y X) ≫ X ◁ (i.hom ▷ X ≫ ε_ X Y')) (Iso.hom (λ_ X) ≫ Iso.inv (ρ_ X))

Tactic:
calc
      _ = η_ X Y' ▷ X ⊗≫ X ◁ (i.inv ≫ i.hom) ▷ X ≫ X ◁ ε_ X Y' := by
        monoidal
      _ = η_ X Y' ▷ X ⊗≫ X ◁ ε_ X Y' := by
        rw [Iso.inv_hom_id]; monoidal
      _ = _ := by
        rw [evaluation_coevaluation'']
        simp

Premises used: CategoryTheory.ExactPairing.evaluation, CategoryTheory.CategoryStruct.comp, CategoryTheory.ExactPairing.coevaluation, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y₁ Y₂ : C
p₁ : ExactPairing X Y₁
p₂ : ExactPairing X Y₂
rw : Eq.{v₁ + 1} (α := Y₁ ⟶ Y₁) (𝟙 (@rightDual.{v₁, u₁} _ inst inst_1 X _)) (𝟙 Y₁)
⊢ Eq.{v₁ + 1} (α := Y₁ ⟶ Y₁) (CategoryStruct.comp (Y := Y₂) (𝟙 Xᘁ) (𝟙 Xᘁ) : Y₁ ⟶ Y₁) (𝟙 Y₁ : Y₁ ⟶ Y₁)

Tactic:
rw [← @comp_rightAdjointMate, Category.comp_id, @rightAdjointMate_id]

Premises used: CategoryTheory.comp_rightAdjointMate, CategoryTheory.Category.comp_id, CategoryTheory.rightAdjointMate_id
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y₁ Y₂ : C
p₁ : ExactPairing X Y₁
p₂ : ExactPairing X Y₂
⊢ Eq.{v₁ + 1} (α := Y₁ ⟶ Y₁) (𝟙 (@rightDual.{v₁, u₁} _ inst inst_1 X _)) (𝟙 Y₁)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y₁ Y₂ : C
p₁ : ExactPairing X Y₁
p₂ : ExactPairing X Y₂
rw : Eq.{v₁ + 1} (α := Y₂ ⟶ Y₂) (𝟙 (@rightDual.{v₁, u₁} _ inst inst_1 X _)) (𝟙 Y₂)
⊢ Eq.{v₁ + 1} (α := Y₂ ⟶ Y₂) (CategoryStruct.comp (Y := Y₁) (𝟙 Xᘁ) (𝟙 Xᘁ) : Y₂ ⟶ Y₂) (𝟙 Y₂ : Y₂ ⟶ Y₂)

Tactic:
rw [← @comp_rightAdjointMate, Category.comp_id, @rightAdjointMate_id]

Premises used: CategoryTheory.comp_rightAdjointMate, CategoryTheory.Category.comp_id, CategoryTheory.rightAdjointMate_id
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y₁ Y₂ : C
p₁ : ExactPairing X Y₁
p₂ : ExactPairing X Y₂
⊢ Eq.{v₁ + 1} (α := Y₂ ⟶ Y₂) (𝟙 (@rightDual.{v₁, u₁} _ inst inst_1 X _)) (𝟙 Y₂)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X₁ X₂ Y : C
p₁ : ExactPairing X₁ Y
p₂ : ExactPairing X₂ Y
rw : Eq.{v₁ + 1} (α := X₁ ⟶ X₁) (𝟙 (@leftDual.{v₁, u₁} _ inst inst_1 Y _)) (𝟙 X₁)
⊢ Eq.{v₁ + 1} (α := X₁ ⟶ X₁) (CategoryStruct.comp (Y := X₂) (ᘁ𝟙 Y) (ᘁ𝟙 Y) : X₁ ⟶ X₁) (𝟙 X₁ : X₁ ⟶ X₁)

Tactic:
rw [← @comp_leftAdjointMate C, Category.comp_id, @leftAdjointMate_id]

Premises used: CategoryTheory.leftAdjointMate_id, CategoryTheory.Category.comp_id, CategoryTheory.comp_leftAdjointMate
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X₁ X₂ Y : C
p₁ : ExactPairing X₁ Y
p₂ : ExactPairing X₂ Y
⊢ Eq.{v₁ + 1} (α := X₁ ⟶ X₁) (𝟙 (@leftDual.{v₁, u₁} _ inst inst_1 Y _)) (𝟙 X₁)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X₁ X₂ Y : C
p₁ : ExactPairing X₁ Y
p₂ : ExactPairing X₂ Y
rw : Eq.{v₁ + 1} (α := X₂ ⟶ X₂) (𝟙 (@leftDual.{v₁, u₁} _ inst inst_1 Y _)) (𝟙 X₂)
⊢ Eq.{v₁ + 1} (α := X₂ ⟶ X₂) (CategoryStruct.comp (Y := X₁) (ᘁ𝟙 Y) (ᘁ𝟙 Y) : X₂ ⟶ X₂) (𝟙 X₂ : X₂ ⟶ X₂)

Tactic:
rw [← @comp_leftAdjointMate C, Category.comp_id, @leftAdjointMate_id]

Premises used: CategoryTheory.leftAdjointMate_id, CategoryTheory.Category.comp_id, CategoryTheory.comp_leftAdjointMate
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X₁ X₂ Y : C
p₁ : ExactPairing X₁ Y
p₂ : ExactPairing X₂ Y
⊢ Eq.{v₁ + 1} (α := X₂ ⟶ X₂) (𝟙 (@leftDual.{v₁, u₁} _ inst inst_1 Y _)) (𝟙 X₂)

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y : C
p : ExactPairing X Y
w : (rightDualIso p p).hom = Iso.hom (Iso.refl Y)
⊢ rightDualIso p p = Iso.refl Y

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y : C
p : ExactPairing X Y
⊢ (rightDualIso p p).hom = Iso.hom (Iso.refl Y)

Tactic:
simp only [rightDualIso, Iso.refl_hom, @rightAdjointMate_id]

Premises used: CategoryTheory.rightDualIso, CategoryTheory.rightAdjointMate_id, CategoryTheory.Iso.refl_hom
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y : C
p : ExactPairing X Y
w : (leftDualIso p p).hom = Iso.hom (Iso.refl X)
⊢ leftDualIso p p = Iso.refl X

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Monoidal.Rigid.Basic
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y : C
p : ExactPairing X Y
⊢ (leftDualIso p p).hom = Iso.hom (Iso.refl X)

Tactic:
simp only [leftDualIso, Iso.refl_hom, @leftAdjointMate_id]

Premises used: CategoryTheory.leftDualIso, CategoryTheory.leftAdjointMate_id, CategoryTheory.Iso.refl_hom
-- 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} (α := X ⟶ X)
    (CategoryStruct.comp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) X (tensorUnit.{v_1, u_1} C (𝒞 := inst_1)))
      (Iso.inv (ρ_ X))
      ((X ◁ (η_ X Y ≫ Iso.inv (β_ Y X)) ≫ Iso.inv (α_ X Y X) ≫ (Iso.hom (β_ X Y) ≫ ε_ X Y) ▷ X) ≫ Iso.hom (λ_ X)))
    (𝟙 X)
⊢ Eq.{v_1 + 1} (α :=
    tensorObj.{v_1, u_1} (𝒞 := inst_1) X (tensorUnit.{v_1, u_1} C (𝒞 := inst_1)) ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorUnit.{v_1, u_1} C (𝒞 := inst_1)) X)
    (X ◁ (η_ X Y ≫ Iso.inv (β_ Y X)) ≫ Iso.inv (α_ X Y X) ≫ (Iso.hom (β_ X Y) ≫ ε_ X Y) ▷ X)
    (Iso.hom (ρ_ X) ≫ Iso.inv (λ_ X))

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} (α := X ⟶ X)
    (CategoryStruct.comp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) X (tensorUnit.{v_1, u_1} C (𝒞 := inst_1)))
      (Iso.inv (ρ_ X))
      ((X ◁ (η_ X Y ≫ Iso.inv (β_ Y X)) ≫ Iso.inv (α_ X Y X) ≫ (Iso.hom (β_ X Y) ≫ ε_ X Y) ▷ X) ≫ Iso.hom (λ_ 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) X Y)) (X ◁ η_ X Y)
        (monoidalComp (X := tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X) X) (Y :=
          tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X) X)
          (X ◁ Iso.inv (β_ Y X) ⊗≫ Iso.hom (β_ X Y) ▷ X) (ε_ X Y ▷ X ⊗≫ 𝟙 X))))

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 :
  X ◁ Iso.inv (β_ Y X) ⊗≫ Iso.hom (β_ X Y) ▷ 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)))))
⊢ Eq.{v_1 + 1} (α := 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) X Y)) (X ◁ η_ X Y)
        (monoidalComp (X := tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X) X) (Y :=
          tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X) X)
          (X ◁ Iso.inv (β_ Y X) ⊗≫ Iso.hom (β_ X Y) ▷ X) (ε_ X Y ▷ X ⊗≫ 𝟙 X))))
    (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)))

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

Tactic:
simp only [monoidalComp, MonoidalCoherence.assoc'_iso, MonoidalCoherence.whiskerRight_iso,
        MonoidalCoherence.refl_iso, whiskerRightIso_refl, Iso.refl_trans, Iso.symm_hom,
        MonoidalCoherence.assoc_iso, Iso.trans_refl, 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) 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) X Y) ⟶
      tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X) X)
    (X ◁ Iso.inv (β_ Y X) ≫ Iso.inv (α_ X Y X) ≫ Iso.hom (β_ X 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.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) 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:
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:
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