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) 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: 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) 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) (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]
-- 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) (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)
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) (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]
-- 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) (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))
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 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))
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) 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))
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) X Y))
  ((((Y ◁ Iso.hom (β_ X Y) ≫ inv (Iso.hom (α_ Y Y X))) ≫ inv (Iso.inv (β_ Y Y) ▷ X)) ≫ inv (Iso.inv (α_ Y Y X))) ≫
    inv (Y ◁ Iso.inv (β_ 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))
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) 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) X Y))
  ((((Y ◁ Iso.hom (β_ X Y) ≫ inv (Iso.hom (α_ Y Y X))) ≫ inv (Iso.inv (β_ Y Y) ▷ X)) ≫ inv (Iso.inv (α_ Y Y X))) ≫
    inv (Y ◁ Iso.inv (β_ 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))
Tactic: iterate 4 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) (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) Y X) Y)
        (η_ X Y ▷ Y ≫ Iso.hom (β_ (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y) Y))
        ((Iso.inv (β_ Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X)) ≫ Y ◁ ε_ X Y) ⊗≫ 𝟙 Y)) =
    𝟙 Y
have rw : 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) Y X) Y)
      (Iso.hom (β_ (tensorUnit.{v_1, u_1} C (𝒞 := inst_1)) Y) ≫ Y ◁ η_ X Y)
      ((ε_ X Y ▷ Y ≫ Iso.inv (β_ Y (tensorUnit.{v_1, u_1} C (𝒞 := inst_1)))) ⊗≫ 𝟙 Y)) =
  𝟙 Y
Tactic: rw [braiding_naturality_left, ← braiding_inv_naturality_left]
-- 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)
    (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)
have _ : Eq.{v_1 + 1} (α := Y ⟶ Y)
  (CategoryStruct.comp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorUnit.{v_1, u_1} C (𝒞 := inst_1)) Y)
    (Iso.inv (λ_ Y))
    (((η_ X Y ≫ Iso.inv (β_ Y X)) ▷ Y ≫ Iso.hom (α_ Y X Y) ≫ Y ◁ (Iso.hom (β_ X Y) ≫ ε_ X Y)) ≫ Iso.hom (ρ_ Y)))
  (monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorUnit.{v_1, u_1} C (𝒞 := inst_1)) Y) (𝟙 Y)
    (monoidalComp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) (tensorObj.{v_1, u_1} (𝒞 := inst_1) X Y) Y) (η_ X Y ▷ Y)
      (CategoryStruct.comp (Y := tensorObj.{v_1, u_1} (𝒞 := inst_1) Y (tensorObj.{v_1, u_1} (𝒞 := inst_1) Y X))
        (Iso.inv (β_ Y X) ▷ Y ⊗≫ Y ◁ Iso.hom (β_ X Y)) (Y ◁ ε_ X Y ⊗≫ 𝟙 Y))))
Tactic: calc
    _ = 𝟙 Y ⊗≫ η_ X Y ▷ Y ⊗≫ ((β_ Y X).inv ▷ Y ⊗≫ Y ◁ (β_ X Y).hom) ≫ Y ◁ ε_ X Y ⊗≫ 𝟙 Y := by
      monoidal
    _ = 𝟙 Y ⊗≫ η_ X Y ▷ Y ⊗≫ (𝟙 ((X ⊗ Y) ⊗ Y) ⊗≫ X ◁ (β_ Y Y).hom ⊗≫ (β_ X Y).hom ▷ Y
        ⊗≫ Y ◁ (β_ Y X).inv ⊗≫ (β_ Y Y).inv ▷ X ⊗≫ 𝟙 (Y ⊗ Y ⊗ X)) ⊗≫ Y ◁ ε_ X Y ⊗≫ 𝟙 Y := by
      congr 3
      on_goal 2 => simp [monoidalComp]
      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]
      iterate 2 rw [← IsIso.eq_inv_comp]
      repeat rw [← assoc]
      iterate 4 rw [← IsIso.comp_inv_eq]
      simpa using (yang_baxter Y X Y).symm
    _ = 𝟙 Y ⊗≫ (η_ X Y ▷ Y ≫ (β_ (X ⊗ Y) Y).hom) ⊗≫ ((β_ Y (Y ⊗ X)).inv ≫ Y ◁ ε_ X Y) ⊗≫ 𝟙 Y := by
      simp [monoidalComp, braiding_tensor_left_hom, braiding_tensor_right_inv]
    _ = _ := by
      rw [braiding_naturality_left, ← braiding_inv_naturality_left]
      simp [monoidalComp]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Rigid.FunctorCategory (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Groupoid.{u_3, u_1} C
inst_1 : Category.{v_1, u_2} D
inst_2 : MonoidalCategory.{v_1, u_2} D
inst_3 : RightRigidCategory.{v_1, u_2} D
F : Functor.{u_3, v_1, u_1, u_2} C D
X Y : C
f : X ⟶ Y
⊢ Functor.map ((𝟙_ (Functor.{u_3, v_1, u_1, u_2} C D)) (𝒞 := Functor.category)) f ≫
      η_ (F.obj Y)
        (Functor.obj.{u_3, v_1, u_1, u_2}
          { obj := fun (X : C) ↦ @HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _,
            map := fun {X Y : C} (f : X ⟶ Y) ↦ F.map (inv f)ᘁ, map_id := ⋯, map_comp := ⋯ }
          Y) =
    η_ (F.obj X)
        (Functor.obj.{u_3, v_1, u_1, u_2}
          { obj := fun (X : C) ↦ @HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _,
            map := fun {X Y : C} (f : X ⟶ Y) ↦ F.map (inv f)ᘁ, map_id := ⋯, map_comp := ⋯ :
            Functor.{u_3, v_1, u_1, u_2} C D }
          X) ≫
      (tensorObj (𝒞 := Functor.category) F
            { obj := fun (X : C) ↦ @HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _,
              map := fun {X Y : C} (f : X ⟶ Y) ↦ F.map (inv f)ᘁ, map_id := ⋯, map_comp := ⋯ :
              Functor.{u_3, v_1, u_1, u_2} C D }).map
        f
have dsimp : Eq (α :=
  tensorUnit.{v_1, u_2} D (𝒞 := inst_1) ⟶
    tensorObj.{v_1, u_2} (𝒞 := inst_1) (F.obj Y) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _))
  (𝟙 (tensorUnit.{v_1, u_2} D (𝒞 := inst_1)) ≫
    η_ (F.obj Y) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _))
  (CategoryStruct.comp (Y :=
    tensorObj.{v_1, u_2} (𝒞 := inst_1) (F.obj X) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _))
    (η_ (F.obj X) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _)) (F.map f ⊗ₘ F.map (inv f)ᘁ))
Tactic: dsimp
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Rigid.FunctorCategory (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Groupoid.{u_3, u_1} C
inst_1 : Category.{v_1, u_2} D
inst_2 : MonoidalCategory.{v_1, u_2} D
inst_3 : RightRigidCategory.{v_1, u_2} D
F : Functor.{u_3, v_1, u_1, u_2} C D
X Y : C
f : X ⟶ Y
⊢ Eq (α :=
    tensorUnit.{v_1, u_2} D (𝒞 := inst_1) ⟶
      tensorObj.{v_1, u_2} (𝒞 := inst_1) (F.obj Y) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _))
    (𝟙 (tensorUnit.{v_1, u_2} D (𝒞 := inst_1)) ≫
      η_ (F.obj Y) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _))
    (CategoryStruct.comp (Y :=
      tensorObj.{v_1, u_2} (𝒞 := inst_1) (F.obj X) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _))
      (η_ (F.obj X) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _)) (F.map f ⊗ₘ F.map (inv f)ᘁ))
have rw : Eq (α :=
  tensorUnit.{v_1, u_2} D (𝒞 := inst_1) ⟶
    tensorObj.{v_1, u_2} (𝒞 := inst_1) (F.obj Y) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _))
  (𝟙 (tensorUnit.{v_1, u_2} D (𝒞 := inst_1)) ≫
    η_ (F.obj Y) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _))
  (CategoryStruct.comp (Y :=
    tensorObj.{v_1, u_2} (𝒞 := inst_1) (F.obj X) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _))
    (η_ (F.obj X) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _)) (F.map f ⊗ₘ inv (F.map f)ᘁ))
Tactic: rw [Functor.map_inv, Category.id_comp, ← id_tensor_comp_tensor_id,
              id_tensorHom, tensorHom_id, ← Category.assoc,
              coevaluation_comp_rightAdjointMate, Category.assoc, ← comp_whiskerRight,
              IsIso.inv_hom_id, id_whiskerRight, Category.comp_id]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Rigid.FunctorCategory (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Groupoid.{u_3, u_1} C
inst_1 : Category.{v_1, u_2} D
inst_2 : MonoidalCategory.{v_1, u_2} D
inst_3 : RightRigidCategory.{v_1, u_2} D
F : Functor.{u_3, v_1, u_1, u_2} C D
X Y : C
f : X ⟶ Y
rw :
  Eq (α :=
    tensorUnit.{v_1, u_2} D (𝒞 := inst_1) ⟶
      tensorObj.{v_1, u_2} (𝒞 := inst_1) (F.obj Y) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _))
    (𝟙 (tensorUnit.{v_1, u_2} D (𝒞 := inst_1)) ≫
      η_ (F.obj Y) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _))
    (CategoryStruct.comp (Y :=
      tensorObj.{v_1, u_2} (𝒞 := inst_1) (F.obj X) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _))
      (η_ (F.obj X) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _)) (F.map f ⊗ₘ inv (F.map f)ᘁ))
⊢ Eq (α :=
    tensorUnit.{v_1, u_2} D (𝒞 := inst_1) ⟶
      tensorObj.{v_1, u_2} (𝒞 := inst_1) (F.obj Y) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _))
    (𝟙 (tensorUnit.{v_1, u_2} D (𝒞 := inst_1)) ≫
      η_ (F.obj Y) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _))
    (CategoryStruct.comp (Y :=
      tensorObj.{v_1, u_2} (𝒞 := inst_1) (F.obj X) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _))
      (η_ (F.obj X) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _)) (F.map f ⊗ₘ F.map (inv f)ᘁ))
have rw₁ : Eq (α :=
  tensorUnit.{v_1, u_2} D (𝒞 := inst_1) ⟶
    tensorObj.{v_1, u_2} (𝒞 := inst_1) (F.obj Y) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _))
  (η_ (F.obj Y) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj Y) _))
  (CategoryStruct.comp (Y :=
    tensorObj.{v_1, u_2} (𝒞 := inst_1) (F.obj X) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _))
    (η_ (F.obj X) (@HasRightDual.rightDual.{v_1, u_2} _ inst_1 inst_2 (F.obj X) _)) (F.map f ⊗ₘ inv (F.map f)ᘁ))
Tactic: rw [Functor.map_inv, Category.id_comp, ← id_tensor_comp_tensor_id,
              id_tensorHom, tensorHom_id, ← Category.assoc,
              coevaluation_comp_rightAdjointMate, Category.assoc, ← comp_whiskerRight,
              IsIso.inv_hom_id, id_whiskerRight, Category.comp_id]