-- 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 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)))
Tactic: rw [← IsIso.inv_comp_eq, IsIso.Iso.inv_hom, ← HalfBraiding.monoidal_assoc,
        ← HalfBraiding.naturality_assoc, HalfBraiding.monoidal]