awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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.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:
(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
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))
⊢ 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:
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
⊢ 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:
(cancel_epi (μ F _ _ ▷ _)).1 ?_

Premises used: CategoryTheory.MonoidalCategoryStruct.whiskerRight, 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
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))
⊢ 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 ?_

Premises used: CategoryTheory.MonoidalCategoryStruct.whiskerRight, 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
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)
⊢ 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

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.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:
(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
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))
⊢ 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:
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
⊢ 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:
(cancel_epi (_ ◁ μ F _ _)).1 ?_

Premises used: CategoryTheory.MonoidalCategoryStruct.whiskerLeft, 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
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))
⊢ 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 ?_

Premises used: CategoryTheory.MonoidalCategoryStruct.whiskerLeft, CategoryTheory.Functor.LaxMonoidal.μ, Iff.mp, CategoryTheory.cancel_epi
-- 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 : C
⊢ 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 (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ▷ X ≫ Iso.inv (β_ X (tensorUnit.{v₁, u₁} C (𝒞 := inst)))

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 : C
⊢ Eq (α :=
    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))) ▷ tensorUnit.{v₁, u₁} C (𝒞 := inst) ≫
      Iso.hom (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) 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))

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 : C
⊢ Eq (α :=
    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 (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) 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 (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
        tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ Iso.hom (β_ X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
          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))

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 : C
⊢ Eq (α :=
    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 (α_ (tensorUnit.{v₁, u₁} C (𝒞 := inst)) X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
        tensorUnit.{v₁, u₁} C (𝒞 := inst) ◁ Iso.hom (β_ X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫
          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)) (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))

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 : C
rw 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))))
⊢ 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)))

Tactic:
rw [braiding_leftUnitor_aux₁]

Premises used: CategoryTheory.braiding_leftUnitor_aux₁
-- 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 : C
a : X ◁ Iso.hom (λ_ (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ Iso.hom (β_ X (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

Tactic:
rw [← braiding_naturality_right]

Premises used: CategoryTheory.BraidedCategory.braiding_naturality_right
-- 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 : C
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))))
⊢ 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))))

Tactic:
slice_lhs 2 3 => rw [← braiding_naturality_right]

Premises used: CategoryTheory.BraidedCategory.braiding_naturality_right
-- 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 : 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))) ≫
        Iso.hom (β_ X (tensorUnit.{v₁, u₁} C (𝒞 := inst))) ≫ Iso.inv (β_ X (tensorUnit.{v₁, u₁} C (𝒞 := inst))))

Tactic:
simp only [assoc]

Premises used: CategoryTheory.Category.assoc