diff --git a/Mathlib/Algebra/Group/Basic.lean b/Mathlib/Algebra/Group/Basic.lean
index c5a21819126940..c62e2142f4ad6e 100644
--- a/Mathlib/Algebra/Group/Basic.lean
+++ b/Mathlib/Algebra/Group/Basic.lean
@@ -1088,6 +1088,10 @@ instance AddCommGroup.toGrindIntModule [s : AddCommGroup α] :
     add_zsmul n m a := add_zsmul a n m
     zsmul_natCast_eq_nsmul n a := by simp }
 
+-- Give the core instance deriving a module structure from a `Grind.IntModule` a higher priority,
+-- so that for an `AddCommGroup` it is preferred over the `AddCommMonoid`-based instance above.
+attribute [instance 1100] Lean.Grind.IntModule.OfNatModule.ofNatModule
+
 instance IsRightCancelAdd.toGrindAddRightCancel [AddSemigroup α] [IsRightCancelAdd α] :
     Grind.AddRightCancel α where
   add_right_cancel _ _ _ := add_right_cancel