awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : C
f : X ⟶ Y
Z : C
a :
  Eq (α := tensorObj.{v_2, u_2} (𝒞 := inst_1) (F.obj X) (F.obj Z) ⟶ F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) Z Y))
    (μ F X Z ≫ F.map (f ▷ Z) ≫ F.map (β Y Z).hom) (μ F X Z ≫ F.map ((β X Z).hom ≫ Z ◁ f))
a₁ :
  Eq (α := tensorObj.{v_2, u_2} (𝒞 := inst_1) (F.obj X) (F.obj Z) ⟶ F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) Z Y))
    (F.map f ▷ F.obj Z ≫ μ F Y Z ≫ F.map (β Y Z).hom) (μ F X Z ≫ F.map ((β X Z).hom ≫ Z ◁ f))
a₂ :
  Eq (α := tensorObj.{v_2, u_2} (𝒞 := inst_1) (F.obj X) (F.obj Z) ⟶ F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) Z Y))
    (F.map f ▷ F.obj Z ≫ Iso.hom (β_ (F.obj Y) (F.obj Z)) ≫ μ F Z Y) (μ F X Z ≫ F.map ((β X Z).hom ≫ Z ◁ f))
a₃ :
  Eq (α := tensorObj.{v_2, u_2} (𝒞 := inst_1) (F.obj X) (F.obj Z) ⟶ F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) Z Y))
    (F.map f ▷ F.obj Z ≫ Iso.hom (β_ (F.obj Y) (F.obj Z)) ≫ μ F Z Y) (μ F X Z ≫ F.map (β X Z).hom ≫ F.map (Z ◁ f))
a₄ :
  Eq (α := tensorObj.{v_2, u_2} (𝒞 := inst_1) (F.obj X) (F.obj Z) ⟶ F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) Z Y))
    (F.map f ▷ F.obj Z ≫ Iso.hom (β_ (F.obj Y) (F.obj Z)) ≫ μ F Z Y)
    (Iso.hom (β_ (F.obj X) (F.obj Z)) ≫ μ F Z X ≫ F.map (Z ◁ f))
⊢ Eq (α := tensorObj.{v_2, u_2} (𝒞 := inst_1) (F.obj X) (F.obj Z) ⟶ F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) Z Y))
    (μ F X Z ≫ F.map (f ▷ Z ≫ (β Y Z).hom)) (μ F X Z ≫ F.map ((β X Z).hom ≫ Z ◁ f))
have a₅ : Eq (α := tensorObj.{v_2, u_2} (𝒞 := inst_1) (F.obj X) (F.obj Z) ⟶ F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) Z Y))
  (Iso.hom (β_ (F.obj X) (F.obj Z)) ≫ F.obj Z ◁ F.map f ≫ μ F Z Y)
  (Iso.hom (β_ (F.obj X) (F.obj Z)) ≫ μ F Z X ≫ F.map (Z ◁ f))
Tactic: rw [Functor.map_comp, ← μ_natural_left_assoc, w, Functor.map_comp,
      reassoc_of% w, braiding_naturality_left_assoc, μ_natural_right]
-- 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 : C
f : X ⟶ Y
Z : C
a :
  Eq (α := tensorObj.{v_2, u_2} (𝒞 := inst_1) (F.obj X) (F.obj Z) ⟶ F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) Z Y))
    (μ F X Z ≫ F.map (f ▷ Z) ≫ F.map (β Y Z).hom) (μ F X Z ≫ F.map ((β X Z).hom ≫ Z ◁ f))
a₁ :
  Eq (α := tensorObj.{v_2, u_2} (𝒞 := inst_1) (F.obj X) (F.obj Z) ⟶ F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) Z Y))
    (F.map f ▷ F.obj Z ≫ μ F Y Z ≫ F.map (β Y Z).hom) (μ F X Z ≫ F.map ((β X Z).hom ≫ Z ◁ f))
a₂ :
  Eq (α := tensorObj.{v_2, u_2} (𝒞 := inst_1) (F.obj X) (F.obj Z) ⟶ F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) Z Y))
    (F.map f ▷ F.obj Z ≫ Iso.hom (β_ (F.obj Y) (F.obj Z)) ≫ μ F Z Y) (μ F X Z ≫ F.map ((β X Z).hom ≫ Z ◁ f))
a₃ :
  Eq (α := tensorObj.{v_2, u_2} (𝒞 := inst_1) (F.obj X) (F.obj Z) ⟶ F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) Z Y))
    (F.map f ▷ F.obj Z ≫ Iso.hom (β_ (F.obj Y) (F.obj Z)) ≫ μ F Z Y) (μ F X Z ≫ F.map (β X Z).hom ≫ F.map (Z ◁ f))
a₄ :
  Eq (α := tensorObj.{v_2, u_2} (𝒞 := inst_1) (F.obj X) (F.obj Z) ⟶ F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) Z Y))
    (F.map f ▷ F.obj Z ≫ Iso.hom (β_ (F.obj Y) (F.obj Z)) ≫ μ F Z Y)
    (Iso.hom (β_ (F.obj X) (F.obj Z)) ≫ μ F Z X ≫ F.map (Z ◁ f))
a₅ :
  Eq (α := tensorObj.{v_2, u_2} (𝒞 := inst_1) (F.obj X) (F.obj Z) ⟶ F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) Z Y))
    (Iso.hom (β_ (F.obj X) (F.obj Z)) ≫ F.obj Z ◁ F.map f ≫ μ F Z Y)
    (Iso.hom (β_ (F.obj X) (F.obj Z)) ≫ μ F Z X ≫ F.map (Z ◁ f))
⊢ Eq (α := tensorObj.{v_2, u_2} (𝒞 := inst_1) (F.obj X) (F.obj Z) ⟶ F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) Z Y))
    (μ F X Z ≫ F.map (f ▷ Z ≫ (β Y Z).hom)) (μ F X Z ≫ F.map ((β X Z).hom ≫ Z ◁ f))
have a₆ : Eq (α := tensorObj.{v_2, u_2} (𝒞 := inst_1) (F.obj X) (F.obj Z) ⟶ F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) Z Y))
  (Iso.hom (β_ (F.obj X) (F.obj Z)) ≫ μ F Z X ≫ F.map (Z ◁ f))
  (Iso.hom (β_ (F.obj X) (F.obj Z)) ≫ μ F Z X ≫ F.map (Z ◁ f))
Tactic: rw [Functor.map_comp, ← μ_natural_left_assoc, w, Functor.map_comp,
      reassoc_of% w, braiding_naturality_left_assoc, μ_natural_right]
-- 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
⊢ Iso.hom (α_ X Y Z) ≫ Iso.hom (β X (tensorObj.{v_1, u_1} (𝒞 := inst) Y Z)) ≫ Iso.hom (α_ Y Z X) =
    (β X Y).hom ▷ Z ≫ Iso.hom (α_ Y X Z) ≫ Y ◁ (β X Z).hom
have a : F.map (Iso.hom (α_ X Y Z) ≫ Iso.hom (β X (tensorObj.{v_1, u_1} (𝒞 := inst) Y Z)) ≫ Iso.hom (α_ Y Z X)) =
  F.map ((β X Y).hom ▷ Z ≫ Iso.hom (α_ Y X Z) ≫ Y ◁ (β X Z).hom)
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.map (Iso.hom (α_ X Y Z) ≫ Iso.hom (β X (tensorObj.{v_1, u_1} (𝒞 := inst) Y Z)) ≫ Iso.hom (α_ Y Z X)) =
    F.map ((β X Y).hom ▷ Z ≫ Iso.hom (α_ Y X Z) ≫ Y ◁ (β X Z).hom)
have a : Eq (α :=
  tensorObj.{v_2, u_2} (𝒞 := inst_1) (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) X Y)) (F.obj Z) ⟶
    F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) Y (tensorObj.{v_1, u_1} (𝒞 := inst) Z X)))
  (μ F (tensorObj.{v_1, u_1} (𝒞 := inst) X Y) Z ≫
    F.map (Iso.hom (α_ X Y Z) ≫ Iso.hom (β X (tensorObj.{v_1, u_1} (𝒞 := inst) Y Z)) ≫ Iso.hom (α_ Y Z X)))
  (μ F (tensorObj.{v_1, u_1} (𝒞 := inst) X Y) Z ≫ F.map ((β X Y).hom ▷ Z ≫ Iso.hom (α_ Y X Z) ≫ Y ◁ (β X Z).hom))
Tactic: refine (cancel_epi (μ F _ _)).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
⊢ Eq (α :=
    tensorObj.{v_2, u_2} (𝒞 := inst_1) (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) X Y)) (F.obj Z) ⟶
      F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) Y (tensorObj.{v_1, u_1} (𝒞 := inst) Z X)))
    (μ F (tensorObj.{v_1, u_1} (𝒞 := inst) X Y) Z ≫
      F.map (Iso.hom (α_ X Y Z) ≫ Iso.hom (β X (tensorObj.{v_1, u_1} (𝒞 := inst) Y Z)) ≫ Iso.hom (α_ Y Z X)))
    (μ F (tensorObj.{v_1, u_1} (𝒞 := inst) X Y) Z ≫ F.map ((β X Y).hom ▷ Z ≫ Iso.hom (α_ Y X Z) ≫ Y ◁ (β X Z).hom))
have a : Eq (α :=
  tensorObj.{v_2, u_2} (𝒞 := inst_1) (tensorObj.{v_2, u_2} (𝒞 := inst_1) (F.obj X) (F.obj Y)) (F.obj Z) ⟶
    F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) Y (tensorObj.{v_1, u_1} (𝒞 := inst) Z X)))
  (μ F X Y ▷ F.obj Z ≫
    μ F (tensorObj.{v_1, u_1} (𝒞 := inst) X Y) Z ≫
      F.map (Iso.hom (α_ X Y Z) ≫ Iso.hom (β X (tensorObj.{v_1, u_1} (𝒞 := inst) Y Z)) ≫ Iso.hom (α_ Y Z X)))
  (μ F X Y ▷ F.obj Z ≫
    μ F (tensorObj.{v_1, u_1} (𝒞 := inst) X Y) Z ≫ F.map ((β X Y).hom ▷ Z ≫ Iso.hom (α_ Y X Z) ≫ Y ◁ (β X Z).hom))
Tactic: refine (cancel_epi (μ F _ _ ▷ _)).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
⊢ Iso.inv (α_ X Y Z) ≫ Iso.hom (β (tensorObj.{v_1, u_1} (𝒞 := inst) X Y) Z) ≫ Iso.inv (α_ Z X Y) =
    X ◁ (β Y Z).hom ≫ Iso.inv (α_ X Z Y) ≫ (β X Z).hom ▷ Y
have a : F.map (Iso.inv (α_ X Y Z) ≫ Iso.hom (β (tensorObj.{v_1, u_1} (𝒞 := inst) X Y) Z) ≫ Iso.inv (α_ Z X Y)) =
  F.map (X ◁ (β Y Z).hom ≫ Iso.inv (α_ X Z Y) ≫ (β X Z).hom ▷ Y)
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.map (Iso.inv (α_ X Y Z) ≫ Iso.hom (β (tensorObj.{v_1, u_1} (𝒞 := inst) X Y) Z) ≫ Iso.inv (α_ Z X Y)) =
    F.map (X ◁ (β Y Z).hom ≫ Iso.inv (α_ X Z Y) ≫ (β X Z).hom ▷ Y)
have a : Eq (α :=
  tensorObj.{v_2, u_2} (𝒞 := inst_1) (F.obj X) (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) Y Z)) ⟶
    F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) Z X) Y))
  (μ F X (tensorObj.{v_1, u_1} (𝒞 := inst) Y Z) ≫
    F.map (Iso.inv (α_ X Y Z) ≫ Iso.hom (β (tensorObj.{v_1, u_1} (𝒞 := inst) X Y) Z) ≫ Iso.inv (α_ Z X Y)))
  (μ F X (tensorObj.{v_1, u_1} (𝒞 := inst) Y Z) ≫ F.map (X ◁ (β Y Z).hom ≫ Iso.inv (α_ X Z Y) ≫ (β X Z).hom ▷ Y))
Tactic: refine (cancel_epi (μ F _ _)).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
⊢ Eq (α :=
    tensorObj.{v_2, u_2} (𝒞 := inst_1) (F.obj X) (F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) Y Z)) ⟶
      F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) Z X) Y))
    (μ F X (tensorObj.{v_1, u_1} (𝒞 := inst) Y Z) ≫
      F.map (Iso.inv (α_ X Y Z) ≫ Iso.hom (β (tensorObj.{v_1, u_1} (𝒞 := inst) X Y) Z) ≫ Iso.inv (α_ Z X Y)))
    (μ F X (tensorObj.{v_1, u_1} (𝒞 := inst) Y Z) ≫ F.map (X ◁ (β Y Z).hom ≫ Iso.inv (α_ X Z Y) ≫ (β X Z).hom ▷ Y))
have a : Eq (α :=
  tensorObj.{v_2, u_2} (𝒞 := inst_1) (F.obj X) (tensorObj.{v_2, u_2} (𝒞 := inst_1) (F.obj Y) (F.obj Z)) ⟶
    F.obj (tensorObj.{v_1, u_1} (𝒞 := inst) (tensorObj.{v_1, u_1} (𝒞 := inst) Z X) Y))
  (F.obj X ◁ μ F Y Z ≫
    μ F X (tensorObj.{v_1, u_1} (𝒞 := inst) Y Z) ≫
      F.map (Iso.inv (α_ X Y Z) ≫ Iso.hom (β (tensorObj.{v_1, u_1} (𝒞 := inst) X Y) Z) ≫ Iso.inv (α_ Z X Y)))
  (F.obj X ◁ μ F Y Z ≫
    μ F X (tensorObj.{v_1, u_1} (𝒞 := inst) Y Z) ≫ F.map (X ◁ (β Y Z).hom ≫ Iso.inv (α_ X Z Y) ≫ (β X Z).hom ▷ Y))
Tactic: refine (cancel_epi (_ ◁ μ F _ _)).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 : C
⊢ Iso.hom (α_ X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
      Iso.hom
          (β_ X
            (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) ≫
        Iso.hom (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X) ≫
          tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ Iso.inv (β_ X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
            Iso.inv (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
              Iso.hom (λ_ X) ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) =
    Iso.hom (α_ X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
      Iso.hom
          (β_ X
            (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) ≫
        Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ▷ X ≫ Iso.inv (β_ X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
have rw : Eq.{v₁ + 1} (α :=
  tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
      (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶
    tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
  (Iso.hom (α_ X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
    Iso.hom
        (β_ X
          (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) ≫
      Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ▷ X ≫ Iso.inv (β_ X (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
  (Iso.hom (α_ X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
    Iso.hom
        (β_ X
          (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) ≫
      Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ▷ X ≫ Iso.inv (β_ X (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
Tactic: rw [braiding_leftUnitor_aux₁]
-- 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 : C
| Iso.hom
      (β_ X (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) ≫
    Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ▷ X
have a : X ◁ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ Iso.hom (β_ X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
Tactic: rw [← braiding_naturality_right]
-- 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 : C
⊢ Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
        (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (Iso.hom (α_ X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
      Iso.hom
          (β_ X
            (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) ≫
        Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ▷ X ≫ Iso.inv (β_ X (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
    (Iso.hom (α_ X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
      X ◁ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
        Iso.hom (β_ X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ Iso.inv (β_ X (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
have slice_lhs : Eq.{v₁ + 1} (α :=
  tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
      (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶
    tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
  (Iso.hom (α_ X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
    (X ◁ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ Iso.hom (β_ X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))) ≫
      Iso.inv (β_ X (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
  (Iso.hom (α_ X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
    X ◁ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
      Iso.hom (β_ X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ Iso.inv (β_ X (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
Tactic: slice_lhs 2 3 => rw [← braiding_naturality_right]
-- 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 : C
⊢ Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
        (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (Iso.hom (α_ X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
      X ◁ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
        Iso.hom (β_ X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ Iso.inv (β_ X (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
    (Iso.hom (α_ X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
      X ◁ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
have rw : Iso.hom (α_ X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
    X ◁ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
      𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) =
  Iso.hom (α_ X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
    X ◁ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
Tactic: rw [Iso.hom_inv_id, comp_id]
-- 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 : C
rw :
  Iso.hom (α_ X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
      X ◁ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
        𝟙 (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) =
    Iso.hom (α_ X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
      X ◁ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
⊢ Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
        (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (Iso.hom (α_ X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
      X ◁ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
        Iso.hom (β_ X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ Iso.inv (β_ X (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
    (Iso.hom (α_ X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
      X ◁ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
have rw₁ : Eq.{v₁ + 1} (α :=
  tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
      (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶
    tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
  (Iso.hom (α_ X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
    X ◁ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
  (Iso.hom (α_ X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
    X ◁ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
Tactic: rw [Iso.hom_inv_id, comp_id]
-- 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 : C
⊢ Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
        (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (Iso.hom (α_ X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
      X ◁ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))))
    (Iso.hom (ρ_ X) ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst))
have rw : Eq.{v₁ + 1} (α :=
  tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
      (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶
    tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
  (Iso.hom (ρ_ X) ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst)) (Iso.hom (ρ_ X) ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst))
Tactic: rw [triangle]
-- 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 : C
⊢ Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ X)
    (Iso.hom (β_ X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ Iso.hom (λ_ X)) (Iso.hom (ρ_ X))
have rw : Eq.{v₁ + 1} (α :=
  tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
      (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶
    tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
  ((Iso.hom (β_ X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ Iso.hom (λ_ X)) ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst))
  (Iso.hom (ρ_ X) ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst))
Tactic: rw [← whiskerRight_iff, comp_whiskerRight, braiding_leftUnitor_aux₂]
-- 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 : C
rw :
  Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
        (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶
      tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    ((Iso.hom (β_ X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ Iso.hom (λ_ X)) ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst))
    (Iso.hom (ρ_ X) ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst))
⊢ Eq.{v₁ + 1} (α := tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶ X)
    (Iso.hom (β_ X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ Iso.hom (λ_ X)) (Iso.hom (ρ_ X))
have rw₁ : Eq.{v₁ + 1} (α :=
  tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
      (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶
    tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
  (Iso.hom (β_ X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫
    Iso.hom (λ_ X) ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst))
  (Iso.hom (ρ_ X) ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst))
Tactic: rw [← whiskerRight_iff, comp_whiskerRight, braiding_leftUnitor_aux₂]