awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.CategoryTheory.Monoidal.Center
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X₁ X₂ : Center.{v₁, u₁} C
f : X₁ ⟶ X₂
Y : Center.{v₁, u₁} C
U : C
⊢ f.f ▷ Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ▷ U ≫
      Iso.hom
          (α_ (X₂.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)) (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
            U) ≫
        X₂.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁
            (Y.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ≫
          Iso.inv
              (α_ (X₂.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)) U
                (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))) ≫
            (X₂.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ▷
                Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ≫
              Iso.hom
                (α_ U (X₂.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
                  (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))) =
    monoidalComp (Y :=
      MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst) (X₁.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
        (MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst) (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)) U))
      (𝟙
        (MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst)
          (MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst) (X₁.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
            (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)))
          U))
      (monoidalComp (Y :=
        MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst)
          (MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst) (X₂.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
            U)
          (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)))
        (f.f ▷
            MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst) (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
              U ≫
          X₂.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁
            (Y.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom)
        ((X₂.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ▷
            Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ⊗≫
          𝟙
            (MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst) U
              (MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst)
                (X₂.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
                (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))))))

Tactic:
monoidal
-- Module: Mathlib.CategoryTheory.Monoidal.Center
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X₁ X₂ : Center.{v₁, u₁} C
f : X₁ ⟶ X₂
Y : Center.{v₁, u₁} C
U : C
⊢ monoidalComp (Y :=
      MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst) (X₁.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
        (MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst) (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)) U))
      (𝟙
        (MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst)
          (MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst) (X₁.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
            (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)))
          U))
      (monoidalComp (Y :=
        MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst)
          (MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst) (X₂.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
            U)
          (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)))
        (X₁.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁
            (Y.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ≫
          f.f ▷
            MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst) U
              (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)))
        ((X₂.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ▷
            Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ⊗≫
          𝟙
            (MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst) U
              (MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst)
                (X₂.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
                (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)))))) =
    monoidalComp (Y :=
      MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst) (X₁.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
        (MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst) (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)) U))
      (𝟙
        (MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst)
          (MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst) (X₁.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
            (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)))
          U))
      (monoidalComp (Y :=
        MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst)
          (MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst) (X₁.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
            U)
          (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)))
        (X₁.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁
          (Y.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom)
        ((f.f ▷ U ≫ (X₂.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom) ▷
            Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ⊗≫
          𝟙
            (MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst) U
              (MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst)
                (X₂.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
                (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))))))

Tactic:
monoidal
-- Module: Mathlib.CategoryTheory.Monoidal.Center
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X₁ X₂ : Center.{v₁, u₁} C
f : X₁ ⟶ X₂
Y : Center.{v₁, u₁} C
U : C
⊢ monoidalComp (Y :=
      MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst) (X₁.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
        (MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst) (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)) U))
      (𝟙
        (MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst)
          (MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst) (X₁.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
            (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)))
          U))
      (monoidalComp (Y :=
        MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst)
          (MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst) (X₁.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
            U)
          (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)))
        (X₁.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁
          (Y.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom)
        (((X₁.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ≫ U ◁ f.f) ▷
            Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ⊗≫
          𝟙
            (MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst) U
              (MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst)
                (X₂.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
                (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)))))) =
    (Iso.hom
          (α_ (X₁.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)) (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
            U) ≫
        X₁.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁
            (Y.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ≫
          Iso.inv
              (α_ (X₁.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)) U
                (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))) ≫
            (X₁.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ▷
                Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ≫
              Iso.hom
                (α_ U (X₁.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
                  (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)))) ≫
      U ◁ f.f ▷ Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)

Tactic:
monoidal
-- Module: Mathlib.CategoryTheory.Monoidal.Center
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X₁ Y₁ X₂ Y₂ : Center.{v₁, u₁} C
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
U : C
rw :
  (f.f ▷ X₂.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ≫
          Y₁.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁ g.f) ▷
        U ≫
      ((Y₁.tensorObj Y₂).snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom =
    ((X₁.tensorObj X₂).snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ≫
      U ◁
        (f.f ▷ X₂.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ≫
          Y₁.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁ g.f)
rw₁ :
  f.f ▷ X₂.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ▷ U ≫
      (Y₁.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁ g.f) ▷ U ≫
        ((Y₁.tensorObj Y₂).snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom =
    ((X₁.tensorObj X₂).snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ≫
      U ◁
        (f.f ▷ X₂.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ≫
          Y₁.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁ g.f)
rw₂ :
  f.f ▷ X₂.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ▷ U ≫
      ((Y₁.tensorObj X₂).snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ≫
        U ◁ Y₁.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁ g.f =
    ((X₁.tensorObj X₂).snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ≫
      U ◁
        (f.f ▷ X₂.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ≫
          Y₁.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁ g.f)
rw₃ :
  ((X₁.tensorObj X₂).snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ≫
      U ◁ f.f ▷ X₂.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ≫
        U ◁ Y₁.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁ g.f =
    ((X₁.tensorObj X₂).snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ≫
      U ◁
        (f.f ▷ X₂.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ≫
          Y₁.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁ g.f)
rw₄ rw₅ :
  ((X₁.tensorObj X₂).snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ≫
      U ◁ f.f ▷ X₂.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ≫
        U ◁ Y₁.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁ g.f =
    ((X₁.tensorObj X₂).snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ≫
      U ◁ f.f ▷ X₂.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ≫
        U ◁ Y₁.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁ g.f
⊢ (f.f ⊗ₘ g.f) ▷ U ≫ ((Y₁.tensorObj Y₂).snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom =
    ((X₁.tensorObj X₂).snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ≫ U ◁ (f.f ⊗ₘ g.f)

Tactic:
rw [tensorHom_def, comp_whiskerRight_assoc, whiskerLeft_comm, whiskerRight_comm_assoc,
      MonoidalCategory.whiskerLeft_comp]

Premises used: CategoryTheory.Center.whiskerLeft_comm, CategoryTheory.MonoidalCategory.whiskerLeft_comp, CategoryTheory.MonoidalCategory.tensorHom_def, CategoryTheory.MonoidalCategory.comp_whiskerRight_assoc, CategoryTheory.Center.whiskerRight_comm_assoc
-- Module: Mathlib.CategoryTheory.Monoidal.Center
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y Z : Center.{v₁, u₁} C
U : C
⊢ Iso.hom
          (α_ (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)) (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
            (Z.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))) ▷
        U ≫
      ((X.tensorObj (Y.tensorObj Z)).snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom =
    (((X.tensorObj Y).tensorObj Z).snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ≫
      U ◁
        Iso.hom
          (α_ (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)) (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
            (Z.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Center
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X : Center.{v₁, u₁} C
U : C
⊢ Iso.hom (λ_ (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))) ▷ U ≫
      (X.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom =
    ((tensorObj tensorUnit X).snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ≫
      U ◁ Iso.hom (λ_ (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Center
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X : Center.{v₁, u₁} C
U : C
⊢ Iso.hom (ρ_ (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))) ▷ U ≫
      (X.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom =
    ((X.tensorObj tensorUnit).snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ≫
      U ◁ Iso.hom (ρ_ (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)))

Tactic:
simp
-- Module: Mathlib.CategoryTheory.Monoidal.Center
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X₁ Y₁ X₂ Y₂ : Center.{v₁, u₁} C
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
w : (tensorHom f g).f = (whiskerRight f X₂ ≫ Y₁.whiskerLeft g).f
⊢ tensorHom f g = whiskerRight f X₂ ≫ Y₁.whiskerLeft g

Tactic:
ext
-- Module: Mathlib.CategoryTheory.Monoidal.Center
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X₁ Y₁ X₂ Y₂ : Center.{v₁, u₁} C
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
⊢ (tensorHom f g).f = (whiskerRight f X₂ ≫ Y₁.whiskerLeft g).f

Tactic:
simp [tensorHom_def]

Premises used: CategoryTheory.MonoidalCategory.tensorHom_def
-- Module: Mathlib.CategoryTheory.Monoidal.Center
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y : Center.{v₁, u₁} C
⊢ (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) X Y).fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) =
    MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst) (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
      (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Center
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y : Center.{v₁, u₁} C
U : C
⊢ (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) X Y).snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U =
    α_ (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)) (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)) U ≪≫
      X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁ᵢ Y.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U ≪≫
        Iso.symm
            (α_ (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)) U
              (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))) ≪≫
          X.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U ▷ᵢ
              Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ≪≫
            α_ U (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
              (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))

Tactic:
rfl

Premises used: CategoryTheory.Iso.trans, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Center
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y₁ Y₂ : Center.{v₁, u₁} C
f : Y₁ ⟶ Y₂
⊢ Hom.f (X ◁ f) = X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁ f.f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Center
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X₁ X₂ : Center.{v₁, u₁} C
f : X₁ ⟶ X₂
Y : Center.{v₁, u₁} C
⊢ Hom.f (f ▷ Y) = f.f ▷ Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Center
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X₁ Y₁ X₂ Y₂ : Center.{v₁, u₁} C
f : X₁ ⟶ Y₁
g : X₂ ⟶ Y₂
⊢ Hom.f (f ⊗ₘ g) = f.f ⊗ₘ g.f

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Center
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
U : C
⊢ Eq.{v₁ + 1} (α :=
    MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst)
        (Sigma.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ((𝟙_ (Center.{v₁, u₁} C)) (𝒞 := instCategory))) U ≅
      MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst) U
        (Sigma.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ((𝟙_ (Center.{v₁, u₁} C)) (𝒞 := instCategory))))
    (HalfBraiding.β
      (Sigma.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ((𝟙_ (Center.{v₁, u₁} C)) (𝒞 := instCategory))) U)
    (λ_ U ≪≫ Iso.symm (ρ_ U))

Tactic:
rfl

Premises used: CategoryTheory.Iso.trans, rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Center
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y Z : Center.{v₁, u₁} C
⊢ Hom.f (Iso.hom (α_ X Y Z)) =
    Iso.hom
      (α_ (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)) (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
        (Z.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Center
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y Z : Center.{v₁, u₁} C
hom_inv_id :
  Iso.hom
        (α_ (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)) (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
          (Z.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))) ≫
      Hom.f (Iso.inv (α_ X Y Z)) =
    𝟙
      ((MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) X Y)
            Z).fst
        (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
⊢ Hom.f (Iso.inv (α_ X Y Z)) =
    Iso.inv
      (α_ (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)) (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
        (Z.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)))

Tactic:
apply Iso.inv_ext'

Premises used: CategoryTheory.Iso.inv_ext'
-- Module: Mathlib.CategoryTheory.Monoidal.Center
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y Z : Center.{v₁, u₁} C
hom_inv_id :
  Hom.f
      (𝟙
        (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) X Y)
          Z)) =
    𝟙
      ((MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) X Y)
            Z).fst
        (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
⊢ Iso.hom
        (α_ (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)) (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
          (Z.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))) ≫
      Hom.f (Iso.inv (α_ X Y Z)) =
    𝟙
      ((MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) X Y)
            Z).fst
        (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))

Tactic:
rw [← associator_hom_f, ← comp_f, Iso.hom_inv_id]

Premises used: CategoryTheory.Center.associator_hom_f, CategoryTheory.Center.comp_f, CategoryTheory.Iso.hom_inv_id
-- Module: Mathlib.CategoryTheory.Monoidal.Center
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y Z : Center.{v₁, u₁} C
⊢ Hom.f
      (𝟙
        (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) X Y)
          Z)) =
    𝟙
      ((MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) X Y)
            Z).fst
        (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Center
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X : Center.{v₁, u₁} C
⊢ Hom.f (Iso.hom (λ_ X)) = Iso.hom (λ_ (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Center
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X : Center.{v₁, u₁} C
hom_inv_id :
  Iso.hom (λ_ (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))) ≫ Hom.f (Iso.inv (λ_ X)) =
    𝟙
      ((MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) ((𝟙_ (Center.{v₁, u₁} C)) (𝒞 := instCategory)) X).fst (β :=
        fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
⊢ Hom.f (Iso.inv (λ_ X)) = Iso.inv (λ_ (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)))

Tactic:
apply Iso.inv_ext'

Premises used: CategoryTheory.Iso.inv_ext'
-- Module: Mathlib.CategoryTheory.Monoidal.Center
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X : Center.{v₁, u₁} C
hom_inv_id :
  Hom.f (𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) ((𝟙_ (Center.{v₁, u₁} C)) (𝒞 := instCategory)) X)) =
    𝟙
      ((MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) ((𝟙_ (Center.{v₁, u₁} C)) (𝒞 := instCategory)) X).fst (β :=
        fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
⊢ Iso.hom (λ_ (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))) ≫ Hom.f (Iso.inv (λ_ X)) =
    𝟙
      ((MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) ((𝟙_ (Center.{v₁, u₁} C)) (𝒞 := instCategory)) X).fst (β :=
        fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))

Tactic:
rw [← leftUnitor_hom_f, ← comp_f, Iso.hom_inv_id]

Premises used: CategoryTheory.Center.comp_f, CategoryTheory.Iso.hom_inv_id, CategoryTheory.Center.leftUnitor_hom_f
-- Module: Mathlib.CategoryTheory.Monoidal.Center
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X : Center.{v₁, u₁} C
⊢ Hom.f (𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) ((𝟙_ (Center.{v₁, u₁} C)) (𝒞 := instCategory)) X)) =
    𝟙
      ((MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) ((𝟙_ (Center.{v₁, u₁} C)) (𝒞 := instCategory)) X).fst (β :=
        fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))

Tactic:
rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Center
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X : Center.{v₁, u₁} C
⊢ Hom.f (Iso.hom (ρ_ X)) = Iso.hom (ρ_ (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)))

Tactic:
rfl

Premises used: rfl
-- Module: Mathlib.CategoryTheory.Monoidal.Center
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X : Center.{v₁, u₁} C
hom_inv_id :
  Iso.hom (ρ_ (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))) ≫ Hom.f (Iso.inv (ρ_ X)) =
    𝟙
      ((MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) X ((𝟙_ (Center.{v₁, u₁} C)) (𝒞 := instCategory))).fst (β :=
        fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
⊢ Hom.f (Iso.inv (ρ_ X)) = Iso.inv (ρ_ (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)))

Tactic:
apply Iso.inv_ext'

Premises used: CategoryTheory.Iso.inv_ext'
-- Module: Mathlib.CategoryTheory.Monoidal.Center
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X : Center.{v₁, u₁} C
hom_inv_id :
  Hom.f (𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) X ((𝟙_ (Center.{v₁, u₁} C)) (𝒞 := instCategory)))) =
    𝟙
      ((MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) X ((𝟙_ (Center.{v₁, u₁} C)) (𝒞 := instCategory))).fst (β :=
        fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
⊢ Iso.hom (ρ_ (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))) ≫ Hom.f (Iso.inv (ρ_ X)) =
    𝟙
      ((MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) X ((𝟙_ (Center.{v₁, u₁} C)) (𝒞 := instCategory))).fst (β :=
        fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))

Tactic:
rw [← rightUnitor_hom_f, ← comp_f, Iso.hom_inv_id]

Premises used: CategoryTheory.Center.comp_f, CategoryTheory.Iso.hom_inv_id, CategoryTheory.Center.rightUnitor_hom_f
-- Module: Mathlib.CategoryTheory.Monoidal.Center
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X : Center.{v₁, u₁} C
⊢ Hom.f (𝟙 (MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) X ((𝟙_ (Center.{v₁, u₁} C)) (𝒞 := instCategory)))) =
    𝟙
      ((MonoidalCategoryStruct.tensorObj (𝒞 := instCategory) X ((𝟙_ (Center.{v₁, u₁} C)) (𝒞 := instCategory))).fst (β :=
        fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))

Tactic:
rfl