-- 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
rw :
  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.inv
                  (α_ U (Y.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
                    (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))) =
    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:
rw [← IsIso.inv_comp_eq, IsIso.Iso.inv_hom, ← HalfBraiding.monoidal_assoc,
        ← HalfBraiding.naturality_assoc, HalfBraiding.monoidal]

Premises used: CategoryTheory.HalfBraiding.naturality_assoc, CategoryTheory.IsIso.inv_comp_eq, CategoryTheory.HalfBraiding.monoidal_assoc, CategoryTheory.IsIso.Iso.inv_hom, CategoryTheory.HalfBraiding.monoidal