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 Z : C
f : Y ⟶ Z
⊢ 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))
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) ≫ F.map (β X Z).hom) (μ F X Y ≫ F.map ((β X Y).hom ≫ f ▷ X))
Tactic: rw [Functor.map_comp, ← μ_natural_right_assoc, w, Functor.map_comp,
      reassoc_of% w, braiding_naturality_right_assoc, μ_natural_left]
-- 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
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) ≫ F.map (β X Z).hom) (μ F X Y ≫ F.map ((β X Y).hom ≫ f ▷ X))
⊢ 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))
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.obj X ◁ F.map f ≫ μ F X Z ≫ F.map (β X Z).hom) (μ F X Y ≫ F.map ((β X Y).hom ≫ f ▷ X))
Tactic: rw [Functor.map_comp, ← μ_natural_right_assoc, w, Functor.map_comp,
      reassoc_of% w, braiding_naturality_right_assoc, μ_natural_left]
-- 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
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) ≫ F.map (β X Z).hom) (μ F X Y ≫ F.map ((β X Y).hom ≫ f ▷ X))
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.obj X ◁ F.map f ≫ μ F X Z ≫ F.map (β X Z).hom) (μ F X Y ≫ F.map ((β X Y).hom ≫ f ▷ X))
⊢ 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))
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.obj X ◁ F.map f ≫ Iso.hom (β_ (F.obj X) (F.obj Z)) ≫ μ F Z X) (μ F X Y ≫ F.map ((β X Y).hom ≫ f ▷ X))
Tactic: rw [Functor.map_comp, ← μ_natural_right_assoc, w, Functor.map_comp,
      reassoc_of% w, braiding_naturality_right_assoc, μ_natural_left]
-- 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
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) ≫ F.map (β X Z).hom) (μ F X Y ≫ F.map ((β X Y).hom ≫ f ▷ X))
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.obj X ◁ F.map f ≫ μ F X Z ≫ F.map (β X Z).hom) (μ F X Y ≫ F.map ((β X Y).hom ≫ f ▷ X))
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.obj X ◁ F.map f ≫ Iso.hom (β_ (F.obj X) (F.obj Z)) ≫ μ F Z X) (μ F X Y ≫ F.map ((β X Y).hom ≫ f ▷ X))
⊢ 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))
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.obj X ◁ F.map f ≫ Iso.hom (β_ (F.obj X) (F.obj Z)) ≫ μ F Z X) (μ F X Y ≫ F.map (β X Y).hom ≫ F.map (f ▷ X))
Tactic: rw [Functor.map_comp, ← μ_natural_right_assoc, w, Functor.map_comp,
      reassoc_of% w, braiding_naturality_right_assoc, μ_natural_left]
-- 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
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) ≫ F.map (β X Z).hom) (μ F X Y ≫ F.map ((β X Y).hom ≫ f ▷ X))
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.obj X ◁ F.map f ≫ μ F X Z ≫ F.map (β X Z).hom) (μ F X Y ≫ F.map ((β X Y).hom ≫ f ▷ X))
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.obj X ◁ F.map f ≫ Iso.hom (β_ (F.obj X) (F.obj Z)) ≫ μ F Z X) (μ F X Y ≫ F.map ((β X Y).hom ≫ f ▷ X))
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.obj X ◁ F.map f ≫ Iso.hom (β_ (F.obj X) (F.obj Z)) ≫ μ F Z X) (μ F X Y ≫ F.map (β X Y).hom ≫ F.map (f ▷ X))
⊢ 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))
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.obj X ◁ F.map f ≫ Iso.hom (β_ (F.obj X) (F.obj Z)) ≫ μ F Z X)
  (Iso.hom (β_ (F.obj X) (F.obj Y)) ≫ μ F Y X ≫ F.map (f ▷ X))
Tactic: rw [Functor.map_comp, ← μ_natural_right_assoc, w, Functor.map_comp,
      reassoc_of% w, braiding_naturality_right_assoc, μ_natural_left]
-- 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
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) ≫ F.map (β X Z).hom) (μ F X Y ≫ F.map ((β X Y).hom ≫ f ▷ X))
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.obj X ◁ F.map f ≫ μ F X Z ≫ F.map (β X Z).hom) (μ F X Y ≫ F.map ((β X Y).hom ≫ f ▷ X))
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.obj X ◁ F.map f ≫ Iso.hom (β_ (F.obj X) (F.obj Z)) ≫ μ F Z X) (μ F X Y ≫ F.map ((β X Y).hom ≫ f ▷ X))
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.obj X ◁ F.map f ≫ Iso.hom (β_ (F.obj X) (F.obj Z)) ≫ μ F Z X) (μ F X Y ≫ F.map (β X Y).hom ≫ F.map (f ▷ X))
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.obj X ◁ F.map f ≫ Iso.hom (β_ (F.obj X) (F.obj Z)) ≫ μ F Z X)
    (Iso.hom (β_ (F.obj X) (F.obj Y)) ≫ μ F Y X ≫ F.map (f ▷ X))
⊢ 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))
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))
  (Iso.hom (β_ (F.obj X) (F.obj Y)) ≫ F.map f ▷ F.obj X ≫ μ F Z X)
  (Iso.hom (β_ (F.obj X) (F.obj Y)) ≫ μ F Y X ≫ F.map (f ▷ X))
Tactic: rw [Functor.map_comp, ← μ_natural_right_assoc, w, Functor.map_comp,
      reassoc_of% w, braiding_naturality_right_assoc, μ_natural_left]
-- 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
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) ≫ F.map (β X Z).hom) (μ F X Y ≫ F.map ((β X Y).hom ≫ f ▷ X))
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.obj X ◁ F.map f ≫ μ F X Z ≫ F.map (β X Z).hom) (μ F X Y ≫ F.map ((β X Y).hom ≫ f ▷ X))
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.obj X ◁ F.map f ≫ Iso.hom (β_ (F.obj X) (F.obj Z)) ≫ μ F Z X) (μ F X Y ≫ F.map ((β X Y).hom ≫ f ▷ X))
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.obj X ◁ F.map f ≫ Iso.hom (β_ (F.obj X) (F.obj Z)) ≫ μ F Z X) (μ F X Y ≫ F.map (β X Y).hom ≫ F.map (f ▷ X))
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.obj X ◁ F.map f ≫ Iso.hom (β_ (F.obj X) (F.obj Z)) ≫ μ F Z X)
    (Iso.hom (β_ (F.obj X) (F.obj Y)) ≫ μ F Y X ≫ F.map (f ▷ X))
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))
    (Iso.hom (β_ (F.obj X) (F.obj Y)) ≫ F.map f ▷ F.obj X ≫ μ F Z X)
    (Iso.hom (β_ (F.obj X) (F.obj Y)) ≫ μ F Y X ≫ F.map (f ▷ X))
⊢ 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))
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))
  (Iso.hom (β_ (F.obj X) (F.obj Y)) ≫ μ F Y X ≫ F.map (f ▷ X))
  (Iso.hom (β_ (F.obj X) (F.obj Y)) ≫ μ F Y X ≫ F.map (f ▷ X))
Tactic: rw [Functor.map_comp, ← μ_natural_right_assoc, w, Functor.map_comp,
      reassoc_of% w, braiding_naturality_right_assoc, μ_natural_left]
-- 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
⊢ f ▷ Z ≫ (β Y Z).hom = (β X Z).hom ≫ Z ◁ f
have a : F.map (f ▷ Z ≫ (β Y Z).hom) = F.map ((β X Z).hom ≫ Z ◁ f)
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 : C
f : X ⟶ Y
Z : C
⊢ F.map (f ▷ Z ≫ (β Y Z).hom) = 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))
  (μ F X Z ≫ F.map (f ▷ Z ≫ (β Y Z).hom)) (μ F X Z ≫ F.map ((β X Z).hom ≫ Z ◁ f))
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 : C
f : X ⟶ Y
Z : C
⊢ 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))
  (μ F X Z ≫ F.map (f ▷ Z) ≫ F.map (β Y Z).hom) (μ F X Z ≫ F.map ((β X Z).hom ≫ 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))
⊢ 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))
  (F.map f ▷ F.obj Z ≫ μ F Y Z ≫ F.map (β Y Z).hom) (μ F X Z ≫ F.map ((β X Z).hom ≫ 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))
⊢ 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))
  (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))
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))
⊢ 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))
  (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))
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))
⊢ 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))
  (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))
Tactic: rw [Functor.map_comp, ← μ_natural_left_assoc, w, Functor.map_comp,
      reassoc_of% w, braiding_naturality_left_assoc, μ_natural_right]