-- 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₁ Y₂ : Center.{v₁, u₁} C
f : Y₁ ⟶ Y₂
U : C
⊢ monoidalComp (Y :=
      MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst) (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
        (MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst) (Y₁.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)) 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)))
          U))
      (monoidalComp (Y :=
        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)))
        (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁
          (f.f ▷ U ≫ (Y₂.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom))
        ((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) 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) (Y₁.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)) 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)))
          U))
      (monoidalComp (Y :=
        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)))
        (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁
          (Y₁.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom)
        ((MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst) (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)) U ◁
              f.f ≫
            (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) U
              (MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst)
                (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
                (Y₂.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))))))
have rw : monoidalComp (Y :=
    MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst) (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X))
      (MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst) (Y₁.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)) 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)))
        U))
    (monoidalComp (Y :=
      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)))
      (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁
        ((Y₁.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom ≫ U ◁ f.f))
      ((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) 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) (Y₁.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)) 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)))
        U))
    (monoidalComp (Y :=
      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)))
      (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X) ◁
        (Y₁.snd (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X).β U).hom)
      ((MonoidalCategoryStruct.tensorObj.{v₁, u₁} (𝒞 := inst) (X.fst (β := fun (X : C) ↦ HalfBraiding.{v₁, u₁} X)) U ◁
            f.f ≫
          (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) 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: rw [f.comm]