diff --git a/Mathlib/Algebra/Category/ModuleCat/Presheaf/Limits.lean b/Mathlib/Algebra/Category/ModuleCat/Presheaf/Limits.lean
index a627bb90c15d88..3de0f01899ad66 100644
--- a/Mathlib/Algebra/Category/ModuleCat/Presheaf/Limits.lean
+++ b/Mathlib/Algebra/Category/ModuleCat/Presheaf/Limits.lean
@@ -79,8 +79,7 @@ noncomputable def limitPresheafOfModules : PresheafOfModules R where
     dsimp
     simp only [limMap_π, Functor.comp_obj, evaluation_obj, Functor.whiskerLeft_app,
       restriction_app, assoc]
-    -- Here we should rewrite using `Functor.assoc` but that gives a "motive is type-incorrect"
-    erw [preservesLimitIso_hom_π]
+    simp only [← Functor.assoc, preservesLimitIso_hom_π]
     rw [← ModuleCat.restrictScalarsId'App_inv_naturality, map_id,
       ModuleCat.restrictScalarsId'_inv_app]
     dsimp
@@ -92,18 +91,15 @@ noncomputable def limitPresheafOfModules : PresheafOfModules R where
     intro j
     simp only [Functor.comp_obj, evaluation_obj, limMap_π, Functor.whiskerLeft_app, restriction_app,
       map_comp, ModuleCat.restrictScalarsComp'_inv_app, Functor.map_comp, assoc]
-    -- Here we should rewrite using `Functor.assoc` but that gives a "motive is type-incorrect"
-    erw [preservesLimitIso_hom_π]
+    simp only [← Functor.assoc, preservesLimitIso_hom_π]
     rw [← ModuleCat.restrictScalarsComp'App_inv_naturality]
     dsimp
     rw [← Functor.map_comp_assoc, ← Functor.map_comp_assoc, assoc,
       preservesLimitIso_inv_π]
-    -- Here we should rewrite using `Functor.assoc` but that gives a "motive is type-incorrect"
-    erw [limMap_π]
+    rw [limMap_π]
     dsimp
     simp only [Functor.map_comp, assoc, preservesLimitIso_inv_π_assoc]
-    -- Here we should rewrite using `Functor.assoc` but that gives a "motive is type-incorrect"
-    erw [limMap_π_assoc]
+    rw [limMap_π_assoc]
     dsimp
 
 set_option backward.isDefEq.respectTransparency false in