Will this work now?

mans0954 · mans0954 · commit 27acbdeac898 · 2023-08-16T08:18:33.000+01:00
diff --git a/Mathlib/Algebra/Hom/Centroid.lean b/Mathlib/Algebra/Hom/Centroid.lean
@@ -542,8 +542,7 @@ def star_ring (mul_comm : ∀ f g : CentroidHom α, f * g = g * f) : StarRing (C
   star_mul := fun f g => by
     rw [mul_comm]
     ext
-    rw [star_apply, mul_apply, mul_apply, star_apply]
-    simp
+    rw [star_apply, mul_apply, mul_apply, star_apply, star_apply, star_star]
   star_add := fun f g => by
     ext
     rw [star_apply, add_apply, star_add, add_apply, star_apply, star_apply] }
