diff --git a/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean b/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean
index cb898e4e7dc8ff..86510146e100fb 100644
--- a/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean
+++ b/Mathlib/Algebra/Category/ModuleCat/ChangeOfRings.lean
@@ -395,10 +395,7 @@ instance hasSMul : SMul S <| (restrictScalars f).obj (of _ S) →ₗ[R] M where
     { toFun := fun s' : S => g (s' * s : S)
       map_add' := fun x y : S => by rw [add_mul, map_add]
       map_smul' := fun r (t : S) => by
-        -- Porting note: needed some erw's even after dsimp to clean things up
-        dsimp
-        rw [← map_smul]
-        erw [smul_eq_mul, smul_eq_mul, mul_assoc] }
+        simp [← map_smul, ModuleCat.restrictScalars.smul_def (M := ModuleCat.of _ S), mul_assoc] }
 
 @[simp]
 theorem smul_apply' (s : S) (g : (restrictScalars f).obj (of _ S) →ₗ[R] M) (s' : S) :