awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
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))
rw₃ 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))
⊢ 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 [Iso.hom_inv_id, comp_id, ← braiding_naturality_right, braiding_tensor_right_hom]

Premises used: CategoryTheory.BraidedCategory.braiding_naturality_right, CategoryTheory.BraidedCategory.braiding_tensor_right_hom, CategoryTheory.Iso.hom_inv_id, CategoryTheory.Category.comp_id
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
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.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)
⊢ 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)))

Tactic:
rw [← cancel_epi (α_ X Y Z).inv, ← cancel_mono (α_ Z Y X).hom]

Premises used: CategoryTheory.cancel_mono, CategoryTheory.MonoidalCategoryStruct.associator, CategoryTheory.cancel_epi, CategoryTheory.Iso.hom, CategoryTheory.Iso.inv
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
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))

Tactic:
yang_baxter X Y Z

Premises used: CategoryTheory.BraidedCategory.yang_baxter
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
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))
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)
⊢ (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:
convert! yang_baxter X Y Z using 1

Premises used: CategoryTheory.BraidedCategory.yang_baxter
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
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) ≫
        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:
monoidal
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
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) 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:
monoidal
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
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.symm (α_ X Y Z) ≪≫ β_ X Y ▷ᵢ Z ≪≫ α_ Y X Z ≪≫ Y ◁ᵢ β_ X Z ≪≫ Iso.symm (α_ Y Z X) ≪≫ β_ Y Z ▷ᵢ X ≪≫ α_ Z Y X)
    (X ◁ᵢ β_ Y Z ≪≫ Iso.symm (α_ X Z Y) ≪≫ β_ X Z ▷ᵢ Y ≪≫ α_ Z X Y ≪≫ Z ◁ᵢ β_ X Y)

Tactic:
Iso.ext (yang_baxter X Y Z)

Premises used: CategoryTheory.BraidedCategory.yang_baxter, CategoryTheory.Iso.ext
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
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) (tensorObj.{v, u} (𝒞 := inst) X Y) Z ≅
      tensorObj.{v, u} (𝒞 := inst) Y (tensorObj.{v, u} (𝒞 := inst) Z X))
    (α_ X Y Z ≪≫ β_ X (tensorObj.{v, u} (𝒞 := inst) Y Z) ≪≫ α_ Y Z X) (β_ X Y ▷ᵢ Z ≪≫ α_ Y X Z ≪≫ Y ◁ᵢ β_ X Z)

Tactic:
Iso.ext (hexagon_forward X Y Z)

Premises used: CategoryTheory.BraidedCategory.hexagon_forward, CategoryTheory.Iso.ext
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
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.symm (α_ X Y Z) ≪≫ β_ (tensorObj.{v, u} (𝒞 := inst) X Y) Z ≪≫ Iso.symm (α_ Z X Y) =
    X ◁ᵢ β_ Y Z ≪≫ Iso.symm (α_ X Z Y) ≪≫ β_ X Z ▷ᵢ Y

Tactic:
Iso.ext (hexagon_reverse X Y Z)

Premises used: CategoryTheory.BraidedCategory.hexagon_reverse, CategoryTheory.Iso.ext
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
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) Y (tensorObj.{v, u} (𝒞 := inst) Z X) ⟶
      tensorObj.{v, u} (𝒞 := inst) (tensorObj.{v, u} (𝒞 := inst) X Y) Z)
    (Iso.inv (α_ Y Z X) ≫ Iso.inv (β_ X (tensorObj.{v, u} (𝒞 := inst) Y Z)) ≫ Iso.inv (α_ X Y Z))
    (Y ◁ Iso.inv (β_ X Z) ≫ Iso.inv (α_ Y X Z) ≫ Iso.inv (β_ X Y) ▷ Z)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
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.hom (α_ Z X Y) ≫ Iso.inv (β_ (tensorObj.{v, u} (𝒞 := inst) X Y) Z) ≫ Iso.hom (α_ X Y Z) =
    Iso.inv (β_ X Z) ▷ Y ≫ Iso.hom (α_ X Z Y) ≫ X ◁ Iso.inv (β_ Y Z)

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
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 : F.map (X ◁ f ≫ (β X Z).hom) = F.map ((β X Y).hom ≫ f ▷ X)
⊢ X ◁ f ≫ (β X Z).hom = (β X Y).hom ≫ f ▷ X

Tactic:
apply F.map_injective

Premises used: CategoryTheory.Functor.map_injective
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
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)

Tactic:
(cancel_epi (μ F ?_ ?_)).1 ?_

Premises used: CategoryTheory.Functor.LaxMonoidal.μ, Iff.mp, CategoryTheory.cancel_epi
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
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 ≫ (β X Z).hom)) (μ F X Y ≫ F.map ((β X Y).hom ≫ f ▷ X))
⊢ F.map (X ◁ f ≫ (β X Z).hom) = F.map ((β X Y).hom ≫ f ▷ X)

Tactic:
refine (cancel_epi (μ F ?_ ?_)).1 ?_

Premises used: CategoryTheory.Functor.LaxMonoidal.μ, Iff.mp, CategoryTheory.cancel_epi
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
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))
a₆ 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))
⊢ 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:
rw [Functor.map_comp, ← μ_natural_right_assoc, w, Functor.map_comp,
      reassoc_of% w, braiding_naturality_right_assoc, μ_natural_left]

Premises used: CategoryTheory.Functor.LaxMonoidal.μ_natural_right_assoc, CategoryTheory.Functor.LaxMonoidal.μ_natural_left, CategoryTheory.Functor.map_comp, CategoryTheory.BraidedCategory.braiding_naturality_right_assoc
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
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 : F.map (f ▷ Z ≫ (β Y Z).hom) = F.map ((β X Z).hom ≫ Z ◁ f)
⊢ f ▷ Z ≫ (β Y Z).hom = (β X Z).hom ≫ Z ◁ f

Tactic:
apply F.map_injective

Premises used: CategoryTheory.Functor.map_injective
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
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)

Tactic:
(cancel_epi (μ F ?_ ?_)).1 ?_

Premises used: CategoryTheory.Functor.LaxMonoidal.μ, Iff.mp, CategoryTheory.cancel_epi
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
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 ≫ (β Y Z).hom)) (μ F X Z ≫ F.map ((β X Z).hom ≫ Z ◁ f))
⊢ F.map (f ▷ Z ≫ (β Y Z).hom) = F.map ((β X Z).hom ≫ Z ◁ f)

Tactic:
refine (cancel_epi (μ F ?_ ?_)).1 ?_

Premises used: CategoryTheory.Functor.LaxMonoidal.μ, Iff.mp, CategoryTheory.cancel_epi
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
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))
a₆ 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))
⊢ 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:
rw [Functor.map_comp, ← μ_natural_left_assoc, w, Functor.map_comp,
      reassoc_of% w, braiding_naturality_left_assoc, μ_natural_right]

Premises used: CategoryTheory.Functor.LaxMonoidal.μ_natural_right, CategoryTheory.Functor.LaxMonoidal.μ_natural_left_assoc, CategoryTheory.BraidedCategory.braiding_naturality_left_assoc, CategoryTheory.Functor.map_comp
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
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
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)
⊢ 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

Tactic:
apply F.map_injective

Premises used: CategoryTheory.Functor.map_injective