-- 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
simp :
  Iso.hom (X.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))) ▷
        U ≫
      Iso.hom
          (α_ (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)) (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 ≫
          Iso.inv
              (α_ (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.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ≫
              Iso.hom
                (α_ U (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
                  (X.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 ◁
                Iso.hom
                  (X.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β
                    (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)))
⊢ Iso.hom (X.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))) ▷
        U ≫
      Iso.hom
          (α_ (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)) (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 ≫
          Iso.inv
              (α_ (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.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ≫
              Iso.hom
                (α_ U (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
                  (X.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 ◁
        Iso.hom
          (X.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)))

Tactic:
simp only [Category.assoc]

Premises used: CategoryTheory.Category.assoc