-- 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
_ :
  Iso.hom
        (α_ (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)) (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
          (MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst) U U')) ≫
      X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁
          (Iso.inv (α_ (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)) U U') ≫
            (Y.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ▷ U' ≫
              Iso.hom (α_ U (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)) U') ≫
                U ◁ (Y.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U').hom ≫
                  Iso.inv (α_ U U' (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)))) ≫
        Iso.inv
            (α_ (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
              (MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst) U U')
              (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))) ≫
          (Iso.inv (α_ (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)) U U') ≫
                (X.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ▷ U' ≫
                  Iso.hom (α_ U (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)) U') ≫
                    U ◁ (X.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U').hom ≫
                      Iso.inv (α_ U U' (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)))) ▷
              Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ≫
            Iso.hom
              (α_ (MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst) U 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)
          (MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst) (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)) U)
          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)))
          (MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst) U U')))
      (monoidalComp (Y :=
        MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst)
          (MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst) (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)) U)
          (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 ▷ U')
        (monoidalComp (Y :=
          MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst) U
            (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))))
          (MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst) (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
                U ◁
              (Y.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U').hom ≫
            (X.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ▷
              MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst) U'
                (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)))
          (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)
                (MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst) U 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)
          (MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst) (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)) U)
          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)))
          (MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst) U U')))
      (monoidalComp (Y :=
        MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst)
          (MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst) (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)) U)
          (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 ▷ U')
        (monoidalComp (Y :=
          MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst) U
            (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))))
          (MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst) (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
                U ◁
              (Y.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U').hom ≫
            (X.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ▷
              MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst) U'
                (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)))
          (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)
                (MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst) U 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.inv
        (α_
          (MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst) (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
            (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)))
          U 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)))) ▷
          U' ≫
        Iso.hom
            (α_ U
              (MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst)
                (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
                (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)))
              U') ≫
          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.inv
              (α_ U U'
                (MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst)
                  (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
                  (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))))
⊢ Eq (α :=
    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)))
        (MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst) U U') ⟶
      MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst) (MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst) U 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))
          (MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst) U U')) ≫
      X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁
          (Iso.inv (α_ (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)) U U') ≫
            (Y.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ▷ U' ≫
              Iso.hom (α_ U (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)) U') ≫
                U ◁ (Y.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U').hom ≫
                  Iso.inv (α_ U U' (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)))) ≫
        Iso.inv
            (α_ (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
              (MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst) U U')
              (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))) ≫
          (Iso.inv (α_ (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)) U U') ≫
                (X.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ▷ U' ≫
                  Iso.hom (α_ U (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)) U') ≫
                    U ◁ (X.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U').hom ≫
                      Iso.inv (α_ U U' (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)))) ▷
              Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ≫
            Iso.hom
              (α_ (MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst) U U')
                (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
                (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))))
    (Iso.inv
        (α_
          (MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst) (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
            (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)))
          U 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)))) ▷
          U' ≫
        Iso.hom
            (α_ U
              (MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst)
                (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
                (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)))
              U') ≫
          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.inv
              (α_ U 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:
calc
          _ = 𝟙 _ ⊗≫
            X.1 ◁ (HalfBraiding.β Y.2 U).hom ▷ U' ⊗≫
              (_ ◁ (HalfBraiding.β Y.2 U').hom ≫
                (HalfBraiding.β X.2 U).hom ▷ _) ⊗≫
                  U ◁ (HalfBraiding.β X.2 U').hom ▷ Y.1 ⊗≫ 𝟙 _ := by monoidal
          _ = _ := by rw [whisker_exchange]; monoidal

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