diff --git a/src/Init/Data/Int/Linear.lean b/src/Init/Data/Int/Linear.lean
index b46ba794a6..5850199ec4 100644
--- a/src/Init/Data/Int/Linear.lean
+++ b/src/Init/Data/Int/Linear.lean
@@ -1524,7 +1524,7 @@ private theorem cooper_right_core
   have d_pos : (0 : Int) < 1 := by decide
   have h₃ : 1 ∣ 0*x + 0 := Int.one_dvd _
   have h := cooper_dvd_right_core a_neg b_pos d_pos h₁ h₂ h₃
-  simp only [Int.mul_one, gcd_zero, Int.natAbs_of_nonneg (Int.le_of_lt b_pos), 
+  simp only [Int.mul_one, gcd_zero, Int.natAbs_of_nonneg (Int.le_of_lt b_pos),
     Int.ediv_self (Int.ne_of_gt b_pos), lcm_one,
     Int.zero_mul, Int.mul_zero, Int.add_zero, Int.dvd_zero,
     and_true, Int.neg_zero] at h
@@ -1915,6 +1915,11 @@ theorem eq_def (ctx : Context) (x : Var) (xPoly : Poly) (p : Poly)
   simp [eq_def_cert]; intro _ h; subst p; simp [h]
   rw [← Int.sub_eq_add_neg, Int.sub_self]
 
+theorem eq_def_norm (ctx : Context) (x : Var) (xPoly xPoly' : Poly) (p : Poly)
+    : eq_def_cert x xPoly' p → x.denote ctx = xPoly.denote' ctx → xPoly.denote' ctx = xPoly'.denote' ctx → p.denote' ctx = 0 := by
+  simp [eq_def_cert]; intro _ h₁ h₂; subst p; simp [h₁, h₂]
+  rw [← Int.sub_eq_add_neg, Int.sub_self]
+
 @[expose]
 def eq_def'_cert (x : Var) (e : Expr) (p : Poly) : Bool :=
   p == .add (-1) x e.norm
@@ -1924,6 +1929,27 @@ theorem eq_def' (ctx : Context) (x : Var) (e : Expr) (p : Poly)
   simp [eq_def'_cert]; intro _ h; subst p; simp [h]
   rw [← Int.sub_eq_add_neg, Int.sub_self]
 
+@[expose]
+def eq_def'_norm_cert (x : Var) (e : Expr) (ePoly ePoly' p : Poly) : Bool :=
+  ePoly == e.norm && p == .add (-1) x ePoly'
+
+theorem eq_def'_norm (ctx : Context) (x : Var) (e : Expr) (ePoly ePoly' : Poly) (p : Poly)
+    : eq_def'_norm_cert x e ePoly ePoly' p → x.denote ctx = e.denote ctx → ePoly.denote' ctx = ePoly'.denote' ctx → p.denote' ctx = 0 := by
+  simp [eq_def'_norm_cert]; intro _ _ h₁ h₂; subst ePoly p; simp [h₁, ← h₂]
+  rw [← Int.sub_eq_add_neg, Int.sub_self]
+
+theorem eq_norm_poly (ctx : Context) (p p' : Poly) : p.denote' ctx = p'.denote' ctx → p.denote' ctx = 0 → p'.denote' ctx = 0 := by
+  intro h; rw [h]; simp
+
+theorem le_norm_poly (ctx : Context) (p p' : Poly) : p.denote' ctx = p'.denote' ctx → p.denote' ctx ≤ 0 → p'.denote' ctx ≤ 0 := by
+  intro h; rw [h]; simp
+
+theorem diseq_norm_poly (ctx : Context) (p p' : Poly) : p.denote' ctx = p'.denote' ctx → p.denote' ctx ≠ 0 → p'.denote' ctx ≠ 0 := by
+  intro h; rw [h]; simp
+
+theorem dvd_norm_poly (ctx : Context) (d : Int) (p p' : Poly) : p.denote' ctx = p'.denote' ctx → d ∣ p.denote' ctx → d ∣ p'.denote' ctx := by
+  intro h; rw [h]; simp
+
 end Int.Linear
 
 theorem Int.not_le_eq (a b : Int) : (¬a ≤ b) = (b + 1 ≤ a) := by
diff --git a/src/Init/Grind/Ring/Poly.lean b/src/Init/Grind/Ring/Poly.lean
index aeee024c5b..e34ce8d933 100644
--- a/src/Init/Grind/Ring/Poly.lean
+++ b/src/Init/Grind/Ring/Poly.lean
@@ -13,7 +13,7 @@ public import Init.Data.RArray
 public import Init.Grind.Ring.Basic
 public import Init.Grind.Ring.Field
 public import Init.Grind.Ordered.Ring
-
+public import Init.GrindInstances.Ring.Int
 public section
 
 namespace Lean.Grind
@@ -97,6 +97,17 @@ def Mon.denote {α} [Semiring α] (ctx : Context α) : Mon → α
   | unit => 1
   | .mult p m => p.denote ctx * denote ctx m
 
+@[expose]
+def Mon.denote' {α} [Semiring α] (ctx : Context α) (m : Mon) : α :=
+  match m with
+  | .unit => 1
+  | .mult pw m => go m (pw.denote ctx)
+where
+  go (m : Mon) (acc : α) : α :=
+    match m with
+    | .unit => acc
+    | .mult pw m => go m (acc * (pw.denote ctx))
+
 @[expose]
 def Mon.ofVar (x : Var) : Mon :=
   .mult { x, k := 1 } .unit
@@ -236,6 +247,24 @@ def Poly.denote [Ring α] (ctx : Context α) (p : Poly) : α :=
   | .num k => Int.cast k
   | .add k m p => Int.cast k * m.denote ctx + denote ctx p
 
+@[expose]
+def Poly.denote' [Ring α] (ctx : Context α) (p : Poly) : α :=
+  match p with
+  | .num k => Int.cast k
+  | .add k m p => go p (denoteTerm k m)
+where
+  denoteTerm (k : Int) (m : Mon) : α :=
+    bif k == 1 then
+      m.denote' ctx
+    else
+      Int.cast k * m.denote' ctx
+
+  go (p : Poly) (acc : α) : α :=
+    match p with
+    | .num 0 => acc
+    | .num k => acc + Int.cast k
+    | .add k m p => go p (acc + denoteTerm k m)
+
 @[expose]
 def Poly.ofMon (m : Mon) : Poly :=
   .add 1 m (.num 0)
@@ -576,6 +605,14 @@ theorem Power.denote_eq {α} [Semiring α] (ctx : Context α) (p : Power)
     : p.denote ctx = p.x.denote ctx ^ p.k := by
   cases p <;> simp [Power.denote] <;> split <;> simp [pow_zero, pow_succ, one_mul]
 
+theorem Mon.denote'_eq_denote {α} [Semiring α] (ctx : Context α) (m : Mon) : m.denote' ctx = m.denote ctx := by
+  cases m <;> simp [denote', denote]
+  next pw m =>
+  generalize pw.denote ctx = acc
+  fun_induction denote'.go
+  next => simp [denote, Semiring.mul_one]
+  next acc pw m ih => simp [ih, denote, Semiring.mul_assoc]
+
 theorem Mon.denote_ofVar {α} [Semiring α] (ctx : Context α) (x : Var)
     : denote ctx (ofVar x) = x.denote ctx := by
   simp [denote, ofVar, Power.denote_eq, pow_succ, pow_zero, one_mul, mul_one]
@@ -658,6 +695,16 @@ theorem Mon.eq_of_revlex {m₁ m₂ : Mon} : revlex m₁ m₂ = .eq → m₁ = m
 theorem Mon.eq_of_grevlex {m₁ m₂ : Mon} : grevlex m₁ m₂ = .eq → m₁ = m₂ := by
   simp [grevlex]; intro; apply eq_of_revlex
 
+theorem Poly.denoteTerm_eq  {α} [Ring α] (ctx : Context α) (k : Int) (m : Mon) : denote'.denoteTerm ctx k m = k * m.denote ctx := by
+  simp [denote'.denoteTerm, Mon.denote'_eq_denote, cond_eq_if]; intro; subst k; rw [Ring.intCast_one, Semiring.one_mul]
+
+theorem Poly.denote'_eq_denote {α} [Ring α] (ctx : Context α) (p : Poly) : p.denote' ctx = p.denote ctx := by
+  cases p <;> simp [denote', denote, denoteTerm_eq]
+  next k m p =>
+    generalize k * m.denote ctx = acc
+    fun_induction denote'.go <;> simp [denote, *, Ring.intCast_zero, Semiring.add_zero, denoteTerm_eq]
+    next ih => simp [denoteTerm_eq] at ih; simp [ih, Semiring.add_assoc]
+
 theorem Poly.denote_ofMon {α} [CommRing α] (ctx : Context α) (m : Mon)
     : denote ctx (ofMon m) = m.denote ctx := by
   simp [ofMon, denote, intCast_one, intCast_zero, one_mul, add_zero]
@@ -1379,6 +1426,7 @@ theorem Poly.normEq0_eq {α} [CommRing α] (ctx : Context α) (p : Poly) (c : Na
     simp [denote, normEq0]; split <;> simp [denote, *]
     next h' => rw [of_mod_eq_0 h h', Semiring.zero_mul, Semiring.zero_add]
 
+@[expose]
 def eq_normEq0_cert (c : Nat) (p₁ p₂ p : Poly) : Bool :=
   p₁ == .num c && p == p₂.normEq0 c
 
@@ -1398,6 +1446,7 @@ theorem gcd_eq_0 [CommRing α] (g n m a b : Int) (h : g = a * n + b * m)
   rw [← Ring.intCast_add, h₂, Semiring.zero_add, ← h] at h₁
   rw [Ring.intCast_zero, h₁]
 
+@[expose]
 def eq_gcd_cert (a b : Int) (p₁ p₂ p : Poly) : Bool :=
   match p₁ with
   | .add .. => false
@@ -1415,6 +1464,7 @@ theorem eq_gcd {α} [CommRing α] (ctx : Context α) (a b : Int) (p₁ p₂ p :
   next n m g =>
   apply gcd_eq_0 g n m a b
 
+@[expose]
 def d_normEq0_cert (c : Nat) (p₁ p₂ p : Poly) : Bool :=
   p₂ == .num c && p == p₁.normEq0 c
 
@@ -1423,5 +1473,11 @@ theorem d_normEq0 {α} [CommRing α] (ctx : Context α) (k : Int) (c : Nat) (ini
   simp [d_normEq0_cert]; intro _ h₁ h₂; subst p p₂; simp [Poly.denote]
   intro h; rw [p₁.normEq0_eq] <;> assumption
 
+@[expose] def norm_int_cert (e : Expr) (p : Poly) : Bool :=
+  e.toPoly == p
+
+theorem norm_int (ctx : Context Int) (e : Expr) (p : Poly) : norm_int_cert e p → e.denote ctx = p.denote' ctx := by
+  simp [norm_int_cert, Poly.denote'_eq_denote]; intro; subst p; simp [Expr.denote_toPoly]
+
 end CommRing
 end Lean.Grind
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat.lean
index b133326811..88cd5f1b0e 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat.lean
@@ -18,6 +18,7 @@ import Lean.Meta.Tactic.Grind.Arith.Cutsat.SearchM
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.Model
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.MBTC
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.Nat
+import Lean.Meta.Tactic.Grind.Arith.Cutsat.CommRing
 
 namespace Lean
 
@@ -27,6 +28,7 @@ builtin_initialize registerTraceClass `grind.cutsat.assert
 builtin_initialize registerTraceClass `grind.cutsat.assert.trivial
 builtin_initialize registerTraceClass `grind.cutsat.assert.unsat
 builtin_initialize registerTraceClass `grind.cutsat.assert.store
+builtin_initialize registerTraceClass `grind.cutsat.assert.nonlinear
 
 builtin_initialize registerTraceClass `grind.debug.cutsat.subst
 builtin_initialize registerTraceClass `grind.debug.cutsat.search
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/CommRing.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/CommRing.lean
new file mode 100644
index 0000000000..f2ecc8b8c5
--- /dev/null
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/CommRing.lean
@@ -0,0 +1,58 @@
+/-
+Copyright (c) 2025 Amazon.com, Inc. or its affiliates. All Rights Reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import Lean.Meta.Tactic.Grind.ProveEq
+import Lean.Meta.Tactic.Grind.Arith.CommRing.RingId
+import Lean.Meta.Tactic.Grind.Arith.CommRing.Reify
+import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
+import Lean.Meta.Tactic.Grind.Arith.Cutsat.Var
+
+/-!
+CommRing interface for cutsat. We use it to normalize nonlinear polynomials.
+-/
+
+namespace Lean.Meta.Grind.Arith.Cutsat
+
+/-- Returns `true` if `p` contains a nonlinear monomial. -/
+def _root_.Int.Linear.Poly.isNonlinear (p : Poly) : GoalM Bool := do
+  let .add _ x p := p | return false
+  if (← getVar x).isAppOf ``HMul.hMul then return true
+  p.isNonlinear
+
+def _root_.Int.Linear.Poly.getGeneration (p : Poly) : GoalM Nat := do
+  go p 0
+where
+  go : Poly → Nat → GoalM Nat
+  | .num _, gen => return gen
+  | .add _ x p, gen => do go p (max (← Grind.getGeneration (← getVar x)) gen)
+
+def getIntRingId? : GoalM (Option Nat) := do
+  CommRing.getRingId? (← getIntExpr)
+
+/-- Normalize the polynomial using `CommRing`-/
+def _root_.Int.Linear.Poly.normCommRing? (p : Poly) : GoalM (Option (CommRing.RingExpr × CommRing.Poly × Poly)) := do
+  unless (← p.isNonlinear) do return none
+  let some ringId ← getIntRingId? | return none
+  CommRing.RingM.run ringId do
+    let e ← p.denoteExpr'
+    -- TODO: we can avoid the following statement if we construct the `Int` denotation using
+    -- Internalized operators instead of `mkIntMul` and `mkIntAdd`
+    let e ← shareCommon (← canon e)
+    let gen ← p.getGeneration
+    let some re ← CommRing.reify? e (gen := gen) | return none
+    let p' := re.toPoly
+    let e' ← p'.denoteExpr
+    let e' ← preprocessLight e'
+    -- Remark: we are reusing the `IntModule` virtual parent.
+    -- TODO: Investigate whether we should have a custom virtual parent for cutsat
+    internalize e' gen (some getIntModuleVirtualParent)
+    let p'' ← toPoly e'
+    if p == p'' then return none
+    modify' fun s => { s with usedCommRing := true }
+    trace[grind.cutsat.assert.nonlinear] "{← p.pp} ===> {← p''.pp}"
+    return some (re, p', p'')
+
+end Lean.Meta.Grind.Arith.Cutsat
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/DvdCnstr.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/DvdCnstr.lean
index 440e41268e..152ad76c14 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/DvdCnstr.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/DvdCnstr.lean
@@ -85,6 +85,14 @@ partial def DvdCnstr.assert (c : DvdCnstr) : GoalM Unit := withIncRecDepth do
     c.p.updateOccs
     modify' fun s => { s with dvds := s.dvds.set x (some c) }
 
+/-- Asserts a constraint coming from the core. -/
+private def DvdCnstr.assertCore (c : DvdCnstr) : GoalM Unit := do
+  if let some (re, rp, p) ← c.p.normCommRing? then
+    let c := { c with p, h := .commRingNorm c re rp : DvdCnstr}
+    c.assert
+  else
+    c.assert
+
 def propagateIntDvd (e : Expr) : GoalM Unit := do
   let_expr Dvd.dvd _ inst a b ← e | return ()
   unless (← isInstDvdInt inst) do return ()
@@ -94,7 +102,7 @@ def propagateIntDvd (e : Expr) : GoalM Unit := do
   if (← isEqTrue e) then
     let p ← toPoly b
     let c := { d, p, h := .core e : DvdCnstr }
-    c.assert
+    c.assertCore
   else if (← isEqFalse e) then
     pushNewFact <| mkApp4 (mkConst ``Int.Linear.of_not_dvd) a b reflBoolTrue (mkOfEqFalseCore e (← mkEqFalseProof e))
 
@@ -106,7 +114,7 @@ def propagateNatDvd (e : Expr) : GoalM Unit := do
   let p := b'.norm
   if (← isEqTrue e) then
     let c := { d, p, h := .coreNat e d b b' : DvdCnstr }
-    c.assert
+    c.assertCore
   else if (← isEqFalse e) then
     let_expr Dvd.dvd _ _ a b ← e | return ()
     pushNewFact <| mkApp3 (mkConst ``Nat.emod_pos_of_not_dvd) a b (mkOfEqFalseCore e (← mkEqFalseProof e))
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean
index 3348bfa685..1ea2ccb29a 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/EqCnstr.lean
@@ -9,6 +9,7 @@ import Lean.Meta.Tactic.Grind.Arith.Cutsat.Var
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.DvdCnstr
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.LeCnstr
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
+import Lean.Meta.Tactic.Grind.Arith.Cutsat.CommRing
 
 namespace Lean.Meta.Grind.Arith.Cutsat
 
@@ -223,9 +224,18 @@ private def exprAsPoly (a : Expr) : GoalM Poly := do
 private def processNewIntEq (a b : Expr) : GoalM Unit := do
   let p₁ ← exprAsPoly a
   let p₂ ← exprAsPoly b
+  -- Remark: we don't need to use the comm ring normalizer here because `p` is always linear.
   let p := p₁.combine (p₂.mul (-1))
   { p, h := .core a b p₁ p₂ : EqCnstr }.assert
 
+/-- Asserts a constraint coming from the core. -/
+private def EqCnstr.assertCore (c : EqCnstr) : GoalM Unit := do
+  if let some (re, rp, p) ← c.p.normCommRing? then
+    let c := { p, h := .commRingNorm c re rp : EqCnstr}
+    c.assert
+  else
+    c.assert
+
 private def processNewNatEq (a b : Expr) : GoalM Unit := do
   let (lhs, rhs) ← Int.OfNat.toIntEq a b
   let gen ← getGeneration a
@@ -235,7 +245,7 @@ private def processNewNatEq (a b : Expr) : GoalM Unit := do
   let p := lhs'.sub rhs' |>.norm
   let c := { p, h := .coreNat a b lhs rhs lhs' rhs' : EqCnstr }
   trace[grind.debug.cutsat.nat] "{← c.pp}"
-  c.assert
+  c.assertCore
 
 private def processNewToIntEq (a b : Expr) : ToIntM Unit := do
   let gen := max (← getGeneration a) (← getGeneration b)
@@ -246,7 +256,7 @@ private def processNewToIntEq (a b : Expr) : ToIntM Unit := do
   let rhs ← toLinearExpr b' gen
   let p := lhs.sub rhs |>.norm
   let c := { p, h := .coreToInt a b thm lhs rhs : EqCnstr }
-  c.assert
+  c.assertCore
 
 @[export lean_process_cutsat_eq]
 def processNewEqImpl (a b : Expr) : GoalM Unit := do
@@ -262,6 +272,8 @@ def processNewEqImpl (a b : Expr) : GoalM Unit := do
     ToIntM.run α do processNewToIntEq a b
 
 private def processNewIntDiseq (a b : Expr) : GoalM Unit := do
+  -- Remark: we don't need to use comm ring to normalize these polynomials because they are
+  -- always linear.
   let p₁ ← exprAsPoly a
   let c ← if let some 0 ← getIntValue? b then
     pure { p := p₁, h := .core0 a b : DiseqCnstr }
@@ -271,6 +283,14 @@ private def processNewIntDiseq (a b : Expr) : GoalM Unit := do
     pure {p, h := .core a b p₁ p₂ : DiseqCnstr }
   c.assert
 
+/-- Asserts a constraint coming from the core. -/
+private def DiseqCnstr.assertCore (c : DiseqCnstr) : GoalM Unit := do
+  if let some (re, rp, p) ← c.p.normCommRing? then
+    let c := { p, h := .commRingNorm c re rp : DiseqCnstr }
+    c.assert
+  else
+    c.assert
+
 private def processNewNatDiseq (a b : Expr) : GoalM Unit := do
   let (lhs, rhs) ← Int.OfNat.toIntEq a b
   let gen ← getGeneration a
@@ -279,7 +299,7 @@ private def processNewNatDiseq (a b : Expr) : GoalM Unit := do
   let rhs' ← toLinearExpr (← rhs.denoteAsIntExpr ctx) gen
   let p := lhs'.sub rhs' |>.norm
   let c := { p, h := .coreNat a b lhs rhs lhs' rhs' : DiseqCnstr }
-  c.assert
+  c.assertCore
 
 private def processNewToIntDiseq (a b : Expr) : ToIntM Unit := do
   let gen := max (← getGeneration a) (← getGeneration b)
@@ -290,7 +310,7 @@ private def processNewToIntDiseq (a b : Expr) : ToIntM Unit := do
   let rhs ← toLinearExpr b' gen
   let p := lhs.sub rhs |>.norm
   let c := { p, h := .coreToInt a b thm lhs rhs : DiseqCnstr }
-  c.assert
+  c.assertCore
 
 @[export lean_process_cutsat_diseq]
 def processNewDiseqImpl (a b : Expr) : GoalM Unit := do
@@ -352,8 +372,12 @@ private def internalizeInt (e : Expr) : GoalM Unit := do
     -- It is pointless to assert `x = x`
     -- This can happen if `e` is a nonlinear term (e.g., `e` is `a*b`)
     return
-  let c := { p := .add (-1) x p, h := .defn e p : EqCnstr }
-  c.assert
+  if let some (re, rp, p') ← p.normCommRing? then
+    let c := { p := .add (-1) x p', h := .defnCommRing e p re rp p' : EqCnstr }
+    c.assert
+  else
+    let c := { p := .add (-1) x p, h := .defn e p : EqCnstr }
+    c.assert
 
 private def expandDivMod (a : Expr) (b : Int) : GoalM Unit := do
   if b == 0 || b == 1 || b == -1 then
@@ -411,8 +435,12 @@ private def internalizeNat (e : Expr) : GoalM Unit := do
   trace[grind.debug.cutsat.internalize] "{aquote natCast_e}:= {← p.pp}"
   let x ← mkVar natCast_e
   modify' fun s => { s with natDef := s.natDef.insert { expr := e } x }
-  let c := { p := .add (-1) x p, h := .defnNat e' x e'' : EqCnstr }
-  c.assert
+  if let some (re, rp, p') ← p.normCommRing? then
+    let c := { p := .add (-1) x p', h := .defnNatCommRing e' x e'' p re rp p' : EqCnstr }
+    c.assert
+  else
+    let c := { p := .add (-1) x p, h := .defnNat e' x e'' : EqCnstr }
+    c.assert
 
 private def isToIntForbiddenParent (parent? : Option Expr) : Bool :=
   if let some parent := parent? then
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/LeCnstr.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/LeCnstr.lean
index 56eb26b8b1..b6b92c89d1 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/LeCnstr.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/LeCnstr.lean
@@ -12,6 +12,7 @@ import Lean.Meta.Tactic.Grind.Arith.Cutsat.Proof
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.Nat
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.Norm
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
+import Lean.Meta.Tactic.Grind.Arith.Cutsat.CommRing
 
 namespace Lean.Meta.Grind.Arith.Cutsat
 
@@ -135,6 +136,14 @@ private def toPolyLe? (e : Expr) : GoalM (Option Poly) := do
     reportNonNormalized e; return none
   return some (← toPoly a)
 
+/-- Asserts a constraint coming from the core. -/
+private def LeCnstr.assertCore (c : LeCnstr) : GoalM Unit := do
+  if let some (re, rp, p) ← c.p.normCommRing? then
+    let c := { p, h := .commRingNorm c re rp : LeCnstr}
+    c.assert
+  else
+    c.assert
+
 /--
 Given an expression `e` that is in `True` (or `False` equivalence class), if `e` is an
 integer inequality, asserts it to the cutsat state.
@@ -145,7 +154,7 @@ def propagateIntLe (e : Expr) (eqTrue : Bool) : GoalM Unit := do
     pure { p, h := .core e : LeCnstr }
   else
     pure { p := p.mul (-1) |>.addConst 1, h := .coreNeg e p : LeCnstr }
-  c.assert
+  c.assertCore
 
 def propagateNatLe (e : Expr) (eqTrue : Bool) : GoalM Unit := do
   let some (lhs, rhs) ← Int.OfNat.toIntLe? e | return ()
@@ -158,7 +167,7 @@ def propagateNatLe (e : Expr) (eqTrue : Bool) : GoalM Unit := do
     pure { p, h := .coreNat e lhs rhs lhs' rhs' : LeCnstr }
   else
     pure { p := p.mul (-1) |>.addConst 1, h := .coreNatNeg e lhs rhs lhs' rhs' : LeCnstr }
-  c.assert
+  c.assertCore
 
 def propagateToIntLe (e : Expr) (eqTrue : Bool) : ToIntM Unit := do
   let some thm ← if eqTrue then pure (← getInfo).ofLE? else pure (← getInfo).ofNotLE? | return ()
@@ -172,7 +181,7 @@ def propagateToIntLe (e : Expr) (eqTrue : Bool) : ToIntM Unit := do
   let rhs ← toLinearExpr b' gen
   let p := lhs.sub rhs |>.norm
   let c := { p, h := .coreToInt e eqTrue thm lhs rhs : LeCnstr }
-  c.assert
+  c.assertCore
 
 def propagateLe (e : Expr) (eqTrue : Bool) : GoalM Unit := do
   unless (← getConfig).cutsat do return ()
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean
index 71a281bd03..31bbf617bb 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean
@@ -4,11 +4,15 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
 prelude
+import Init.Grind.Ring.Poly
 import Lean.Meta.Tactic.Grind.Diseq
 import Lean.Meta.Tactic.Grind.Arith.Util
 import Lean.Meta.Tactic.Grind.Arith.ProofUtil
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.Nat
+import Lean.Meta.Tactic.Grind.Arith.Cutsat.CommRing
+import Lean.Meta.Tactic.Grind.Arith.CommRing.Util
+import Lean.Meta.Tactic.Grind.Arith.CommRing.Proof
 
 namespace Lean.Meta.Grind.Arith.Cutsat
 
@@ -20,12 +24,15 @@ structure ProofM.State where
   polyMap     : Std.HashMap Poly Expr := {}
   exprMap     : Std.HashMap Int.Linear.Expr Expr := {}
   natExprMap  : Std.HashMap Int.OfNat.Expr Expr := {}
+  ringPolyMap : Std.HashMap CommRing.Poly Expr := {}
+  ringExprMap : Std.HashMap CommRing.RingExpr Expr := {}
 
 structure ProofM.Context where
   ctx       : Expr
   /-- Variables before reordering -/
   ctx'      : Expr
   natCtx    : Expr
+  ringCtx   : Expr
   /--
   `unordered` is `true` if we entered a `.reorder c` justification. The variables in `c` and
   its dependencies are unordered.
@@ -64,27 +71,41 @@ private abbrev caching (c : α) (k : ProofM Expr) : ProofM Expr := do
     modify fun s => { s with cache := s.cache.insert addr h }
     return h
 
-def mkPolyDecl (p : Poly) : ProofM Expr := do
+private def mkPolyDecl (p : Poly) : ProofM Expr := do
   if let some x := (← get).polyMap[p]? then
     return x
   let x := mkFVar (← mkFreshFVarId)
   modify fun s => { s with polyMap := s.polyMap.insert p x }
   return x
 
-def mkExprDecl (e : Int.Linear.Expr) : ProofM Expr := do
+private def mkExprDecl (e : Int.Linear.Expr) : ProofM Expr := do
   if let some x := (← get).exprMap[e]? then
     return x
   let x := mkFVar (← mkFreshFVarId)
   modify fun s => { s with exprMap := s.exprMap.insert e x }
   return x
 
-def mkNatExprDecl (e : Int.OfNat.Expr) : ProofM Expr := do
+private def mkNatExprDecl (e : Int.OfNat.Expr) : ProofM Expr := do
   if let some x := (← get).natExprMap[e]? then
     return x
   let x := mkFVar (← mkFreshFVarId)
   modify fun s => { s with natExprMap := s.natExprMap.insert e x }
   return x
 
+private def mkRingPolyDecl (p : CommRing.Poly) : ProofM Expr := do
+  if let some x := (← get).ringPolyMap[p]? then
+    return x
+  let x := mkFVar (← mkFreshFVarId)
+  modify fun s => { s with ringPolyMap := s.ringPolyMap.insert p x }
+  return x
+
+private def mkRingExprDecl (e : CommRing.RingExpr) : ProofM Expr := do
+  if let some x := (← get).ringExprMap[e]? then
+    return x
+  let x := mkFVar (← mkFreshFVarId)
+  modify fun s => { s with ringExprMap := s.ringExprMap.insert e x }
+  return x
+
 private def toContextExprCore (vars : PArray Expr) (type : Expr) : MetaM Expr :=
   if h : 0 < vars.size then
     RArray.toExpr type id (RArray.ofFn (vars[·]) h)
@@ -100,18 +121,34 @@ private def toContextExpr' : GoalM Expr := do
 private def toNatContextExpr : GoalM Expr := do
   toContextExprCore (← getNatVars) Nat.mkType
 
+private def toRingContextExpr : GoalM Expr := do
+  if (← get').usedCommRing then
+    if let some ringId ← getIntRingId? then
+      return (← CommRing.RingM.run ringId do CommRing.toContextExpr)
+  RArray.toExpr Int.mkType id (RArray.leaf (mkIntLit 0))
+
 private abbrev withProofContext (x : ProofM Expr) : GoalM Expr := do
   withLetDecl `ctx (mkApp (mkConst ``RArray [levelZero]) Int.mkType) (← toContextExpr) fun ctx => do
   withLetDecl `ctx' (mkApp (mkConst ``RArray [levelZero]) Int.mkType) (← toContextExpr') fun ctx' => do
+  withLetDecl `rctx (mkApp (mkConst ``RArray [levelZero]) Int.mkType) (← toRingContextExpr) fun ringCtx => do
   withLetDecl `nctx (mkApp (mkConst ``RArray [levelZero]) Nat.mkType) (← toNatContextExpr) fun natCtx => do
-    go { ctx, ctx', natCtx } |>.run' {}
+    go { ctx, ctx', ringCtx, natCtx } |>.run' {}
 where
   go : ProofM Expr := do
     let h ← x
     let h ← mkLetOfMap (← get).polyMap h `p (mkConst ``Int.Linear.Poly) toExpr
     let h ← mkLetOfMap (← get).exprMap h `e (mkConst ``Int.Linear.Expr) toExpr
     let h ← mkLetOfMap (← get).natExprMap h `a (mkConst ``Int.OfNat.Expr) toExpr
-    mkLetFVars #[(← getContext), (← read).ctx', (← getNatContext)] h
+    let h ← mkLetOfMap (← get).ringPolyMap h `rp (mkConst ``Grind.CommRing.Poly) toExpr
+    let h ← mkLetOfMap (← get).ringExprMap h `re (mkConst ``Grind.CommRing.Expr) toExpr
+    mkLetFVars #[(← getContext), (← read).ctx', (← read).ringCtx, (← getNatContext)] h
+
+/--
+Returns a Lean expression representing the auxiliary `CommRing` variable context needed for normalizing
+nonlinear polynomials.
+-/
+private abbrev getRingContext : ProofM Expr := do
+  return (← read).ringCtx
 
 private def DvdCnstr.get_d_a (c : DvdCnstr) : GoalM (Int × Int) := do
   let d := c.d
@@ -154,6 +191,20 @@ partial def EqCnstr.toExprProof (c' : EqCnstr) : ProofM Expr := caching c' do
       (← getContext) (← mkPolyDecl c₁.p) (← mkPolyDecl c₂.p)
       reflBoolTrue (← c₁.toExprProof) (← c₂.toExprProof)
   | .reorder c => withUnordered <| c.toExprProof
+  | .commRingNorm c e p =>
+    let h := mkApp4 (mkConst ``Grind.CommRing.norm_int) (← getRingContext) (← mkRingExprDecl e) (← mkRingPolyDecl p) reflBoolTrue
+    return mkApp5 (mkConst ``Int.Linear.eq_norm_poly) (← getContext) (← mkPolyDecl c.p) (← mkPolyDecl c'.p) h (← c.toExprProof)
+  | .defnCommRing e p re rp p' =>
+    let h := mkApp4 (mkConst ``Grind.CommRing.norm_int) (← getRingContext) (← mkRingExprDecl re) (← mkRingPolyDecl rp) reflBoolTrue
+    let some x := (← getVarMap).find? { expr := e } | throwError "`grind` internal error, missing cutsat variable{indentExpr e}"
+    return mkApp8 (mkConst ``Int.Linear.eq_def_norm) (← getContext)
+      (toExpr x) (← mkPolyDecl p) (← mkPolyDecl p') (← mkPolyDecl c'.p)
+      reflBoolTrue (← mkEqRefl e) h
+  | .defnNatCommRing e x e' p re rp p' =>
+    let h₁ := mkApp2 (mkConst ``Int.OfNat.Expr.eq_denoteAsInt) (← getNatContext) (← mkNatExprDecl e)
+    let h₂ := mkApp4 (mkConst ``Grind.CommRing.norm_int) (← getRingContext) (← mkRingExprDecl re) (← mkRingPolyDecl rp) reflBoolTrue
+    return mkApp9 (mkConst ``Int.Linear.eq_def'_norm) (← getContext) (toExpr x) (← mkExprDecl e')
+      (← mkPolyDecl p) (← mkPolyDecl p') (← mkPolyDecl c'.p) reflBoolTrue h₁ h₂
 
 partial def DvdCnstr.toExprProof (c' : DvdCnstr) : ProofM Expr := caching c' do
   trace[grind.debug.cutsat.proof] "{← c'.pp}"
@@ -216,6 +267,9 @@ partial def DvdCnstr.toExprProof (c' : DvdCnstr) : ProofM Expr := caching c' do
       (← getContext) (← mkPolyDecl p₁) (← mkPolyDecl p₂) (← mkPolyDecl c₃.p) (toExpr c₃.d) (toExpr s.k) (toExpr c'.d) (← mkPolyDecl c'.p)
       (← s.toExprProof) reflBoolTrue
   | .reorder c => withUnordered <| c.toExprProof
+  | .commRingNorm c e p =>
+    let h := mkApp4 (mkConst ``Grind.CommRing.norm_int) (← getRingContext) (← mkRingExprDecl e) (← mkRingPolyDecl p) reflBoolTrue
+    return mkApp6 (mkConst ``Int.Linear.dvd_norm_poly) (← getContext) (toExpr c.d) (← mkPolyDecl c.p) (← mkPolyDecl c'.p) h (← c.toExprProof)
 
 partial def LeCnstr.toExprProof (c' : LeCnstr) : ProofM Expr := caching c' do
   trace[grind.debug.cutsat.proof] "{← c'.pp}"
@@ -302,6 +356,9 @@ partial def LeCnstr.toExprProof (c' : LeCnstr) : ProofM Expr := caching c' do
       return mkApp10 (mkConst thmName)
         (← getContext) (← mkPolyDecl p₁) (← mkPolyDecl p₂) (← mkPolyDecl c₃.p) (toExpr c₃.d) (toExpr s.k) (toExpr coeff) (← mkPolyDecl c'.p) (← s.toExprProof) reflBoolTrue
   | .reorder c => withUnordered <| c.toExprProof
+  | .commRingNorm c e p =>
+    let h := mkApp4 (mkConst ``Grind.CommRing.norm_int) (← getRingContext) (← mkRingExprDecl e) (← mkRingPolyDecl p) reflBoolTrue
+    return mkApp5 (mkConst ``Int.Linear.le_norm_poly) (← getContext) (← mkPolyDecl c.p) (← mkPolyDecl c'.p) h (← c.toExprProof)
 
 partial def DiseqCnstr.toExprProof (c' : DiseqCnstr) : ProofM Expr := caching c' do
   match c'.h with
@@ -329,6 +386,9 @@ partial def DiseqCnstr.toExprProof (c' : DiseqCnstr) : ProofM Expr := caching c'
       (← getContext) (toExpr x) (← mkPolyDecl c₁.p) (← mkPolyDecl c₂.p) (← mkPolyDecl c'.p)
       reflBoolTrue (← c₁.toExprProof) (← c₂.toExprProof)
   | .reorder c => withUnordered <| c.toExprProof
+  | .commRingNorm c e p =>
+    let h := mkApp4 (mkConst ``Grind.CommRing.norm_int) (← getRingContext) (← mkRingExprDecl e) (← mkRingPolyDecl p) reflBoolTrue
+    return mkApp5 (mkConst ``Int.Linear.diseq_norm_poly) (← getContext) (← mkPolyDecl c.p) (← mkPolyDecl c'.p) h (← c.toExprProof)
 
 partial def CooperSplit.toExprProof (s : CooperSplit) : ProofM Expr := caching s do
   match s.h with
@@ -412,8 +472,9 @@ open CollectDecVars
 mutual
 partial def EqCnstr.collectDecVars (c' : EqCnstr) : CollectDecVarsM Unit := do unless (← alreadyVisited c') do
   match c'.h with
-  | .core0 .. | .core .. | .coreNat .. | .defn .. | .defnNat .. | .coreToInt .. => return () -- Equalities coming from the core never contain cutsat decision variables
-  | .reorder c | .norm c | .divCoeffs c => c.collectDecVars
+  | .core0 .. | .core .. | .coreNat .. | .defn .. | .defnNat ..
+  | .defnCommRing .. | .defnNatCommRing .. | .coreToInt .. => return () -- Equalities coming from the core never contain cutsat decision variables
+  | .commRingNorm c .. | .reorder c | .norm c | .divCoeffs c => c.collectDecVars
   | .subst _ c₁ c₂ | .ofLeGe c₁ c₂ => c₁.collectDecVars; c₂.collectDecVars
 
 partial def CooperSplit.collectDecVars (s : CooperSplit) : CollectDecVarsM Unit := do unless (← alreadyVisited s) do
@@ -429,14 +490,15 @@ partial def DvdCnstr.collectDecVars (c' : DvdCnstr) : CollectDecVarsM Unit := do
   match c'.h with
   | .core _ | .coreNat .. => return ()
   | .cooper₁ c | .cooper₂ c
-  | .reorder c | .norm c | .elim c | .divCoeffs c | .ofEq _ c => c.collectDecVars
+  | .commRingNorm c .. | .reorder c | .norm c | .elim c | .divCoeffs c | .ofEq _ c => c.collectDecVars
   | .solveCombine c₁ c₂ | .solveElim c₁ c₂ | .subst _ c₁ c₂ => c₁.collectDecVars; c₂.collectDecVars
 
 partial def LeCnstr.collectDecVars (c' : LeCnstr) : CollectDecVarsM Unit := do unless (← alreadyVisited c') do
   match c'.h with
   | .core .. | .coreNeg .. | .coreNat .. | .coreNatNeg .. | .coreToInt .. | .denoteAsIntNonneg .. | .bound .. => return ()
   | .dec h => markAsFound h
-  | .reorder c | .cooper c | .norm c | .divCoeffs c => c.collectDecVars
+  | .commRingNorm c .. | .reorder c | .cooper c
+  | .norm c | .divCoeffs c => c.collectDecVars
   | .dvdTight c₁ c₂ | .negDvdTight c₁ c₂
   | .combine c₁ c₂ | .combineDivCoeffs c₁ c₂ _
   | .subst _ c₁ c₂ | .ofLeDiseq c₁ c₂ => c₁.collectDecVars; c₂.collectDecVars
@@ -445,7 +507,7 @@ partial def LeCnstr.collectDecVars (c' : LeCnstr) : CollectDecVarsM Unit := do u
 partial def DiseqCnstr.collectDecVars (c' : DiseqCnstr) : CollectDecVarsM Unit := do unless (← alreadyVisited c') do
   match c'.h with
   | .core0 .. | .core .. | .coreNat .. | .coreToInt .. => return () -- Disequalities coming from the core never contain cutsat decision variables
-  | .reorder c | .norm c | .divCoeffs c | .neg c => c.collectDecVars
+  | .commRingNorm c .. | .reorder c | .norm c | .divCoeffs c | .neg c => c.collectDecVars
   | .subst _ c₁ c₂  => c₁.collectDecVars; c₂.collectDecVars
 
 end
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Types.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Types.lean
index 5785ee0d5f..167d0b3562 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Types.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Types.lean
@@ -10,6 +10,7 @@ import Lean.Data.PersistentArray
 import Lean.Meta.Tactic.Grind.ExprPtr
 import Lean.Meta.Tactic.Grind.Arith.Util
 import Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
+import Lean.Meta.Tactic.Grind.Arith.CommRing.Types
 
 namespace Lean.Meta.Grind.Arith.Cutsat
 
@@ -95,6 +96,9 @@ inductive EqCnstrProof where
   | subst (x : Var) (c₁ : EqCnstr) (c₂ : EqCnstr)
   | ofLeGe (c₁ : LeCnstr) (c₂ : LeCnstr)
   | reorder (c : EqCnstr)
+  | commRingNorm (c : EqCnstr) (e : CommRing.RingExpr) (p : CommRing.Poly)
+  | defnCommRing (e : Expr) (p : Poly) (re : CommRing.RingExpr) (rp : CommRing.Poly) (p' : Poly)
+  | defnNatCommRing (e : Int.OfNat.Expr) (x : Var) (e' : Int.Linear.Expr) (p : Poly) (re : CommRing.RingExpr) (rp : CommRing.Poly) (p' : Poly)
 
 /-- A divisibility constraint and its justification/proof. -/
 structure DvdCnstr where
@@ -156,6 +160,7 @@ inductive DvdCnstrProof where
   /-- `c.c₃?` must be `some` -/
   | cooper₂ (c : CooperSplit)
   | reorder (c : DvdCnstr)
+  | commRingNorm (c : DvdCnstr) (e : CommRing.RingExpr) (p : CommRing.Poly)
 
 /-- An inequality constraint and its justification/proof. -/
 structure LeCnstr where
@@ -182,6 +187,7 @@ inductive LeCnstrProof where
   | dvdTight (c₁ : DvdCnstr) (c₂ : LeCnstr)
   | negDvdTight (c₁ : DvdCnstr) (c₂ : LeCnstr)
   | reorder (c : LeCnstr)
+  | commRingNorm (c : LeCnstr) (e : CommRing.RingExpr) (p : CommRing.Poly)
 
 /-- A disequality constraint and its justification/proof. -/
 structure DiseqCnstr where
@@ -203,6 +209,7 @@ inductive DiseqCnstrProof where
   | neg (c : DiseqCnstr)
   | subst (x : Var) (c₁ : EqCnstr) (c₂ : DiseqCnstr)
   | reorder (c : DiseqCnstr)
+  | commRingNorm (c : DiseqCnstr) (e : CommRing.RingExpr) (p : CommRing.Poly)
 
 /--
 A proof of `False`.
@@ -330,6 +337,10 @@ structure State where
   from a α-term `e` to the pair `(toInt e, α)`.
   -/
   toIntTermMap : PHashMap ExprPtr ToIntTermInfo := {}
+  /--
+  `usedCommRing` is `true` if the `CommRing` has been used to normalize expressions.
+  -/
+  usedCommRing : Bool := false
   deriving Inhabited
 
 end Lean.Meta.Grind.Arith.Cutsat
diff --git a/src/Lean/Meta/Tactic/Grind/Main.lean b/src/Lean/Meta/Tactic/Grind/Main.lean
index b40b2a73f5..ec9685c275 100644
--- a/src/Lean/Meta/Tactic/Grind/Main.lean
+++ b/src/Lean/Meta/Tactic/Grind/Main.lean
@@ -75,11 +75,12 @@ def GrindM.run (x : GrindM α) (params : Params) (fallback : Fallback) : MetaM 
   let (btrueExpr, scState)  := shareCommonAlpha (mkConst ``Bool.true) scState
   let (natZExpr, scState)   := shareCommonAlpha (mkNatLit 0) scState
   let (ordEqExpr, scState)  := shareCommonAlpha (mkConst ``Ordering.eq) scState
+  let (intExpr, scState)    := shareCommonAlpha Int.mkType scState
   let simprocs := params.normProcs
   let simpMethods := Simp.mkMethods simprocs discharge? (wellBehavedDischarge := true)
   let simp := params.norm
   let config := params.config
-  x (← mkMethods fallback).toMethodsRef { config, simpMethods, simp, trueExpr, falseExpr, natZExpr, btrueExpr, bfalseExpr, ordEqExpr }
+  x (← mkMethods fallback).toMethodsRef { config, simpMethods, simp, trueExpr, falseExpr, natZExpr, btrueExpr, bfalseExpr, ordEqExpr, intExpr }
     |>.run' { scState }
 
 private def mkCleanState (mvarId : MVarId) (params : Params) : MetaM Clean.State := mvarId.withContext do
diff --git a/src/Lean/Meta/Tactic/Grind/Types.lean b/src/Lean/Meta/Tactic/Grind/Types.lean
index f7ab618d41..d76c1ef871 100644
--- a/src/Lean/Meta/Tactic/Grind/Types.lean
+++ b/src/Lean/Meta/Tactic/Grind/Types.lean
@@ -112,6 +112,7 @@ structure Context where
   btrueExpr    : Expr
   bfalseExpr   : Expr
   ordEqExpr    : Expr -- `Ordering.eq`
+  intExpr      : Expr -- `Int`
 
 /-- Key for the congruence theorem cache. -/
 structure CongrTheoremCacheKey where
@@ -246,6 +247,10 @@ def getNatZeroExpr : GrindM Expr := do
 def getOrderingEqExpr : GrindM Expr := do
   return (← readThe Context).ordEqExpr
 
+/-- Returns the internalized `Int`.  -/
+def getIntExpr : GrindM Expr := do
+  return (← readThe Context).intExpr
+
 def cheapCasesOnly : GrindM Bool :=
   return (← readThe Context).cheapCases
 
diff --git a/tests/lean/grind/algebra/nat.lean b/tests/lean/grind/algebra/nat.lean
deleted file mode 100644
index 7b3f6a84b8..0000000000
--- a/tests/lean/grind/algebra/nat.lean
+++ /dev/null
@@ -1,16 +0,0 @@
-
-open Lean.Grind
-
-variable [CommRing R] [LinearOrder R] [OrderedRing R]
-example (a b : R) (h : 0 ≤ a * b) : 0 ≤ b * a := by grind
-example (a b : R) (h : 7 ≤ a * b) : 7 ≤ b * a := by grind
-
--- These don't work because `cutsat` disables `linarith`.
--- We could use the CommRing normalizer in cutsat to solve these.
-example (a b : Int) (h : 0 ≤ a * b) : 0 ≤ b * a := by grind
-example (a b : Int) (h : 7 ≤ a * b) : 7 ≤ b * a := by grind
-
--- These should work by embedding `Nat` into its Grothendieck completion,
--- and using that the embedding is monotone.
-example (a b : Nat) (h : 0 ≤ a * b) : 0 ≤ b * a := by grind
-example (a b : Nat) (h : 7 ≤ a * b) : 7 ≤ b * a := by grind
diff --git a/tests/lean/run/grind_canon_insts.lean b/tests/lean/run/grind_canon_insts.lean
index 602c1e791e..f5d762b9f4 100644
--- a/tests/lean/run/grind_canon_insts.lean
+++ b/tests/lean/run/grind_canon_insts.lean
@@ -57,25 +57,3 @@ set_option trace.Meta.debug true
 example (a b c d : Nat) : b * (a * c) = d * (b * c) → False := by
   rw [left_comm] -- Introduces a new (non-canonical) instance for `Mul Nat`
   grind on_failure fallback -- State should have only 3 `*`-applications
-
-
-set_option pp.notation false in
-set_option pp.explicit true in
-/--
-trace: [Meta.debug] [@HMul.hMul Int Int Int (@instHMul Int Int.instMul) (@NatCast.natCast Int instNatCastInt b)
-       (@NatCast.natCast Int instNatCastInt a),
-     @HMul.hMul Int Int Int (@instHMul Int Int.instMul) (@NatCast.natCast Int instNatCastInt b)
-       (@NatCast.natCast Int instNatCastInt d),
-     @HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) b a,
-     @HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) b d]
--/
-#guard_msgs (trace) in
-example (a b c d : Nat) : b * a = d * b → False := by
-  rw [CommMonoid.mul_comm d b] -- Introduces a new (non-canonical) instance for `Mul Nat`
-  -- See target here
-  guard_target =ₛ
-    @HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) b a
-    =
-    @HMul.hMul Nat Nat Nat (@instHMul Nat (@Semigroup.toMul Nat (@Monoid.toSemigroup Nat (@CommMonoid.toMonoid Nat instCommMonoidNat)))) b d
-    → False
-  grind on_failure fallback -- State should have only 2 `*`-applications, and they use the same instance
diff --git a/tests/lean/run/grind_cutsat_commring.lean b/tests/lean/run/grind_cutsat_commring.lean
new file mode 100644
index 0000000000..e003c7c7f5
--- /dev/null
+++ b/tests/lean/run/grind_cutsat_commring.lean
@@ -0,0 +1,39 @@
+open Lean.Grind
+
+variable [CommRing R] [LinearOrder R] [OrderedRing R]
+example (a b : R) (h : 0 ≤ a * b) : 0 ≤ b * a := by grind
+example (a b : R) (h : 7 ≤ a * b) : 7 ≤ b * a := by grind
+
+example (a b : Int) (h : 0 ≤ a * b) : 0 ≤ b * a := by grind
+example (a b : Int) (h : 7 ≤ a * b) : 7 ≤ b * a := by grind
+
+example (a b : Nat) (h : 0 ≤ a * b) : 0 ≤ b * a := by grind
+example (a b : Nat) (h : 7 ≤ a * b) : 7 ≤ b * a := by grind
+example (a b : Nat) (h : 7 ≤ a * b + b) : 7 ≤ b + b * a := by grind
+
+example (a b : Int) (h₁ : 2 ∣ a*b) (h₂ : 2 ∣ 2*b*a + 1 - a*b) : False := by grind
+example (a b : Int) (h₁ : 2 ∣ a*b) : 2 ∣ b*a := by grind
+example (a b : Int) (h₁ : 3 ∣ a*b + b + c) (h₂ : 3 ∣ b*a + b + c + 1) : False := by grind
+
+example (a b : Nat) (h₁ : 2 ∣ a*b) (h₂ : 2 ∣ b*a + 1) : False := by grind
+example (a b : Nat) (h₁ : 2 ∣ 2*a*b + b) (h₂ : 2 ∣ b + 2*b*a + 1) : False := by grind
+
+example (a b : Int) (h : a + 1 = a * b) : 2 * b * a - 2 * a ≤ 2 := by grind
+example (a b : Int) (h : a + 1 = b * a) : 2 * a * b - 2 * a ≤ 2 := by grind
+example (a b : Int) (h : a + 1 = 3 * b * a) : 6 * a * b - 2 * a ≤ 2 := by grind
+example (a b c : Int) (h₁ : a + 1 + c = b * a) (h₂ : c + 2*b*a = 0) : 6 * a * b - 2 * a ≤ 2 := by grind
+
+example (a b : Nat) (h : a + a * b = 1) : 2 * b * a + 2 * a ≤ 2 := by grind
+example (a b : Nat) (h : a + b * a = 1) : 2 * a * b + 2 * a ≤ 2 := by grind
+example (a b : Nat) (h : a + 2 * b * a = 10) : 2 * a * b + a ≤ 10 := by grind
+example (a b : Nat) (h : a + 2 * b * a = a^2 + b) : 2 * a * b ≤ b + a*a:= by grind
+
+example (a b : Int) (h : a + 1 = b * a) : 2 * a * b - 2 * a ≤ 2 := by grind
+
+example (a b : Int) (h₁ : a + 1 ≠ a * b) (h₂ : a * b ≤ a + 1) : b * a < a + 1 := by grind
+example (a b : Int) (h₁ : a + 1 ≠ b * a) (h₂ : a * b ≤ a + 1) : b * a < a + 1 := by grind
+example (a b : Int) (h₁ : a + 1 ≠ a * b * a) (h₂ : a * a * b ≤ a + 1) : b * a^2 < a + 1 := by grind
+
+example (a b : Nat) (h₁ : a + 1 ≠ a * b) (h₂ : a * b ≤ a + 1) : b * a < a + 1 := by grind
+example (a b : Nat) (h₁ : a + 1 ≠ b * a) (h₂ : a * b ≤ a + 1) : b * a < a + 1 := by grind
+example (a b : Nat) (h₁ : a + 1 ≠ a * b * a) (h₂ : a * a * b ≤ a + 1) : b * a^2 < a + 1 := by grind
diff --git a/tests/lean/run/grind_cutsat_nat_le.lean b/tests/lean/run/grind_cutsat_nat_le.lean
index 559f580823..2458de0e23 100644
--- a/tests/lean/run/grind_cutsat_nat_le.lean
+++ b/tests/lean/run/grind_cutsat_nat_le.lean
@@ -32,7 +32,8 @@ trace: [grind.cutsat.assert] -1*↑a ≤ 0
 [grind.cutsat.assert] -1*「↑a * ↑b」 ≤ 0
 [grind.cutsat.assert] -1*「1」 + 1 = 0
 [grind.cutsat.assert] -1*↑c ≤ 0
-[grind.cutsat.assert] -1*↑c + 「↑a * ↑b」 + 1 ≤ 0
+[grind.cutsat.assert] -1*「↑a * ↑b + -1 * ↑c + 1」 + 「↑a * ↑b」 + -1*↑c + 1 = 0
+[grind.cutsat.assert] 「↑a * ↑b」 + -1*↑c + 1 ≤ 0
 [grind.cutsat.assert] -1*↑0 = 0
 [grind.cutsat.assert] ↑c = 0
 [grind.cutsat.assert] 0 ≤ 0