awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
X X' Y Y' : C
f : X ⟶ Y
g : X' ⟶ Y'
simp_rw :
  Eq (α := tensorObj.{v, u} (𝒞 := inst) X X' ⟶ tensorObj.{v, u} (𝒞 := inst) Y' Y) (X ◁ g ≫ f ▷ Y' ≫ Iso.hom (β_ Y Y'))
    (Iso.hom (β_ X X') ≫ g ▷ X ≫ Y' ◁ f)
⊢ Eq (α := tensorObj.{v, u} (𝒞 := inst) X X' ⟶ tensorObj.{v, u} (𝒞 := inst) Y' Y) ((X ◁ g ≫ f ▷ Y') ≫ Iso.hom (β_ Y Y'))
    (Iso.hom (β_ X X') ≫ g ▷ X ≫ Y' ◁ f)
have simp_rw₁ : Eq (α := tensorObj.{v, u} (𝒞 := inst) X X' ⟶ tensorObj.{v, u} (𝒞 := inst) Y' Y) (X ◁ g ≫ Iso.hom (β_ X Y') ≫ Y' ◁ f)
  (Iso.hom (β_ X X') ≫ g ▷ X ≫ Y' ◁ f)
Tactic: simp_rw [Category.assoc, braiding_naturality_left, braiding_naturality_right_assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
X Y Z : C
⊢ Eq.{v + 1} (α :=
    tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z) ⟶
      tensorObj.{v, u} (𝒞 := inst) Z (tensorObj.{v, u} (𝒞 := inst) Y X))
    (Iso.inv (α_ X Y Z) ≫
      Iso.hom (β_ X Y) ▷ Z ≫
        Iso.hom (α_ Y X Z) ≫ Y ◁ Iso.hom (β_ X Z) ≫ Iso.inv (α_ Y Z X) ≫ Iso.hom (β_ Y Z) ▷ X ≫ Iso.hom (α_ Z Y X))
    (X ◁ Iso.hom (β_ Y Z) ≫ Iso.inv (α_ X Z Y) ≫ Iso.hom (β_ X Z) ▷ Y ≫ Iso.hom (α_ Z X Y) ≫ Z ◁ Iso.hom (β_ X Y))
have rw : Eq.{v + 1} (α :=
  tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z) ⟶
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Z Y) X)
  ((Iso.hom (β_ X (tensorObj.{v, u} (𝒞 := inst) Y Z)) ≫ Iso.hom (β_ Y Z) ▷ X ≫ Iso.hom (α_ Z Y X)) ≫ Iso.inv (α_ Z Y X))
  ((X ◁ Iso.hom (β_ Y Z) ≫ Iso.inv (α_ X Z Y) ≫ Iso.hom (β_ X Z) ▷ Y ≫ Iso.hom (α_ Z X Y) ≫ Z ◁ Iso.hom (β_ X Y)) ≫
    Iso.inv (α_ Z Y X))
Tactic: rw [← braiding_tensor_right_hom_assoc X Y Z, ← cancel_mono (α_ Z Y X).inv]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
X Y Z : C
⊢ Eq.{v + 1} (α :=
    tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z) ⟶
      tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Z Y) X)
    ((Iso.hom (β_ X (tensorObj.{v, u} (𝒞 := inst) Y Z)) ≫ Iso.hom (β_ Y Z) ▷ X ≫ Iso.hom (α_ Z Y X)) ≫
      Iso.inv (α_ Z Y X))
    ((X ◁ Iso.hom (β_ Y Z) ≫ Iso.inv (α_ X Z Y) ≫ Iso.hom (β_ X Z) ▷ Y ≫ Iso.hom (α_ Z X Y) ≫ Z ◁ Iso.hom (β_ X Y)) ≫
      Iso.inv (α_ Z Y X))
have rw : Eq.{v + 1} (α :=
  tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z) ⟶
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Z Y) X)
  (Iso.hom (β_ X (tensorObj.{v, u} (𝒞 := inst) Y Z)) ≫ (Iso.hom (β_ Y Z) ▷ X ≫ Iso.hom (α_ Z Y X)) ≫ Iso.inv (α_ Z Y X))
  ((X ◁ Iso.hom (β_ Y Z) ≫ Iso.inv (α_ X Z Y) ≫ Iso.hom (β_ X Z) ▷ Y ≫ Iso.hom (α_ Z X Y) ≫ Z ◁ Iso.hom (β_ X Y)) ≫
    Iso.inv (α_ Z Y X))
Tactic: rw [assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
X Y Z : C
⊢ Eq.{v + 1} (α :=
    tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z) ⟶
      tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Z Y) X)
    (Iso.hom (β_ X (tensorObj.{v, u} (𝒞 := inst) Y Z)) ≫
      (Iso.hom (β_ Y Z) ▷ X ≫ Iso.hom (α_ Z Y X)) ≫ Iso.inv (α_ Z Y X))
    ((X ◁ Iso.hom (β_ Y Z) ≫ Iso.inv (α_ X Z Y) ≫ Iso.hom (β_ X Z) ▷ Y ≫ Iso.hom (α_ Z X Y) ≫ Z ◁ Iso.hom (β_ X Y)) ≫
      Iso.inv (α_ Z Y X))
have rw : Eq.{v + 1} (α :=
  tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z) ⟶
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Z Y) X)
  (Iso.hom (β_ X (tensorObj.{v, u} (𝒞 := inst) Y Z)) ≫ Iso.hom (β_ Y Z) ▷ X ≫ Iso.hom (α_ Z Y X) ≫ Iso.inv (α_ Z Y X))
  ((X ◁ Iso.hom (β_ Y Z) ≫ Iso.inv (α_ X Z Y) ≫ Iso.hom (β_ X Z) ▷ Y ≫ Iso.hom (α_ Z X Y) ≫ Z ◁ Iso.hom (β_ X Y)) ≫
    Iso.inv (α_ Z Y X))
Tactic: rw [assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
X Y Z : C
⊢ Eq.{v + 1} (α :=
    tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z) ⟶
      tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Z Y) X)
    (Iso.hom (β_ X (tensorObj.{v, u} (𝒞 := inst) Y Z)) ≫ Iso.hom (β_ Y Z) ▷ X ≫ Iso.hom (α_ Z Y X) ≫ Iso.inv (α_ Z Y X))
    ((X ◁ Iso.hom (β_ Y Z) ≫ Iso.inv (α_ X Z Y) ≫ Iso.hom (β_ X Z) ▷ Y ≫ Iso.hom (α_ Z X Y) ≫ Z ◁ Iso.hom (β_ X Y)) ≫
      Iso.inv (α_ Z Y X))
have rw : Eq.{v + 1} (α :=
  tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z) ⟶
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Z Y) X)
  (Iso.hom (β_ X (tensorObj.{v, u} (𝒞 := inst) Y Z)) ≫ Iso.hom (β_ Y Z) ▷ X ≫ Iso.hom (α_ Z Y X) ≫ Iso.inv (α_ Z Y X))
  (X ◁ Iso.hom (β_ Y Z) ≫
    (Iso.inv (α_ X Z Y) ≫ Iso.hom (β_ X Z) ▷ Y ≫ Iso.hom (α_ Z X Y) ≫ Z ◁ Iso.hom (β_ X Y)) ≫ Iso.inv (α_ Z Y X))
Tactic: rw [assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
X Y Z : C
⊢ Eq.{v + 1} (α :=
    tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z) ⟶
      tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Z Y) X)
    (Iso.hom (β_ X (tensorObj.{v, u} (𝒞 := inst) Y Z)) ≫ Iso.hom (β_ Y Z) ▷ X ≫ Iso.hom (α_ Z Y X) ≫ Iso.inv (α_ Z Y X))
    (X ◁ Iso.hom (β_ Y Z) ≫
      (Iso.inv (α_ X Z Y) ≫ Iso.hom (β_ X Z) ▷ Y ≫ Iso.hom (α_ Z X Y) ≫ Z ◁ Iso.hom (β_ X Y)) ≫ Iso.inv (α_ Z Y X))
have rw : Eq.{v + 1} (α :=
  tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z) ⟶
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Z Y) X)
  (Iso.hom (β_ X (tensorObj.{v, u} (𝒞 := inst) Y Z)) ≫ Iso.hom (β_ Y Z) ▷ X ≫ Iso.hom (α_ Z Y X) ≫ Iso.inv (α_ Z Y X))
  (X ◁ Iso.hom (β_ Y Z) ≫
    Iso.inv (α_ X Z Y) ≫ (Iso.hom (β_ X Z) ▷ Y ≫ Iso.hom (α_ Z X Y) ≫ Z ◁ Iso.hom (β_ X Y)) ≫ Iso.inv (α_ Z Y X))
Tactic: rw [assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
X Y Z : C
⊢ Eq.{v + 1} (α :=
    tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z) ⟶
      tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Z Y) X)
    (Iso.hom (β_ X (tensorObj.{v, u} (𝒞 := inst) Y Z)) ≫ Iso.hom (β_ Y Z) ▷ X ≫ Iso.hom (α_ Z Y X) ≫ Iso.inv (α_ Z Y X))
    (X ◁ Iso.hom (β_ Y Z) ≫
      Iso.inv (α_ X Z Y) ≫ (Iso.hom (β_ X Z) ▷ Y ≫ Iso.hom (α_ Z X Y) ≫ Z ◁ Iso.hom (β_ X Y)) ≫ Iso.inv (α_ Z Y X))
have rw : Eq.{v + 1} (α :=
  tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z) ⟶
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Z Y) X)
  (Iso.hom (β_ X (tensorObj.{v, u} (𝒞 := inst) Y Z)) ≫ Iso.hom (β_ Y Z) ▷ X ≫ Iso.hom (α_ Z Y X) ≫ Iso.inv (α_ Z Y X))
  (X ◁ Iso.hom (β_ Y Z) ≫
    Iso.inv (α_ X Z Y) ≫ Iso.hom (β_ X Z) ▷ Y ≫ (Iso.hom (α_ Z X Y) ≫ Z ◁ Iso.hom (β_ X Y)) ≫ Iso.inv (α_ Z Y X))
Tactic: rw [assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
X Y Z : C
⊢ Eq.{v + 1} (α :=
    tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z) ⟶
      tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Z Y) X)
    (Iso.hom (β_ X (tensorObj.{v, u} (𝒞 := inst) Y Z)) ≫ Iso.hom (β_ Y Z) ▷ X ≫ Iso.hom (α_ Z Y X) ≫ Iso.inv (α_ Z Y X))
    (X ◁ Iso.hom (β_ Y Z) ≫
      Iso.inv (α_ X Z Y) ≫ Iso.hom (β_ X Z) ▷ Y ≫ (Iso.hom (α_ Z X Y) ≫ Z ◁ Iso.hom (β_ X Y)) ≫ Iso.inv (α_ Z Y X))
have rw : Eq.{v + 1} (α :=
  tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z) ⟶
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Z Y) X)
  (Iso.hom (β_ X (tensorObj.{v, u} (𝒞 := inst) Y Z)) ≫ Iso.hom (β_ Y Z) ▷ X ≫ Iso.hom (α_ Z Y X) ≫ Iso.inv (α_ Z Y X))
  (X ◁ Iso.hom (β_ Y Z) ≫
    Iso.inv (α_ X Z Y) ≫ Iso.hom (β_ X Z) ▷ Y ≫ Iso.hom (α_ Z X Y) ≫ Z ◁ Iso.hom (β_ X Y) ≫ Iso.inv (α_ Z Y X))
Tactic: rw [assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
X Y Z : C
⊢ Eq.{v + 1} (α :=
    tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z) ⟶
      tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Z Y) X)
    ((Iso.hom (β_ X (tensorObj.{v, u} (𝒞 := inst) Y Z)) ≫ Iso.hom (β_ Y Z) ▷ X ≫ Iso.hom (α_ Z Y X)) ≫
      Iso.inv (α_ Z Y X))
    ((X ◁ Iso.hom (β_ Y Z) ≫ Iso.inv (α_ X Z Y) ≫ Iso.hom (β_ X Z) ▷ Y ≫ Iso.hom (α_ Z X Y) ≫ Z ◁ Iso.hom (β_ X Y)) ≫
      Iso.inv (α_ Z Y X))
have repeat : Eq.{v + 1} (α :=
  tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z) ⟶
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Z Y) X)
  (Iso.hom (β_ X (tensorObj.{v, u} (𝒞 := inst) Y Z)) ≫ Iso.hom (β_ Y Z) ▷ X ≫ Iso.hom (α_ Z Y X) ≫ Iso.inv (α_ Z Y X))
  (X ◁ Iso.hom (β_ Y Z) ≫
    Iso.inv (α_ X Z Y) ≫ Iso.hom (β_ X Z) ▷ Y ≫ Iso.hom (α_ Z X Y) ≫ Z ◁ Iso.hom (β_ X Y) ≫ Iso.inv (α_ Z Y X))
Tactic: repeat rw [assoc]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
X Y Z : C
⊢ Eq.{v + 1} (α :=
    tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z) ⟶
      tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Z Y) X)
    (Iso.hom (β_ X (tensorObj.{v, u} (𝒞 := inst) Y Z)) ≫ Iso.hom (β_ Y Z) ▷ X ≫ Iso.hom (α_ Z Y X) ≫ Iso.inv (α_ Z Y X))
    (X ◁ Iso.hom (β_ Y Z) ≫
      Iso.inv (α_ X Z Y) ≫ Iso.hom (β_ X Z) ▷ Y ≫ Iso.hom (α_ Z X Y) ≫ Z ◁ Iso.hom (β_ X Y) ≫ Iso.inv (α_ Z Y X))
have rw : Iso.hom (β_ X (tensorObj.{v, u} (𝒞 := inst) Y Z)) ≫
    Iso.hom (β_ Y Z) ▷ X ≫ 𝟙 (tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Z Y) X) =
  X ◁ Iso.hom (β_ Y Z) ≫
    Iso.inv (α_ X Z Y) ≫ Iso.hom (β_ X Z) ▷ Y ≫ Iso.hom (α_ Z X Y) ≫ Z ◁ Iso.hom (β_ X Y) ≫ Iso.inv (α_ Z Y X)
Tactic: rw [Iso.hom_inv_id, comp_id, ← braiding_naturality_right, braiding_tensor_right_hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
X Y Z : C
rw :
  Iso.hom (β_ X (tensorObj.{v, u} (𝒞 := inst) Y Z)) ≫
      Iso.hom (β_ Y Z) ▷ X ≫ 𝟙 (tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Z Y) X) =
    X ◁ Iso.hom (β_ Y Z) ≫
      Iso.inv (α_ X Z Y) ≫ Iso.hom (β_ X Z) ▷ Y ≫ Iso.hom (α_ Z X Y) ≫ Z ◁ Iso.hom (β_ X Y) ≫ Iso.inv (α_ Z Y X)
⊢ Eq.{v + 1} (α :=
    tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z) ⟶
      tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Z Y) X)
    (Iso.hom (β_ X (tensorObj.{v, u} (𝒞 := inst) Y Z)) ≫ Iso.hom (β_ Y Z) ▷ X ≫ Iso.hom (α_ Z Y X) ≫ Iso.inv (α_ Z Y X))
    (X ◁ Iso.hom (β_ Y Z) ≫
      Iso.inv (α_ X Z Y) ≫ Iso.hom (β_ X Z) ▷ Y ≫ Iso.hom (α_ Z X Y) ≫ Z ◁ Iso.hom (β_ X Y) ≫ Iso.inv (α_ Z Y X))
have rw₁ : Eq.{v + 1} (α :=
  tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z) ⟶
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Z Y) X)
  (Iso.hom (β_ X (tensorObj.{v, u} (𝒞 := inst) Y Z)) ≫ Iso.hom (β_ Y Z) ▷ X)
  (X ◁ Iso.hom (β_ Y Z) ≫
    Iso.inv (α_ X Z Y) ≫ Iso.hom (β_ X Z) ▷ Y ≫ Iso.hom (α_ Z X Y) ≫ Z ◁ Iso.hom (β_ X Y) ≫ Iso.inv (α_ Z Y X))
Tactic: rw [Iso.hom_inv_id, comp_id, ← braiding_naturality_right, braiding_tensor_right_hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
X Y Z : C
rw :
  Iso.hom (β_ X (tensorObj.{v, u} (𝒞 := inst) Y Z)) ≫
      Iso.hom (β_ Y Z) ▷ X ≫ 𝟙 (tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Z Y) X) =
    X ◁ Iso.hom (β_ Y Z) ≫
      Iso.inv (α_ X Z Y) ≫ Iso.hom (β_ X Z) ▷ Y ≫ Iso.hom (α_ Z X Y) ≫ Z ◁ Iso.hom (β_ X Y) ≫ Iso.inv (α_ Z Y X)
rw₁ :
  Eq.{v + 1} (α :=
    tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z) ⟶
      tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Z Y) X)
    (Iso.hom (β_ X (tensorObj.{v, u} (𝒞 := inst) Y Z)) ≫ Iso.hom (β_ Y Z) ▷ X)
    (X ◁ Iso.hom (β_ Y Z) ≫
      Iso.inv (α_ X Z Y) ≫ Iso.hom (β_ X Z) ▷ Y ≫ Iso.hom (α_ Z X Y) ≫ Z ◁ Iso.hom (β_ X Y) ≫ Iso.inv (α_ Z Y X))
⊢ Eq.{v + 1} (α :=
    tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z) ⟶
      tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Z Y) X)
    (Iso.hom (β_ X (tensorObj.{v, u} (𝒞 := inst) Y Z)) ≫ Iso.hom (β_ Y Z) ▷ X ≫ Iso.hom (α_ Z Y X) ≫ Iso.inv (α_ Z Y X))
    (X ◁ Iso.hom (β_ Y Z) ≫
      Iso.inv (α_ X Z Y) ≫ Iso.hom (β_ X Z) ▷ Y ≫ Iso.hom (α_ Z X Y) ≫ Z ◁ Iso.hom (β_ X Y) ≫ Iso.inv (α_ Z Y X))
have rw₂ : Eq.{v + 1} (α :=
  tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z) ⟶
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Z Y) X)
  (X ◁ Iso.hom (β_ Y Z) ≫ Iso.hom (β_ X (tensorObj.{v, u} (𝒞 := inst) Z Y)))
  (X ◁ Iso.hom (β_ Y Z) ≫
    Iso.inv (α_ X Z Y) ≫ Iso.hom (β_ X Z) ▷ Y ≫ Iso.hom (α_ Z X Y) ≫ Z ◁ Iso.hom (β_ X Y) ≫ Iso.inv (α_ Z Y X))
Tactic: rw [Iso.hom_inv_id, comp_id, ← braiding_naturality_right, braiding_tensor_right_hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
X Y Z : C
rw :
  Iso.hom (β_ X (tensorObj.{v, u} (𝒞 := inst) Y Z)) ≫
      Iso.hom (β_ Y Z) ▷ X ≫ 𝟙 (tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Z Y) X) =
    X ◁ Iso.hom (β_ Y Z) ≫
      Iso.inv (α_ X Z Y) ≫ Iso.hom (β_ X Z) ▷ Y ≫ Iso.hom (α_ Z X Y) ≫ Z ◁ Iso.hom (β_ X Y) ≫ Iso.inv (α_ Z Y X)
rw₁ :
  Eq.{v + 1} (α :=
    tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z) ⟶
      tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Z Y) X)
    (Iso.hom (β_ X (tensorObj.{v, u} (𝒞 := inst) Y Z)) ≫ Iso.hom (β_ Y Z) ▷ X)
    (X ◁ Iso.hom (β_ Y Z) ≫
      Iso.inv (α_ X Z Y) ≫ Iso.hom (β_ X Z) ▷ Y ≫ Iso.hom (α_ Z X Y) ≫ Z ◁ Iso.hom (β_ X Y) ≫ Iso.inv (α_ Z Y X))
rw₂ :
  Eq.{v + 1} (α :=
    tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z) ⟶
      tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Z Y) X)
    (X ◁ Iso.hom (β_ Y Z) ≫ Iso.hom (β_ X (tensorObj.{v, u} (𝒞 := inst) Z Y)))
    (X ◁ Iso.hom (β_ Y Z) ≫
      Iso.inv (α_ X Z Y) ≫ Iso.hom (β_ X Z) ▷ Y ≫ Iso.hom (α_ Z X Y) ≫ Z ◁ Iso.hom (β_ X Y) ≫ Iso.inv (α_ Z Y X))
⊢ Eq.{v + 1} (α :=
    tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z) ⟶
      tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Z Y) X)
    (Iso.hom (β_ X (tensorObj.{v, u} (𝒞 := inst) Y Z)) ≫ Iso.hom (β_ Y Z) ▷ X ≫ Iso.hom (α_ Z Y X) ≫ Iso.inv (α_ Z Y X))
    (X ◁ Iso.hom (β_ Y Z) ≫
      Iso.inv (α_ X Z Y) ≫ Iso.hom (β_ X Z) ▷ Y ≫ Iso.hom (α_ Z X Y) ≫ Z ◁ Iso.hom (β_ X Y) ≫ Iso.inv (α_ Z Y X))
have rw₃ : Eq.{v + 1} (α :=
  tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z) ⟶
    tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Z Y) X)
  (X ◁ Iso.hom (β_ Y Z) ≫
    Iso.inv (α_ X Z Y) ≫ Iso.hom (β_ X Z) ▷ Y ≫ Iso.hom (α_ Z X Y) ≫ Z ◁ Iso.hom (β_ X Y) ≫ Iso.inv (α_ Z Y X))
  (X ◁ Iso.hom (β_ Y Z) ≫
    Iso.inv (α_ X Z Y) ≫ Iso.hom (β_ X Z) ▷ Y ≫ Iso.hom (α_ Z X Y) ≫ Z ◁ Iso.hom (β_ X Y) ≫ Iso.inv (α_ Z Y X))
Tactic: rw [Iso.hom_inv_id, comp_id, ← braiding_naturality_right, braiding_tensor_right_hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
X Y Z : C
⊢ monoidalComp (Y := tensorObj.{v, u} (𝒞 := inst) Y (tensorObj.{v, u} (𝒞 := inst) X Z)) (Iso.hom (β_ X Y) ▷ Z)
      (Y ◁ Iso.hom (β_ X Z) ⊗≫ Iso.hom (β_ Y Z) ▷ X) =
    monoidalComp (Y := tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z))
      (𝟙 (tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) X Y) Z))
      (monoidalComp (X := tensorObj.{v, u} (𝒞 := inst) Z (tensorObj.{v, u} (𝒞 := inst) Y X))
        (monoidalComp (Y := tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) X Z) Y) (X ◁ Iso.hom (β_ Y Z))
          (Iso.hom (β_ X Z) ▷ Y ⊗≫ Z ◁ Iso.hom (β_ X Y)))
        (𝟙 (tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Z Y) X)))
have rw : (Iso.inv (α_ X Y Z) ≫
      monoidalComp (Y := tensorObj.{v, u} (𝒞 := inst) Y (tensorObj.{v, u} (𝒞 := inst) X Z)) (Iso.hom (β_ X Y) ▷ Z)
        (Y ◁ Iso.hom (β_ X Z) ⊗≫ Iso.hom (β_ Y Z) ▷ X)) ≫
    Iso.hom (α_ Z Y X) =
  (Iso.inv (α_ X Y Z) ≫
      monoidalComp (Y := tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z))
        (𝟙 (tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) X Y) Z))
        (monoidalComp (X := tensorObj.{v, u} (𝒞 := inst) Z (tensorObj.{v, u} (𝒞 := inst) Y X))
          (monoidalComp (Y := tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) X Z) Y) (X ◁ Iso.hom (β_ Y Z))
            (Iso.hom (β_ X Z) ▷ Y ⊗≫ Z ◁ Iso.hom (β_ X Y)))
          (𝟙 (tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Z Y) X)))) ≫
    Iso.hom (α_ Z Y X)
Tactic: rw [← cancel_epi (α_ X Y Z).inv, ← cancel_mono (α_ Z Y X).hom]
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
X Y Z : C
⊢ (Iso.inv (α_ X Y Z) ≫
        monoidalComp (Y := tensorObj.{v, u} (𝒞 := inst) Y (tensorObj.{v, u} (𝒞 := inst) X Z)) (Iso.hom (β_ X Y) ▷ Z)
          (Y ◁ Iso.hom (β_ X Z) ⊗≫ Iso.hom (β_ Y Z) ▷ X)) ≫
      Iso.hom (α_ Z Y X) =
    (Iso.inv (α_ X Y Z) ≫
        monoidalComp (Y := tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z))
          (𝟙 (tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) X Y) Z))
          (monoidalComp (X := tensorObj.{v, u} (𝒞 := inst) Z (tensorObj.{v, u} (𝒞 := inst) Y X))
            (monoidalComp (Y := tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) X Z) Y)
              (X ◁ Iso.hom (β_ Y Z)) (Iso.hom (β_ X Z) ▷ Y ⊗≫ Z ◁ Iso.hom (β_ X Y)))
            (𝟙 (tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Z Y) X)))) ≫
      Iso.hom (α_ Z Y X)
have h : Eq.{v + 1} (α :=
  tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z) ⟶
    tensorObj.{v, u} (𝒞 := inst) Z (tensorObj.{v, u} (𝒞 := inst) Y X))
  ((Iso.inv (α_ X Y Z) ≫
      monoidalComp (Y := tensorObj.{v, u} (𝒞 := inst) Y (tensorObj.{v, u} (𝒞 := inst) X Z)) (Iso.hom (β_ X Y) ▷ Z)
        (Y ◁ Iso.hom (β_ X Z) ⊗≫ Iso.hom (β_ Y Z) ▷ X)) ≫
    Iso.hom (α_ Z Y X))
  (Iso.inv (α_ X Y Z) ≫
    Iso.hom (β_ X Y) ▷ Z ≫
      Iso.hom (α_ Y X Z) ≫ Y ◁ Iso.hom (β_ X Z) ≫ Iso.inv (α_ Y Z X) ≫ Iso.hom (β_ Y Z) ▷ X ≫ Iso.hom (α_ Z Y X))
Tactic: convert! yang_baxter X Y Z using 1
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Basic (goal)
Goal:
C : Type u
inst : Category.{v, u} C
inst_1 : MonoidalCategory.{v, u} C
inst_2 : BraidedCategory.{v, u} C
X Y Z : C
h :
  Eq.{v + 1} (α :=
    tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z) ⟶
      tensorObj.{v, u} (𝒞 := inst) Z (tensorObj.{v, u} (𝒞 := inst) Y X))
    ((Iso.inv (α_ X Y Z) ≫
        monoidalComp (Y := tensorObj.{v, u} (𝒞 := inst) Y (tensorObj.{v, u} (𝒞 := inst) X Z)) (Iso.hom (β_ X Y) ▷ Z)
          (Y ◁ Iso.hom (β_ X Z) ⊗≫ Iso.hom (β_ Y Z) ▷ X)) ≫
      Iso.hom (α_ Z Y X))
    (Iso.inv (α_ X Y Z) ≫
      Iso.hom (β_ X Y) ▷ Z ≫
        Iso.hom (α_ Y X Z) ≫ Y ◁ Iso.hom (β_ X Z) ≫ Iso.inv (α_ Y Z X) ≫ Iso.hom (β_ Y Z) ▷ X ≫ Iso.hom (α_ Z Y X))
⊢ (Iso.inv (α_ X Y Z) ≫
        monoidalComp (Y := tensorObj.{v, u} (𝒞 := inst) Y (tensorObj.{v, u} (𝒞 := inst) X Z)) (Iso.hom (β_ X Y) ▷ Z)
          (Y ◁ Iso.hom (β_ X Z) ⊗≫ Iso.hom (β_ Y Z) ▷ X)) ≫
      Iso.hom (α_ Z Y X) =
    (Iso.inv (α_ X Y Z) ≫
        monoidalComp (Y := tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z))
          (𝟙 (tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) X Y) Z))
          (monoidalComp (X := tensorObj.{v, u} (𝒞 := inst) Z (tensorObj.{v, u} (𝒞 := inst) Y X))
            (monoidalComp (Y := tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) X Z) Y)
              (X ◁ Iso.hom (β_ Y Z)) (Iso.hom (β_ X Z) ▷ Y ⊗≫ Z ◁ Iso.hom (β_ X Y)))
            (𝟙 (tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Z Y) X)))) ≫
      Iso.hom (α_ Z Y X)
have h₁ : (Iso.inv (α_ X Y Z) ≫
      monoidalComp (Y := tensorObj.{v, u} (𝒞 := inst) X (tensorObj.{v, u} (𝒞 := inst) Y Z))
        (𝟙 (tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) X Y) Z))
        (monoidalComp (X := tensorObj.{v, u} (𝒞 := inst) Z (tensorObj.{v, u} (𝒞 := inst) Y X))
          (monoidalComp (Y := tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) X Z) Y) (X ◁ Iso.hom (β_ Y Z))
            (Iso.hom (β_ X Z) ▷ Y ⊗≫ Z ◁ Iso.hom (β_ X Y)))
          (𝟙 (tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) Z Y) X)))) ≫
    Iso.hom (α_ Z Y X) =
  X ◁ Iso.hom (β_ Y Z) ≫ Iso.inv (α_ X Z Y) ≫ Iso.hom (β_ X Z) ▷ Y ≫ Iso.hom (α_ Z X Y) ≫ Z ◁ Iso.hom (β_ X Y)
Tactic: convert! yang_baxter X Y Z using 1
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Basic (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalCategory.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Monoidal
inst_5 : F.Faithful
inst_6 : BraidedCategory.{v_2, u_2} D
β : (X Y : C) → tensorObj.{v_1, u_1} (𝒞 := inst) X Y ≅ tensorObj.{v_1, u_1} (𝒞 := inst) Y X
w :
  ∀ (X Y : C),
    Eq (α := tensorObj.{v_2, u_2} (𝒞 := inst_1) (F.obj X) (F.obj Y) ⟶ F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) Y X))
      (μ F X Y ≫ F.map (β X Y).hom) (Iso.hom (β_ (F.obj X) (F.obj Y)) ≫ μ F Y X)
X Y Z : C
f : Y ⟶ Z
⊢ X ◁ f ≫ (β X Z).hom = (β X Y).hom ≫ f ▷ X
have a : F.map (X ◁ f ≫ (β X Z).hom) = F.map ((β X Y).hom ≫ f ▷ X)
Tactic: apply F.map_injective
-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Braided.Basic (goal)
Goal:
C : Type u_1
D : Type u_2
inst : Category.{v_1, u_1} C
inst_1 : Category.{v_2, u_2} D
inst_2 : MonoidalCategory.{v_1, u_1} C
inst_3 : MonoidalCategory.{v_2, u_2} D
F : Functor.{v_1, v_2, u_1, u_2} C D
inst_4 : F.Monoidal
inst_5 : F.Faithful
inst_6 : BraidedCategory.{v_2, u_2} D
β : (X Y : C) → tensorObj.{v_1, u_1} (𝒞 := inst) X Y ≅ tensorObj.{v_1, u_1} (𝒞 := inst) Y X
w :
  ∀ (X Y : C),
    Eq (α := tensorObj.{v_2, u_2} (𝒞 := inst_1) (F.obj X) (F.obj Y) ⟶ F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) Y X))
      (μ F X Y ≫ F.map (β X Y).hom) (Iso.hom (β_ (F.obj X) (F.obj Y)) ≫ μ F Y X)
X Y Z : C
f : Y ⟶ Z
⊢ F.map (X ◁ f ≫ (β X Z).hom) = F.map ((β X Y).hom ≫ f ▷ X)
have a : Eq (α := tensorObj.{v_2, u_2} (𝒞 := inst_1) (F.obj X) (F.obj Y) ⟶ F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) Z X))
  (μ F X Y ≫ F.map (X ◁ f ≫ (β X Z).hom)) (μ F X Y ≫ F.map ((β X Y).hom ≫ f ▷ X))
Tactic: refine (cancel_epi (μ F ?_ ?_)).1 ?_