From a2f47a9eb84379f3538d86b6a55d4938b839b2fb Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 30 May 2026 22:12:46 +0000 Subject: [PATCH 1/2] chore: raise priority of Grind.IntModule.OfNatModule.ofNatModule Globally raise the priority of the core `Lean.Grind.IntModule.OfNatModule.ofNatModule` instance to `high` so that it is preferred throughout Mathlib. https://claude.ai/code/session_01Xq5Eavd4WbKAosAW4p2xXg --- Mathlib/Algebra/Group/Basic.lean | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/Mathlib/Algebra/Group/Basic.lean b/Mathlib/Algebra/Group/Basic.lean index c5a21819126940..922eca27753ee9 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 high priority, +-- so that for an `AddCommGroup` it is preferred over the `AddCommMonoid`-based instance above. +attribute [instance high] Lean.Grind.IntModule.OfNatModule.ofNatModule + instance IsRightCancelAdd.toGrindAddRightCancel [AddSemigroup α] [IsRightCancelAdd α] : Grind.AddRightCancel α where add_right_cancel _ _ _ := add_right_cancel From 559d5188a8fa9e701ae3a32aec0706d2a3938312 Mon Sep 17 00:00:00 2001 From: Claude Date: Sat, 30 May 2026 22:23:34 +0000 Subject: [PATCH 2/2] chore: use priority 1100 for Grind.IntModule.OfNatModule.ofNatModule https://claude.ai/code/session_01Xq5Eavd4WbKAosAW4p2xXg --- Mathlib/Algebra/Group/Basic.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Mathlib/Algebra/Group/Basic.lean b/Mathlib/Algebra/Group/Basic.lean index 922eca27753ee9..c62e2142f4ad6e 100644 --- a/Mathlib/Algebra/Group/Basic.lean +++ b/Mathlib/Algebra/Group/Basic.lean @@ -1088,9 +1088,9 @@ 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 high priority, +-- 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 high] Lean.Grind.IntModule.OfNatModule.ofNatModule +attribute [instance 1100] Lean.Grind.IntModule.OfNatModule.ofNatModule instance IsRightCancelAdd.toGrindAddRightCancel [AddSemigroup α] [IsRightCancelAdd α] : Grind.AddRightCancel α where