diff --git a/mathlib4/Mathlib/Algebra/Category/ModuleCat/Presheaf/Monoidal.lean b/mathlib4/Mathlib/Algebra/Category/ModuleCat/Presheaf/Monoidal.lean
index 21055447c..7fc429472 100644
--- a/mathlib4/Mathlib/Algebra/Category/ModuleCat/Presheaf/Monoidal.lean
+++ b/mathlib4/Mathlib/Algebra/Category/ModuleCat/Presheaf/Monoidal.lean
@@ -150,18 +150,30 @@ noncomputable instance monoidalCategory :
     MonoidalCategory (PresheafOfModulesOfCommRing.{u} R) where
   tensorHom_def _ _ := by ext1; apply tensorHom_def
   id_tensorHom_id _ _ := by ext1; apply id_tensorHom_id
-  tensorHom_comp_tensorHom _ _ _ _ := by ext1; apply tensorHom_comp_tensorHom
+  tensorHom_comp_tensorHom _ _ _ _ := by
+    ext1 X
+    apply MonoidalCategory.tensorHom_comp_tensorHom (C := ModuleCat (R.obj X))
   whiskerLeft_id M₁ M₂ := by
     ext1 X
     apply MonoidalCategory.whiskerLeft_id (C := ModuleCat (R.obj X))
   id_whiskerRight _ _ := by
     ext1 X
     apply MonoidalCategory.id_whiskerRight (C := ModuleCat (R.obj X))
-  associator_naturality _ _ _ := by ext1; apply associator_naturality
-  leftUnitor_naturality _ := by ext1; apply leftUnitor_naturality
-  rightUnitor_naturality _ := by ext1; apply rightUnitor_naturality
-  pentagon _ _ _ _ := by ext1; apply pentagon
-  triangle _ _ := by ext1; apply triangle
+  associator_naturality _ _ _ := by
+    ext1 X
+    apply MonoidalCategory.associator_naturality (C := ModuleCat (R.obj X))
+  leftUnitor_naturality _ := by
+    ext1 X
+    apply MonoidalCategory.leftUnitor_naturality (C := ModuleCat (R.obj X))
+  rightUnitor_naturality _ := by
+    ext1 X
+    apply MonoidalCategory.rightUnitor_naturality (C := ModuleCat (R.obj X))
+  pentagon _ _ _ _ := by
+    ext1 X
+    apply MonoidalCategory.pentagon (C := ModuleCat (R.obj X))
+  triangle _ _ := by
+    ext1 X
+    apply MonoidalCategory.triangle (C := ModuleCat (R.obj X))
 
 open BraidedCategory