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} (α := 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)))
have 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)))))
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
⊢ 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)))))
have 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))
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]
-- 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) 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))
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) (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.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) 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) (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]
-- 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) (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]
-- 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) (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]
-- 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) (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]
-- 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) (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]
-- 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) (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]
-- 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) (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]
-- 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) (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]
-- 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) (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]
-- 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) 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]
-- 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) 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))
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) 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]
-- 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) 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))
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) (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]
-- 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 (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)
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) (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]
-- 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) 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))
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: rw [← IsIso.comp_inv_eq]