-- Lean 4 proof step from Mathlib.CategoryTheory.Monoidal.Center (goal)
Goal:
C : Type u₁
inst : Category.{v₁, u₁} C
inst_1 : MonoidalCategory.{v₁, u₁} C
X Y : Center.{v₁, u₁} C
U : C
⊢ 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)))
have 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)))
Tactic: simp only [Category.assoc]