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₁ X₂ X₃ Y₁ Y₂ Y₃ : C
⊢ (Iso.hom
          (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂) X₃
            (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ Y₂) Y₃)) ≫
        tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂ ◁ Iso.inv (α_ X₃ (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ Y₂) Y₃) ≫
          tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂ ◁
              (Iso.inv (α_ X₃ Y₁ Y₂) ≫
                  Iso.hom (β_ X₃ Y₁) ▷ Y₂ ≫ Iso.hom (α_ Y₁ X₃ Y₂) ≫ Y₁ ◁ Iso.hom (β_ X₃ Y₂) ≫ Iso.inv (α_ Y₁ Y₂ X₃)) ▷
                Y₃ ≫
            tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂ ◁ Iso.hom (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ Y₂) X₃ Y₃) ≫
              Iso.inv
                (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ Y₂)
                  (tensorObj.{v₁, u₁} (𝒞 := inst) X₃ Y₃))) ≫
      (Iso.hom (α_ X₁ X₂ (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ Y₂)) ≫
            X₁ ◁ Iso.inv (α_ X₂ Y₁ Y₂) ≫
              X₁ ◁ Iso.hom (β_ X₂ Y₁) ▷ Y₂ ≫
                X₁ ◁ Iso.hom (α_ Y₁ X₂ Y₂) ≫ Iso.inv (α_ X₁ Y₁ (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ Y₂))) ▷
          tensorObj.{v₁, u₁} (𝒞 := inst) X₃ Y₃ ≫
        Iso.hom
          (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ Y₁) (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ Y₂)
            (tensorObj.{v₁, u₁} (𝒞 := inst) X₃ Y₃)) =
    monoidalComp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) X₁
        (tensorObj.{v₁, u₁} (𝒞 := inst) X₂
          (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₃ Y₁) Y₂)
            Y₃)))
      (𝟙
        (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂) X₃)
          (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ Y₂) Y₃)))
      (monoidalComp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) X₁
          (tensorObj.{v₁, u₁} (𝒞 := inst)
            (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ Y₁)
              (tensorObj.{v₁, u₁} (𝒞 := inst) X₃ Y₂))
            Y₃))
        (X₁ ◁ X₂ ◁ Iso.hom (β_ X₃ Y₁) ▷ Y₂ ▷ Y₃)
        (X₁ ◁
            (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ Y₁ ◁ Iso.hom (β_ X₃ Y₂) ≫
                Iso.hom (β_ X₂ Y₁) ▷ tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ X₃) ▷
              Y₃ ⊗≫
          𝟙
            (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ Y₁)
              (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ Y₂)
                (tensorObj.{v₁, u₁} (𝒞 := inst) 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₁ X₂ X₃ Y₁ Y₂ Y₃ : C
⊢ monoidalComp (Y :=
      tensorObj.{v₁, u₁} (𝒞 := inst) X₁
        (tensorObj.{v₁, u₁} (𝒞 := inst) X₂
          (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₃ Y₁) Y₂)
            Y₃)))
      (𝟙
        (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ X₂) X₃)
          (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ Y₂) Y₃)))
      (monoidalComp (Y :=
        tensorObj.{v₁, u₁} (𝒞 := inst) X₁
          (tensorObj.{v₁, u₁} (𝒞 := inst)
            (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ Y₁)
              (tensorObj.{v₁, u₁} (𝒞 := inst) X₃ Y₂))
            Y₃))
        (X₁ ◁ X₂ ◁ Iso.hom (β_ X₃ Y₁) ▷ Y₂ ▷ Y₃)
        (X₁ ◁
            (Iso.hom (β_ X₂ Y₁) ▷ tensorObj.{v₁, u₁} (𝒞 := inst) X₃ Y₂ ≫
                tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ X₂ ◁ Iso.hom (β_ X₃ Y₂)) ▷
              Y₃ ⊗≫
          𝟙
            (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₁ Y₁)
              (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ Y₂)
                (tensorObj.{v₁, u₁} (𝒞 := inst) X₃ Y₃))))) =
    (Iso.hom (α_ X₁ X₂ X₃) ⊗ₘ Iso.hom (α_ Y₁ Y₂ Y₃)) ≫
      (Iso.hom
            (α_ X₁ (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ X₃)
              (tensorObj.{v₁, u₁} (𝒞 := inst) Y₁ (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ Y₃))) ≫
          X₁ ◁ Iso.inv (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ X₃) Y₁ (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ Y₃)) ≫
            X₁ ◁
                (Iso.hom (α_ X₂ X₃ Y₁) ≫
                    X₂ ◁ Iso.hom (β_ X₃ Y₁) ≫ Iso.inv (α_ X₂ Y₁ X₃) ≫ Iso.hom (β_ X₂ Y₁) ▷ X₃ ≫ Iso.hom (α_ Y₁ X₂ X₃)) ▷
                  tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ Y₃ ≫
              X₁ ◁ Iso.hom (α_ Y₁ (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ X₃) (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ Y₃)) ≫
                Iso.inv
                  (α_ X₁ Y₁
                    (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) X₂ X₃)
                      (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ Y₃)))) ≫
        tensorObj.{v₁, u₁} (𝒞 := inst) X₁ Y₁ ◁
          (Iso.hom (α_ X₂ X₃ (tensorObj.{v₁, u₁} (𝒞 := inst) Y₂ Y₃)) ≫
            X₂ ◁ Iso.inv (α_ X₃ Y₂ Y₃) ≫
              X₂ ◁ Iso.hom (β_ X₃ Y₂) ▷ Y₃ ≫
                X₂ ◁ Iso.hom (α_ Y₂ X₃ Y₃) ≫ Iso.inv (α_ X₂ Y₂ (tensorObj.{v₁, u₁} (𝒞 := inst) 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
D : Type u₂
inst_3 : Category.{v₂, u₂} D
inst_4 : MonoidalCategory.{v₂, u₂} D
inst_5 : BraidedCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_6 : F.LaxBraided
W X Y Z : C
rw :
  Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_3) (tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj W) (F.obj X))
        (tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj Y) (F.obj Z)) ⟶
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) W Y) (tensorObj.{v₁, u₁} (𝒞 := inst) X Z)))
    (tensorμ (F.obj W) (F.obj X) (F.obj Y) (F.obj Z) ≫
      (μ F W Y ▷ tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj X) (F.obj Z) ≫
          F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) W Y) ◁ μ F X Z) ≫
        μ F (tensorObj.{v₁, u₁} (𝒞 := inst) W Y) (tensorObj.{v₁, u₁} (𝒞 := inst) X Z))
    ((μ F W X ⊗ₘ μ F Y Z) ≫
      μ F (tensorObj.{v₁, u₁} (𝒞 := inst) W X) (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.map (tensorμ W X Y Z))
⊢ Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_3) (tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj W) (F.obj X))
        (tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj Y) (F.obj Z)) ⟶
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) W Y) (tensorObj.{v₁, u₁} (𝒞 := inst) X Z)))
    (tensorμ (F.obj W) (F.obj X) (F.obj Y) (F.obj Z) ≫
      (μ F W Y ⊗ₘ μ F X Z) ≫ μ F (tensorObj.{v₁, u₁} (𝒞 := inst) W Y) (tensorObj.{v₁, u₁} (𝒞 := inst) X Z))
    ((μ F W X ⊗ₘ μ F Y Z) ≫
      μ F (tensorObj.{v₁, u₁} (𝒞 := inst) W X) (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.map (tensorμ W X Y Z))

Tactic:
rw [tensorHom_def]

Premises used: CategoryTheory.MonoidalCategory.tensorHom_def
-- 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
D : Type u₂
inst_3 : Category.{v₂, u₂} D
inst_4 : MonoidalCategory.{v₂, u₂} D
inst_5 : BraidedCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_6 : F.LaxBraided
W X Y Z : C
simp :
  Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_3) (tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj W) (F.obj X))
        (tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj Y) (F.obj Z)) ⟶
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) W Y) (tensorObj.{v₁, u₁} (𝒞 := inst) X Z)))
    (Iso.hom (α_ (F.obj W) (F.obj X) (tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj Y) (F.obj Z))) ≫
      F.obj W ◁ Iso.inv (α_ (F.obj X) (F.obj Y) (F.obj Z)) ≫
        F.obj W ◁ Iso.hom (β_ (F.obj X) (F.obj Y)) ▷ F.obj Z ≫
          F.obj W ◁ Iso.hom (α_ (F.obj Y) (F.obj X) (F.obj Z)) ≫
            Iso.inv (α_ (F.obj W) (F.obj Y) (tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj X) (F.obj Z))) ≫
              μ F W Y ▷ tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj X) (F.obj Z) ≫
                F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) W Y) ◁ μ F X Z ≫
                  μ F (tensorObj.{v₁, u₁} (𝒞 := inst) W Y) (tensorObj.{v₁, u₁} (𝒞 := inst) X Z))
    ((μ F W X ⊗ₘ μ F Y Z) ≫
      μ F (tensorObj.{v₁, u₁} (𝒞 := inst) W X) (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫
        F.map
          (Iso.hom (α_ W X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ≫
            W ◁ Iso.inv (α_ X Y Z) ≫
              W ◁ Iso.hom (β_ X Y) ▷ Z ≫
                W ◁ Iso.hom (α_ Y X Z) ≫ Iso.inv (α_ W Y (tensorObj.{v₁, u₁} (𝒞 := inst) X Z))))
⊢ Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_3) (tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj W) (F.obj X))
        (tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj Y) (F.obj Z)) ⟶
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) W Y) (tensorObj.{v₁, u₁} (𝒞 := inst) X Z)))
    (tensorμ (F.obj W) (F.obj X) (F.obj Y) (F.obj Z) ≫
      (μ F W Y ▷ tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj X) (F.obj Z) ≫
          F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) W Y) ◁ μ F X Z) ≫
        μ F (tensorObj.{v₁, u₁} (𝒞 := inst) W Y) (tensorObj.{v₁, u₁} (𝒞 := inst) X Z))
    ((μ F W X ⊗ₘ μ F Y Z) ≫
      μ F (tensorObj.{v₁, u₁} (𝒞 := inst) W X) (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫ F.map (tensorμ W X Y Z))

Tactic:
simp only [tensorμ, Category.assoc]

Premises used: CategoryTheory.Category.assoc, CategoryTheory.MonoidalCategory.tensorμ
-- 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
D : Type u₂
inst_3 : Category.{v₂, u₂} D
inst_4 : MonoidalCategory.{v₂, u₂} D
inst_5 : BraidedCategory.{v₂, u₂} D
F : Functor.{v₁, v₂, u₁, u₂} C D
inst_6 : F.LaxBraided
W X Y Z : C
⊢ Eq (α :=
    tensorObj.{v₂, u₂} (𝒞 := inst_3) (tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj W) (F.obj X))
        (tensorObj.{v₂, u₂} (𝒞 := inst_3) (F.obj Y) (F.obj Z)) ⟶
      F.obj (tensorObj.{v₁, u₁} (𝒞 := inst) (tensorObj.{v₁, u₁} (𝒞 := inst) W Y) (tensorObj.{v₁, u₁} (𝒞 := inst) X Z)))
    ((μ F W X ⊗ₘ μ F Y Z) ≫
      μ F (tensorObj.{v₁, u₁} (𝒞 := inst) W X) (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫
        F.map (Iso.inv (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) W X) Y Z)) ≫
          F.map (Iso.hom (α_ W X Y) ▷ Z) ≫
            F.map ((W ◁ Iso.hom (β_ X Y)) ▷ Z) ≫
              F.map (Iso.inv (α_ W Y X) ▷ Z) ≫ F.map (Iso.hom (α_ (tensorObj.{v₁, u₁} (𝒞 := inst) W Y) X Z)))
    ((μ F W X ⊗ₘ μ F Y Z) ≫
      μ F (tensorObj.{v₁, u₁} (𝒞 := inst) W X) (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z) ≫
        F.map
          (Iso.hom (α_ W X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)) ≫
            W ◁ Iso.inv (α_ X Y Z) ≫
              W ◁ Iso.hom (β_ X Y) ▷ Z ≫
                W ◁ Iso.hom (α_ Y X Z) ≫ Iso.inv (α_ W Y (tensorObj.{v₁, u₁} (𝒞 := inst) X Z))))

Tactic:
simp only [← Functor.map_comp, whisker_assoc, Category.assoc, pentagon_inv_inv_hom_hom_inv,
    pentagon_inv_hom_hom_hom_inv_assoc]

Premises used: CategoryTheory.MonoidalCategory.pentagon_inv_inv_hom_hom_inv, CategoryTheory.Category.assoc, CategoryTheory.MonoidalCategory.pentagon_inv_hom_hom_hom_inv_assoc, CategoryTheory.Functor.map_comp, CategoryTheory.MonoidalCategory.whisker_assoc
-- Module: Mathlib.CategoryTheory.Monoidal.Braided.Basic
Goal:
C : Type u_1
inst : Category.{v_1, u_1} C
inst_1 : MonoidalCategory.{v_1, u_1} C
inst_2 : SymmetricCategory.{v_1, u_1} C
X Y : C
⊢ tensorμ X X Y Y ≫ Iso.hom (β_ (tensorObj.{v_1, u_1} (𝒞 := inst) X Y) (tensorObj.{v_1, u_1} (𝒞 := inst) X Y)) =
    (Iso.hom (β_ X X) ⊗ₘ Iso.hom (β_ Y Y)) ≫ tensorμ X X Y Y

Tactic:
simp [tensorμ, SymmetricCategory.braiding_swap_eq_inv_braiding Y X, tensorHom_def]

Premises used: CategoryTheory.MonoidalCategory.tensorHom_def, CategoryTheory.MonoidalCategory.tensorμ, CategoryTheory.SymmetricCategory.braiding_swap_eq_inv_braiding
-- 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
D : Type u₂
inst_3 : Category.{v₂, u₂} D
inst_4 : MonoidalCategory.{v₂, u₂} D
inst_5 : BraidedCategory.{v₂, u₂} D
E : Type u₃
inst_6 : Category.{v₃, u₃} E
inst_7 : MonoidalCategory.{v₃, u₃} E
inst_8 : BraidedCategory.{v₃, u₃} E
X x x_1 : Cᵒᵖ
f : x ⟶ x_1
⊢ Eq (α :=
    Opposite.unop (tensorObj.{v₁, u₁} (𝒞 := opposite) x_1 X) ⟶ Opposite.unop (tensorObj.{v₁, u₁} (𝒞 := opposite) X x))
    (Quiver.Hom.unop (X ◁ f ≫ Iso.hom (Iso.op (β_ (Opposite.unop x_1) (Opposite.unop X)))))
    (Quiver.Hom.unop (Iso.hom (Iso.op (β_ (Opposite.unop x) (Opposite.unop X))) ≫ f ▷ X))

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
D : Type u₂
inst_3 : Category.{v₂, u₂} D
inst_4 : MonoidalCategory.{v₂, u₂} D
inst_5 : BraidedCategory.{v₂, u₂} D
E : Type u₃
inst_6 : Category.{v₃, u₃} E
inst_7 : MonoidalCategory.{v₃, u₃} E
inst_8 : BraidedCategory.{v₃, u₃} E
x x_1 : Cᵒᵖ
f : x ⟶ x_1
Z : Cᵒᵖ
⊢ Eq (α :=
    Opposite.unop (tensorObj.{v₁, u₁} (𝒞 := opposite) Z x_1) ⟶ Opposite.unop (tensorObj.{v₁, u₁} (𝒞 := opposite) x Z))
    (Quiver.Hom.unop (f ▷ Z ≫ Iso.hom (Iso.op (β_ (Opposite.unop Z) (Opposite.unop x_1)))))
    (Quiver.Hom.unop (Iso.hom (Iso.op (β_ (Opposite.unop Z) (Opposite.unop x))) ≫ Z ◁ f))

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 : C
⊢ Eq.{v₁ + 1} (α := op (tensorObj.{v₁, u₁} (𝒞 := inst) Y X) ≅ op (tensorObj.{v₁, u₁} (𝒞 := inst) X Y)) (Iso.op (β_ X Y))
    (β_ (op Y) (op X))

Tactic:
rfl

Premises used: rfl
-- 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 : Cᵒᵖ
⊢ Eq.{v₁ + 1} (α := unop (tensorObj.{v₁, u₁} (𝒞 := opposite) Y X) ≅ unop (tensorObj.{v₁, u₁} (𝒞 := opposite) X Y))
    (Iso.unop (β_ X Y)) (β_ (unop Y) (unop X))

Tactic:
rfl

Premises used: Quiver.Hom.unop, rfl, CategoryTheory.Iso.unop
-- 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 : C
⊢ Eq.{v₁ + 1} (α := op (tensorObj.{v₁, u₁} (𝒞 := inst) Y X) ⟶ op (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    (Quiver.Hom.op (Iso.hom (β_ X Y))) (Iso.hom (β_ (op Y) (op X)))

Tactic:
rfl

Premises used: Quiver.Hom.op, rfl
-- 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 : Cᵒᵖ
⊢ Eq.{v₁ + 1} (α := unop (tensorObj.{v₁, u₁} (𝒞 := opposite) Y X) ⟶ unop (tensorObj.{v₁, u₁} (𝒞 := opposite) X Y))
    (Quiver.Hom.unop (Iso.hom (β_ X Y))) (Iso.hom (β_ (unop Y) (unop X)))

Tactic:
rfl

Premises used: Quiver.Hom.unop, rfl
-- 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 : C
⊢ Eq.{v₁ + 1} (α := op (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶ op (tensorObj.{v₁, u₁} (𝒞 := inst) Y X))
    (Quiver.Hom.op (Iso.inv (β_ X Y))) (Iso.inv (β_ (op Y) (op X)))

Tactic:
rfl

Premises used: Quiver.Hom.op, rfl
-- 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 : Cᵒᵖ
⊢ Eq.{v₁ + 1} (α := unop (tensorObj.{v₁, u₁} (𝒞 := opposite) X Y) ⟶ unop (tensorObj.{v₁, u₁} (𝒞 := opposite) Y X))
    (Quiver.Hom.unop (Iso.inv (β_ X Y))) (Iso.inv (β_ (unop Y) (unop X)))

Tactic:
rfl

Premises used: Quiver.Hom.unop, rfl
-- 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
D : Type u₂
inst_3 : Category.{v₂, u₂} D
inst_4 : MonoidalCategory.{v₂, u₂} D
inst_5 : BraidedCategory.{v₂, u₂} D
E : Type u₃
inst_6 : Category.{v₃, u₃} E
inst_7 : MonoidalCategory.{v₃, u₃} E
inst_8 : BraidedCategory.{v₃, u₃} E
X x x_1 : Cᴹᵒᵖ
f : x ⟶ x_1
⊢ Eq (α :=
    (tensorObj.{v₁, u₁} (𝒞 := monoidalOppositeCategory) X x).unmop ⟶
      (tensorObj.{v₁, u₁} (𝒞 := monoidalOppositeCategory) x_1 X).unmop)
    (Quiver.Hom.unmop (X ◁ f ≫ Iso.hom (Iso.mop (β_ x_1.unmop X.unmop))))
    (Quiver.Hom.unmop (Iso.hom (Iso.mop (β_ x.unmop X.unmop)) ≫ f ▷ X))

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
D : Type u₂
inst_3 : Category.{v₂, u₂} D
inst_4 : MonoidalCategory.{v₂, u₂} D
inst_5 : BraidedCategory.{v₂, u₂} D
E : Type u₃
inst_6 : Category.{v₃, u₃} E
inst_7 : MonoidalCategory.{v₃, u₃} E
inst_8 : BraidedCategory.{v₃, u₃} E
x x_1 : Cᴹᵒᵖ
f : x ⟶ x_1
Z : Cᴹᵒᵖ
⊢ Eq (α :=
    (tensorObj.{v₁, u₁} (𝒞 := monoidalOppositeCategory) x Z).unmop ⟶
      (tensorObj.{v₁, u₁} (𝒞 := monoidalOppositeCategory) Z x_1).unmop)
    (Quiver.Hom.unmop (f ▷ Z ≫ Iso.hom (Iso.mop (β_ Z.unmop x_1.unmop))))
    (Quiver.Hom.unmop (Iso.hom (Iso.mop (β_ Z.unmop x.unmop)) ≫ Z ◁ f))

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 : C
⊢ Eq.{v₁ + 1} (α :=
    { unmop := tensorObj.{v₁, u₁} (𝒞 := inst) X Y : Cᴹᵒᵖ } ≅ { unmop := tensorObj.{v₁, u₁} (𝒞 := inst) Y X })
    (Iso.mop (β_ X Y)) (β_ { unmop := Y } { unmop := X })

Tactic:
rfl

Premises used: rfl
-- 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 : Cᴹᵒᵖ
⊢ Eq.{v₁ + 1} (α :=
    (tensorObj.{v₁, u₁} (𝒞 := monoidalOppositeCategory) X Y).unmop ≅
      (tensorObj.{v₁, u₁} (𝒞 := monoidalOppositeCategory) Y X).unmop)
    (Iso.unmop (β_ X Y)) (β_ Y.unmop X.unmop)

Tactic:
rfl

Premises used: Quiver.Hom.unmop, CategoryTheory.Functor.mapIso, rfl
-- 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 : C
⊢ Eq.{v₁ + 1} (α :=
    { unmop := tensorObj.{v₁, u₁} (𝒞 := inst) X Y : Cᴹᵒᵖ } ⟶ { unmop := tensorObj.{v₁, u₁} (𝒞 := inst) Y X })
    (Quiver.Hom.mop (Iso.hom (β_ X Y))) (Iso.hom (β_ { unmop := Y } { unmop := X }))

Tactic:
rfl

Premises used: Quiver.Hom.mop, rfl
-- 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 : Cᴹᵒᵖ
⊢ Eq.{v₁ + 1} (α :=
    (tensorObj.{v₁, u₁} (𝒞 := monoidalOppositeCategory) X Y).unmop ⟶
      (tensorObj.{v₁, u₁} (𝒞 := monoidalOppositeCategory) Y X).unmop)
    (Quiver.Hom.unmop (Iso.hom (β_ X Y))) (Iso.hom (β_ Y.unmop X.unmop))

Tactic:
rfl

Premises used: Quiver.Hom.unmop, rfl
-- 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 : C
⊢ Eq.{v₁ + 1} (α :=
    { unmop := tensorObj.{v₁, u₁} (𝒞 := inst) Y X : Cᴹᵒᵖ } ⟶ { unmop := tensorObj.{v₁, u₁} (𝒞 := inst) X Y })
    (Quiver.Hom.mop (Iso.inv (β_ X Y))) (Iso.inv (β_ { unmop := Y } { unmop := X }))

Tactic:
rfl

Premises used: Quiver.Hom.mop, rfl
-- 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 : Cᴹᵒᵖ
⊢ Eq.{v₁ + 1} (α :=
    (tensorObj.{v₁, u₁} (𝒞 := monoidalOppositeCategory) Y X).unmop ⟶
      (tensorObj.{v₁, u₁} (𝒞 := monoidalOppositeCategory) X Y).unmop)
    (Quiver.Hom.unmop (Iso.inv (β_ X Y))) (Iso.inv (β_ Y.unmop X.unmop))

Tactic:
rfl

Premises used: Quiver.Hom.unmop, rfl
-- 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
D : Type u₂
inst_3 : Category.{v₂, u₂} D
inst_4 : MonoidalCategory.{v₂, u₂} D
inst_5 : BraidedCategory.{v₂, u₂} D
E : Type u₃
inst_6 : Category.{v₃, u₃} E
inst_7 : MonoidalCategory.{v₃, u₃} E
inst_8 : BraidedCategory.{v₃, u₃} E
X Y Z : C
⊢ Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := monoidalOppositeCategory)
        (tensorObj.{v₁, u₁} (𝒞 := monoidalOppositeCategory) (Functor.obj.{v₁, v₁, u₁, u₁} (mopFunctor C) X)
          (Functor.obj.{v₁, v₁, u₁, u₁} (mopFunctor C) Y))
        (Functor.obj.{v₁, v₁, u₁, u₁} (mopFunctor C) Z) ⟶
      Functor.obj.{v₁, v₁, u₁, u₁} (mopFunctor C)
        (tensorObj.{v₁, u₁} (𝒞 := inst) X (tensorObj.{v₁, u₁} (𝒞 := inst) Y Z)))
    (Iso.hom (β_ { unmop := X : Cᴹᵒᵖ } { unmop := Y : Cᴹᵒᵖ }) ▷ Functor.obj.{v₁, v₁, u₁, u₁} (mopFunctor C) Z ≫
      Iso.hom (β_ { unmop := tensorObj.{v₁, u₁} (𝒞 := inst) X Y : Cᴹᵒᵖ } { unmop := Z : Cᴹᵒᵖ }) ≫
        Functor.map (mopFunctor C) (Iso.hom (α_ X Y Z)))
    (Iso.hom
        (α_ (Functor.obj.{v₁, v₁, u₁, u₁} (mopFunctor C) X) (Functor.obj.{v₁, v₁, u₁, u₁} (mopFunctor C) Y)
          (Functor.obj.{v₁, v₁, u₁, u₁} (mopFunctor C) Z)) ≫
      Functor.obj.{v₁, v₁, u₁, u₁} (mopFunctor C) X ◁ Iso.hom (β_ { unmop := Y : Cᴹᵒᵖ } { unmop := Z : Cᴹᵒᵖ }) ≫
        Iso.hom (β_ { unmop := X } { unmop := tensorObj.{v₁, u₁} (𝒞 := inst) Y Z }))

Tactic:
simp [← yang_baxter_assoc]

Premises used: CategoryTheory.BraidedCategory.yang_baxter_assoc
-- 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
⊢ Eq.{v₁ + 1} (α :=
    tensorUnit.{v₁, u₁} Cᴹᵒᵖ (𝒞 := monoidalOppositeCategory) ⟶
      Functor.obj.{v₁, v₁, u₁, u₁} (mopFunctor C) (tensorUnit.{v₁, u₁} C (𝒞 := inst)))
    (ε (mopFunctor C)) (𝟙 (tensorUnit.{v₁, u₁} Cᴹᵒᵖ (𝒞 := monoidalOppositeCategory)))

Tactic:
rfl

Premises used: rfl
-- 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
⊢ Eq.{v₁ + 1} (α :=
    Functor.obj.{v₁, v₁, u₁, u₁} (mopFunctor C) (tensorUnit.{v₁, u₁} C (𝒞 := inst)) ⟶
      tensorUnit.{v₁, u₁} Cᴹᵒᵖ (𝒞 := monoidalOppositeCategory))
    (η (mopFunctor C)) (𝟙 (Functor.obj.{v₁, v₁, u₁, u₁} (mopFunctor C) (tensorUnit.{v₁, u₁} C (𝒞 := inst))))

Tactic:
rfl

Premises used: rfl
-- 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 : C
⊢ Eq.{v₁ + 1} (α :=
    tensorObj.{v₁, u₁} (𝒞 := monoidalOppositeCategory) (Functor.obj.{v₁, v₁, u₁, u₁} (mopFunctor C) X)
        (Functor.obj.{v₁, v₁, u₁, u₁} (mopFunctor C) Y) ⟶
      Functor.obj.{v₁, v₁, u₁, u₁} (mopFunctor C) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y))
    (μ (mopFunctor C) X Y) (Iso.hom (β_ { unmop := X } { unmop := Y }))

Tactic:
rfl

Premises used: rfl
-- 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 : C
⊢ Eq.{v₁ + 1} (α :=
    Functor.obj.{v₁, v₁, u₁, u₁} (mopFunctor C) (tensorObj.{v₁, u₁} (𝒞 := inst) X Y) ⟶
      tensorObj.{v₁, u₁} (𝒞 := monoidalOppositeCategory) (Functor.obj.{v₁, v₁, u₁, u₁} (mopFunctor C) X)
        (Functor.obj.{v₁, v₁, u₁, u₁} (mopFunctor C) Y))
    (δ (mopFunctor C) X Y) (Iso.inv (β_ { unmop := X } { unmop := Y }))

Tactic:
rfl

Premises used: rfl