awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Rigid.Braided (goal)
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) (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))
have 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))
Tactic: iterate 5 rw [← IsIso.comp_inv_eq]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Rigid.Braided (goal)
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))
        (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
have 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
Tactic: rw [braiding_naturality_right, ← braiding_inv_naturality_right]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Rigid.Braided (goal)
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)))
    (𝟙 X)
have _ : 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: calc
    _ = 𝟙 X ⊗≫ X ◁ η_ X Y ⊗≫ (X ◁ (β_ Y X).inv ⊗≫ (β_ X Y).hom ▷ X) ⊗≫ ε_ X Y ▷ X ⊗≫ 𝟙 X := by
      monoidal
    _ = 𝟙 X ⊗≫ X ◁ η_ X Y ⊗≫ (𝟙 (X ⊗ X ⊗ Y) ⊗≫ (β_ X X).hom ▷ Y ⊗≫ X ◁ (β_ X Y).hom
          ⊗≫ (β_ Y X).inv ▷ X ⊗≫ Y ◁ (β_ X X).inv ⊗≫ 𝟙 ((Y ⊗ X) ⊗ X)) ⊗≫ ε_ X Y ▷ X ⊗≫ 𝟙 X := by
      congr 3
      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]
      rw [← IsIso.eq_inv_comp]
      repeat rw [← assoc]
      iterate 5 rw [← IsIso.comp_inv_eq]
      simpa using yang_baxter X Y X
    _ = 𝟙 X ⊗≫ (X ◁ η_ X Y ≫ (β_ X (X ⊗ Y)).hom) ⊗≫ ((β_ (Y ⊗ X) X).inv ≫ ε_ X Y ▷ X) ⊗≫ 𝟙 X := by
      simp [monoidalComp, braiding_tensor_right_hom, braiding_tensor_left_inv]
    _ = _ := by
      rw [braiding_naturality_right, ← braiding_inv_naturality_right]
      simp [monoidalComp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Rigid.Braided (goal)
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) (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))
have 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)
Tactic: rw [Iso.eq_comp_inv, ← Iso.inv_comp_eq_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Rigid.Braided (goal)
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)
    (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)))
have 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))))))
Tactic: congr 3
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Rigid.Braided (goal)
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))))))
⊢ 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)))
have 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))
Tactic: congr 3
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Rigid.Braided (goal)
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
⊢ 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))))))
have 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))
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]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Rigid.Braided (goal)
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) (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))
have 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))
Tactic: rw [← IsIso.eq_inv_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Rigid.Braided (goal)
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) (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))
have 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))
Tactic: rw [← IsIso.eq_inv_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Rigid.Braided (goal)
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) (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))
have 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))
Tactic: iterate 2 rw [← IsIso.eq_inv_comp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Rigid.Braided (goal)
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) 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))
have 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))
Tactic: rw [← assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Rigid.Braided (goal)
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) 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))
have 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))
Tactic: rw [← assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Rigid.Braided (goal)
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) 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))
have 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))
Tactic: rw [← assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Rigid.Braided (goal)
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) 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))
have 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))
Tactic: rw [← assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Rigid.Braided (goal)
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) 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))
have 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))
Tactic: rw [← assoc]