-- 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))))))
_₁ :
  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)))))) =
    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))))))
_₂ :
  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)))))) =
    (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)
⊢ 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))) =
    (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:
calc
    _ = 𝟙 _ ⊗≫
      (f.f ▷ (Y.fst ⊗ U) ≫ X₂.fst ◁ (HalfBraiding.β Y.snd U).hom) ⊗≫
        (HalfBraiding.β X₂.snd U).hom ▷ Y.fst ⊗≫ 𝟙 _ := by monoidal
    _ = 𝟙 _ ⊗≫
      X₁.fst ◁ (HalfBraiding.β Y.snd U).hom ⊗≫
        (f.f ▷ U ≫ (HalfBraiding.β X₂.snd U).hom) ▷ Y.fst ⊗≫ 𝟙 _ := by
      rw [← whisker_exchange]; monoidal
    _ = _ := by rw [f.comm]; monoidal

Premises used: CategoryTheory.HalfBraiding.β, CategoryTheory.MonoidalCategoryStruct.whiskerLeft, CategoryTheory.CategoryStruct.id, Sigma.fst, CategoryTheory.Center.Hom.f, CategoryTheory.MonoidalCategoryStruct.whiskerRight, CategoryTheory.MonoidalCategoryStruct.tensorObj, CategoryTheory.CategoryStruct.comp, Sigma.snd, CategoryTheory.Iso.hom