-- Lean 4 proof step from Mathlib.Algebra.Category.MonCat.FilteredColimits (goal)
Goal:
J : Type v
inst : SmallCategory J
inst_1 : IsFiltered J
F : J ⥤ CommMonCat
i : J
x :
  (↑(Functor.obj
        (F ⋙
          forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
            carrier) MonCat (FD := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CD :=
            MonCat.carrier))
        i) :
    Type (max u v))
j : J
y :
  (↑(Functor.obj
        (F ⋙
          forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
            carrier) MonCat (FD := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CD :=
            MonCat.carrier))
        j) :
    Type (max u v))
k : J := IsFiltered.max i j
f : i ⟶ IsFiltered.max i j := IsFiltered.leftToMax i j
g : j ⟶ IsFiltered.max i j := IsFiltered.rightToMax i j
⊢ MonCat.FilteredColimits.M.mk
      (F ⋙
        forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
          carrier) MonCat (FD := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CD :=
          MonCat.carrier))
      (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) k
        (HMul.hMul (α := (↑(F.obj k) : Type (max u v))) (β := (↑(F.obj k) : Type (max u v)))
          ((Hom.hom (F.map f) : (a : (↑(F.obj i) : Type (max u v))) → (↑(F.obj k) : Type (max u v))) x :
            (↑(F.obj k) : Type (max u v)))
          ((Hom.hom (F.map g) : (a : (↑(F.obj j) : Type (max u v))) → (↑(F.obj k) : Type (max u v))) y :
            (↑(F.obj k) : Type (max u v))))) =
    MonCat.FilteredColimits.M.mk
      (F ⋙
        forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
          carrier) MonCat (FD := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CD :=
          MonCat.carrier))
      (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) k
        (HMul.hMul (α := (↑(F.obj k) : Type (max u v))) (β := (↑(F.obj k) : Type (max u v)))
          ((Hom.hom (F.map g) : (a : (↑(F.obj j) : Type (max u v))) → (↑(F.obj k) : Type (max u v))) y :
            (↑(F.obj k) : Type (max u v)))
          ((Hom.hom (F.map f) : (a : (↑(F.obj i) : Type (max u v))) → (↑(F.obj k) : Type (max u v))) x :
            (↑(F.obj k) : Type (max u v)))))
have rw : MonCat.FilteredColimits.M.mk
    (F ⋙
      forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
        carrier) MonCat (FD := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CD :=
        MonCat.carrier))
    (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) k
      (HMul.hMul (α := (↑(F.obj k) : Type (max u v))) (β := (↑(F.obj k) : Type (max u v)))
        ((Hom.hom (F.map g) : (a : (↑(F.obj j) : Type (max u v))) → (↑(F.obj k) : Type (max u v))) y :
          (↑(F.obj k) : Type (max u v)))
        ((Hom.hom (F.map f) : (a : (↑(F.obj i) : Type (max u v))) → (↑(F.obj k) : Type (max u v))) x :
          (↑(F.obj k) : Type (max u v))))) =
  MonCat.FilteredColimits.M.mk
    (F ⋙
      forget₂ CommMonCat (FC := fun (x1 x2 : CommMonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CC :=
        carrier) MonCat (FD := fun (x1 x2 : MonCat) ↦ (↑x1 : Type (max u v)) →* (↑x2 : Type (max u v))) (CD :=
        MonCat.carrier))
    (Sigma.mk (β := fun (j : J) ↦ (↑(F.obj j) : Type (max u v))) k
      (HMul.hMul (α := (↑(F.obj k) : Type (max u v))) (β := (↑(F.obj k) : Type (max u v)))
        ((Hom.hom (F.map g) : (a : (↑(F.obj j) : Type (max u v))) → (↑(F.obj k) : Type (max u v))) y :
          (↑(F.obj k) : Type (max u v)))
        ((Hom.hom (F.map f) : (a : (↑(F.obj i) : Type (max u v))) → (↑(F.obj k) : Type (max u v))) x :
          (↑(F.obj k) : Type (max u v)))))
Tactic: rw [mul_comm]