-- 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 U' : C
f : U ⟶ U'
rw :
  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 ▷ 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)
        ((X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁ f ≫
              (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.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁ f ≫
            (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)))))) =
    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.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁ f ≫
              (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:
rw [HalfBraiding.naturality]

Premises used: CategoryTheory.HalfBraiding.naturality