diff --git a/src/Lean/Meta/Tactic/Grind/Arith.lean b/src/Lean/Meta/Tactic/Grind/Arith.lean
index fa577c1ef7..ee1c2b36e2 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith.lean
@@ -15,5 +15,6 @@ public import Lean.Meta.Tactic.Grind.Arith.Cutsat
 public import Lean.Meta.Tactic.Grind.Arith.CommRing
 public import Lean.Meta.Tactic.Grind.Arith.Linear
 public import Lean.Meta.Tactic.Grind.Arith.Simproc
+public import Lean.Meta.Tactic.Grind.Arith.VarRename
 
 public section
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing.lean
index 6c9af67fe9..97513a70d1 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing.lean
@@ -19,6 +19,7 @@ public import Lean.Meta.Tactic.Grind.Arith.CommRing.Proof
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.DenoteExpr
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.Inv
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.PP
+public import Lean.Meta.Tactic.Grind.Arith.CommRing.VarRename
 
 public section
 
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Proof.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Proof.lean
index 3fc33f8cfc..03107cdca3 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Proof.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/Proof.lean
@@ -17,7 +17,6 @@ public import Lean.Meta.Tactic.Grind.Arith.CommRing.ToExpr
 public section
 
 namespace Lean.Meta.Grind.Arith.CommRing
-
 /--
 Returns a context of type `RArray α` containing the variables of the given ring.
 `α` is the type of the ring.
@@ -354,33 +353,24 @@ private abbrev caching (c : α) (k : ProofM Expr) : ProofM Expr := do
     modify fun s => { s with cache := s.cache.insert addr h }
     return h
 
+local macro "declare! " decls:ident a:ident : term =>
+  `(do if let some x := (← get).$decls[$a]? then
+         return x
+       let x := mkFVar (← mkFreshFVarId);
+       modify fun s => { s with $decls:ident := (s.$decls).insert $a x };
+       return x)
+
 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
+  declare! polyMap p
 
 def mkExprDecl (e : RingExpr) : 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
+  declare! exprMap e
 
 def mkSExprDecl (e : SemiringExpr) : ProofM Expr := do
-  if let some x := (← get).sexprMap[e]? then
-    return x
-  let x := mkFVar (← mkFreshFVarId)
-  modify fun s => { s with sexprMap := s.sexprMap.insert e x }
-  return x
+  declare! sexprMap e
 
 def mkMonDecl (m : Mon) : ProofM Expr := do
-  if let some x := (← get).monMap[m]? then
-    return x
-  let x := mkFVar (← mkFreshFVarId)
-  modify fun s => { s with monMap := s.monMap.insert m x }
-  return x
+  declare! monMap m
 
 private def mkStepBasicPrefix (declName : Name) : ProofM Expr := do
   let ctx ← getContext
@@ -516,10 +506,10 @@ private abbrev withProofContext (x : ProofM Expr) : RingM Expr := do
 where
   go : ProofM Expr := do
     let h ← x
-    let h ← mkLetOfMap (← get).polyMap h `p (mkConst ``Grind.CommRing.Poly) toExpr
-    let h ← mkLetOfMap (← get).monMap h `m (mkConst ``Grind.CommRing.Mon) toExpr
-    let h ← mkLetOfMap (← get).exprMap h `e (mkConst ``Grind.CommRing.Expr) toExpr
-    let h ← mkLetOfMap (← get).sexprMap h `s (mkConst ``Grind.Ring.OfSemiring.Expr) toExpr
+    let h := mkLetOfMap (← get).polyMap h `p (mkConst ``Grind.CommRing.Poly) toExpr
+    let h := mkLetOfMap (← get).monMap h `m (mkConst ``Grind.CommRing.Mon) toExpr
+    let h := mkLetOfMap (← get).exprMap h `e (mkConst ``Grind.CommRing.Expr) toExpr
+    let h := mkLetOfMap (← get).sexprMap h `s (mkConst ``Grind.Ring.OfSemiring.Expr) toExpr
     let h ← if let some sctx := (← read).sctx? then mkLetFVars #[sctx] h else pure h
     mkLetFVars #[(← getContext)] h
 
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/CommRing/VarRename.lean b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/VarRename.lean
new file mode 100644
index 0000000000..98c8a2850f
--- /dev/null
+++ b/src/Lean/Meta/Tactic/Grind/Arith/CommRing/VarRename.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
+-/
+module
+
+prelude
+public import Init.Grind.Ring.Poly
+public import Lean.Meta.Tactic.Grind.Arith.VarRename
+
+namespace Lean.Grind.CommRing
+open Lean.Meta.Grind.Arith
+
+public def Power.renameVars (pw : Power) (f : VarRename) : Power :=
+  { pw with x := (f pw.x) }
+
+public def Mon.renameVars (m : Mon) (f : VarRename) : Mon :=
+  match m with
+  | .unit => .unit
+  | .mult pw m => .mult (pw.renameVars f) (renameVars m f)
+
+public def Poly.renameVars (p : Poly) (f : VarRename) : Poly :=
+  match p with
+  | .num _ => p
+  | .add k m p => .add k (m.renameVars f) (renameVars p f)
+
+public def Expr.renameVars (e : Expr) (f : VarRename) : Expr :=
+  match e with
+  | .num .. | .natCast .. | .intCast .. => e
+  | .var x => .var (f x)
+  | .neg a => .neg (renameVars a f)
+  | .add a b => .add (renameVars a f) (renameVars b f)
+  | .sub a b => .sub (renameVars a f) (renameVars b f)
+  | .mul a b => .mul (renameVars a f) (renameVars b f)
+  | .pow a k => .pow (renameVars a f) k
+
+public def Power.collectVars (pw : Power) : VarCollector :=
+  collectVar pw.x
+
+public def Mon.collectVars (m : Mon) : VarCollector :=
+  match m with
+  | .unit => id
+  | .mult pw m => pw.collectVars >> m.collectVars
+
+public def Poly.collectVars (p : Poly) : VarCollector :=
+  match p with
+  | .num _ => id
+  | .add _ m p => m.collectVars >> p.collectVars
+
+public def Expr.collectVars (e : Expr) : VarCollector :=
+  match e with
+  | .num .. | .natCast .. | .intCast .. => id
+  | .var x => collectVar x
+  | .neg a | .pow a _ => a.collectVars
+  | .add a b | .sub a b | .mul a b => a.collectVars >> b.collectVars
+
+end Lean.Grind.CommRing
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat.lean
index 79870cc216..5adc3c0205 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat.lean
@@ -21,6 +21,7 @@ public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Model
 public import Lean.Meta.Tactic.Grind.Arith.Cutsat.MBTC
 public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Nat
 public import Lean.Meta.Tactic.Grind.Arith.Cutsat.CommRing
+public import Lean.Meta.Tactic.Grind.Arith.Cutsat.VarRename
 
 public section
 
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean
index 8936faef6e..5c8263e05e 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean
@@ -14,6 +14,9 @@ public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
 public import Lean.Meta.Tactic.Grind.Arith.Cutsat.Nat
 public import Lean.Meta.Tactic.Grind.Arith.Cutsat.CommRing
 public import Lean.Meta.Tactic.Grind.Arith.CommRing.Util
+public import Lean.Meta.Tactic.Grind.Arith.VarRename
+import Lean.Meta.Tactic.Grind.Arith.Cutsat.VarRename
+import Lean.Meta.Tactic.Grind.Arith.CommRing.VarRename
 import Lean.Meta.Tactic.Grind.Arith.CommRing.Proof
 
 public section
@@ -22,12 +25,47 @@ namespace Lean.Meta.Grind.Arith.Cutsat
 
 deriving instance Hashable for Int.Linear.Expr
 
+/--
+State for the cutsat proof construction monad.
+
+The final proof may reference only a small subset of the cutsat variables.
+Thus, we normalize the variables and remove any that are unused from the context.
+The variable order must be preserved, as the cutsat auxiliary theorems assume the polynomials are ordered.
+
+Another complication is that cutsat may reorder variables during the search.
+This is why we maintain two fields: `vars` and `vars'`.
+
+We create auxiliary free variables for variables, polynomials, and expressions.
+Cutsat also uses the ring solver to normalize nonlinear polynomials.
+
+Remark: after normalization variable declarations are expanded. We do not create let-declarations for them
+since they are just a numeral.
+
+Remark: if cutsat did not reorder variables during the search, then the prime variables and declarations
+are not used.
+
+Remark: recall that the `.reorder` proof objects are delimiters for indicating whether regular variables and
+declarations or the prime ones should be used.
+-/
 structure ProofM.State where
-  cache       : Std.HashMap UInt64 Expr := {}
-  polyMap     : Std.HashMap Poly Expr := {}
-  exprMap     : Std.HashMap Int.Linear.Expr Expr := {}
-  ringPolyMap : Std.HashMap CommRing.Poly Expr := {}
-  ringExprMap : Std.HashMap CommRing.RingExpr Expr := {}
+  /-- Cache for visited cutsat proof terms. The key is the pointer address. -/
+  cache         : Std.HashMap UInt64 Expr := {}
+  /-- Map from used variables to (temporary) free variable. -/
+  varDecls      : Std.HashMap Var Expr := {}
+  /-- Map from used polynomials to free variable. -/
+  polyDecls     : Std.HashMap Poly Expr := {}
+  /-- Map from used cutsat expressions to free variable. -/
+  exprDecls     : Std.HashMap Int.Linear.Expr Expr := {}
+  /-- Map from used variables (before reordering) to (temporary) free variable. -/
+  varDecls'     : Std.HashMap Var Expr := {}
+  /-- Map from used polynomials (before reordering) to free variable. -/
+  polyDecls'    : Std.HashMap Poly Expr := {}
+  /-- Map from used cutsat expressions (before reordering) to free variable. -/
+  exprDecls'    : Std.HashMap Int.Linear.Expr Expr := {}
+  /-- Map from used ring polynomials to free variable. -/
+  ringPolyDecls : Std.HashMap CommRing.Poly Expr := {}
+  /-- Map from used ring expressions to free variable. -/
+  ringExprDecls : Std.HashMap CommRing.RingExpr Expr := {}
 
 structure ProofM.Context where
   ctx       : Expr
@@ -44,7 +82,7 @@ structure ProofM.Context where
 abbrev ProofM := ReaderT ProofM.Context (StateRefT ProofM.State GoalM)
 
 /-- Returns a Lean expression representing the variable context used to construct cutsat proofs. -/
-private abbrev getContext : ProofM Expr := do
+private def getContext : ProofM Expr := do
   return (← read).ctx
 
 /--
@@ -54,7 +92,11 @@ We use this combinator to process `.reorder c` justifications.
 private abbrev withUnordered (k : ProofM α) : ProofM α := do
   withReader (fun c => { c with ctx := c.ctx', unordered := true }) k
 
-private abbrev getVarMap : ProofM (PHashMap ExprPtr Var) := do
+/--
+Returns the mapping from expressions to cutsat variables.
+These are variables before the renaming them.
+-/
+private def getVarMap : ProofM (PHashMap ExprPtr Var) := do
   if (← read).unordered then
     return (← get').varMap'
   else
@@ -69,65 +111,94 @@ private abbrev caching (c : α) (k : ProofM Expr) : ProofM Expr := do
     modify fun s => { s with cache := s.cache.insert addr h }
     return h
 
+local macro "declare! " decls:ident a:ident : term =>
+  `(do if let some x := (← get).$decls[$a]? then
+         return x
+       let x := mkFVar (← mkFreshFVarId);
+       modify fun s => { s with $decls:ident := (s.$decls).insert $a x };
+       return x)
+
+private def mkVarDecl (x : Var) : ProofM Expr := do
+  if (← read).unordered then
+    declare! varDecls' x
+  else
+    declare! varDecls x
+
 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
+  if (← read).unordered then
+    declare! polyDecls' p
+  else
+    declare! polyDecls p
 
 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
+  if (← read).unordered then
+    declare! exprDecls' e
+  else
+    declare! exprDecls e
 
 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
+  declare! ringPolyDecls p
 
 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
+  declare! ringExprDecls e
 
-private def toContextExprCore (vars : PArray Expr) (type : Expr) : MetaM Expr :=
+private def toContextExprCore (vars : Array Expr) (type : Expr) : MetaM Expr :=
   if h : 0 < vars.size then
     RArray.toExpr type id (RArray.ofFn (vars[·]) h)
   else
     RArray.toExpr type id (RArray.leaf (mkIntLit 0))
 
-private def toContextExpr : GoalM Expr := do
-  toContextExprCore (← getVars) Int.mkType
+private def mkContext
+    (ctxVar : Expr) (vars : PArray Expr) (varDecls : Std.HashMap Var Expr) (polyDecls : Std.HashMap Poly Expr) (exprDecls : Std.HashMap Int.Linear.Expr Expr)
+    (h : Expr) : GoalM Expr := do
+  let usedVars     := collectMapVars varDecls collectVar >> collectMapVars polyDecls (·.collectVars) >> collectMapVars exprDecls (·.collectVars) <| {}
+  let vars'        := usedVars.toArray
+  let varRename    := mkVarRename vars'
+  let vars         := vars'.map fun x => vars[x]!
+  let varFVars     := vars'.map fun x => varDecls[x]?.getD default
+  let varIdsAsExpr := List.range vars'.size |>.toArray |>.map toExpr
+  let h := h.replaceFVars varFVars varIdsAsExpr
+  let h := mkLetOfMap exprDecls h `e (mkConst ``Int.Linear.Expr) fun e => toExpr <| e.renameVars varRename
+  let h := mkLetOfMap polyDecls h `p (mkConst ``Int.Linear.Poly) fun p => toExpr <| p.renameVars varRename
+  let h := h.abstract #[ctxVar]
+  if h.hasLooseBVars then
+    let ctxType := mkApp (mkConst ``RArray [levelZero]) Int.mkType
+    let ctxVal ← toContextExprCore vars Int.mkType
+    return .letE `ctx ctxType ctxVal h (nondep := false)
+  else
+    return h
 
-private def toContextExpr' : GoalM Expr := do
-  toContextExprCore (← get').vars' Int.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 def mkRingContext (h : Expr) : ProofM Expr := do
+  unless (← get').usedCommRing do return h
+  let some ringId ← getIntRingId? | return h
+  let vars ← CommRing.RingM.run ringId do return (← CommRing.getRing).vars
+  let usedVars     := collectMapVars (← get).ringPolyDecls (·.collectVars) >> collectMapVars (← get).ringExprDecls (·.collectVars) <| {}
+  let vars'        := usedVars.toArray
+  let varRename    := mkVarRename vars'
+  let vars         := vars'.map fun x => vars[x]!
+  let h := mkLetOfMap (← get).ringExprDecls h `re (mkConst ``Grind.CommRing.Expr) fun e => toExpr <| e.renameVars varRename
+  let h := mkLetOfMap (← get).ringPolyDecls h `rp (mkConst ``Grind.CommRing.Poly) fun p => toExpr <| p.renameVars varRename
+  let h := h.abstract #[(← read).ringCtx]
+  if h.hasLooseBVars then
+    let ctxType := mkApp (mkConst ``RArray [levelZero]) Int.mkType
+    let ctxVal ← toContextExprCore vars Int.mkType
+    return .letE `rctx ctxType ctxVal h (nondep := false)
+  else
+    return h
 
 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
-    go { ctx, ctx', ringCtx } |>.run' {}
+  let ctx := mkFVar (← mkFreshFVarId)
+  let ctx' := mkFVar (← mkFreshFVarId)
+  let ringCtx := mkFVar (← mkFreshFVarId)
+  go { ctx, ctx', ringCtx } |>.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).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 ] h
+    let h ← mkRingContext h
+    let h ← mkContext (← read).ctx' (← get').vars' (← get).varDecls' (← get).polyDecls' (← get).exprDecls' h
+    let h ← mkContext (← read).ctx (← get').vars (← get).varDecls (← get).polyDecls (← get).exprDecls h
+    trace[Meta.debug] "{h}"
+    return h
 
 /--
 Returns a Lean expression representing the auxiliary `CommRing` variable context needed for normalizing
@@ -155,9 +226,9 @@ partial def EqCnstr.toExprProof (c' : EqCnstr) : ProofM Expr := caching c' do
     return mkApp6 (mkConst ``Int.Linear.eq_norm_expr) (← getContext) (← mkExprDecl lhs) (← mkExprDecl rhs) (← mkPolyDecl c'.p) eagerReflBoolTrue h
   | .defn e p =>
     let some x := (← getVarMap).find? { expr := e } | throwError "`grind` internal error, missing cutsat variable{indentExpr e}"
-    return mkApp6 (mkConst ``Int.Linear.eq_def) (← getContext) (toExpr x) (← mkPolyDecl p) (← mkPolyDecl c'.p) eagerReflBoolTrue (← mkEqRefl e)
+    return mkApp6 (mkConst ``Int.Linear.eq_def) (← getContext) (← mkVarDecl x) (← mkPolyDecl p) (← mkPolyDecl c'.p) eagerReflBoolTrue (← mkEqRefl e)
   | .defnNat h x e =>
-    return mkApp6 (mkConst ``Int.Linear.eq_def') (← getContext) (toExpr x) (← mkExprDecl e) (← mkPolyDecl c'.p) eagerReflBoolTrue h
+    return mkApp6 (mkConst ``Int.Linear.eq_def') (← getContext) (← mkVarDecl x) (← mkExprDecl e) (← mkPolyDecl c'.p) eagerReflBoolTrue h
   | .norm c =>
     return mkApp5 (mkConst ``Int.Linear.eq_norm) (← getContext) (← mkPolyDecl c.p) (← mkPolyDecl c'.p) eagerReflBoolTrue (← c.toExprProof)
   | .divCoeffs c =>
@@ -181,11 +252,11 @@ partial def EqCnstr.toExprProof (c' : EqCnstr) : ProofM Expr := caching c' do
     let h := mkApp4 (mkConst ``Grind.CommRing.norm_int) (← getRingContext) (← mkRingExprDecl re) (← mkRingPolyDecl rp) eagerReflBoolTrue
     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)
+      (← mkVarDecl x) (← mkPolyDecl p) (← mkPolyDecl p') (← mkPolyDecl c'.p)
       eagerReflBoolTrue (← mkEqRefl e) h
   | .defnNatCommRing h₁ x e' p re rp p' =>
     let h₂ := mkApp4 (mkConst ``Grind.CommRing.norm_int) (← getRingContext) (← mkRingExprDecl re) (← mkRingPolyDecl rp) eagerReflBoolTrue
-    return mkApp9 (mkConst ``Int.Linear.eq_def'_norm) (← getContext) (toExpr x) (← mkExprDecl e')
+    return mkApp9 (mkConst ``Int.Linear.eq_def'_norm) (← getContext) (← mkVarDecl x) (← mkExprDecl e')
       (← mkPolyDecl p) (← mkPolyDecl p') (← mkPolyDecl c'.p) eagerReflBoolTrue h₁ h₂
 
 partial def DvdCnstr.toExprProof (c' : DvdCnstr) : ProofM Expr := caching c' do
@@ -218,11 +289,11 @@ partial def DvdCnstr.toExprProof (c' : DvdCnstr) : ProofM Expr := caching c' do
       eagerReflBoolTrue (← c₁.toExprProof) (← c₂.toExprProof)
   | .ofEq x c =>
     return mkApp7 (mkConst ``Int.Linear.dvd_of_eq)
-      (← getContext) (toExpr x) (← mkPolyDecl c.p) (toExpr c'.d) (← mkPolyDecl c'.p)
+      (← getContext) (← mkVarDecl x) (← mkPolyDecl c.p) (toExpr c'.d) (← mkPolyDecl c'.p)
       eagerReflBoolTrue (← c.toExprProof)
   | .subst x c₁ c₂ =>
     return mkApp10 (mkConst ``Int.Linear.eq_dvd_subst)
-      (← getContext) (toExpr x) (← mkPolyDecl c₁.p) (toExpr c₂.d) (← mkPolyDecl c₂.p) (toExpr c'.d) (← mkPolyDecl c'.p)
+      (← getContext) (← mkVarDecl x) (← mkPolyDecl c₁.p) (toExpr c₂.d) (← mkPolyDecl c₂.p) (toExpr c'.d) (← mkPolyDecl c'.p)
       eagerReflBoolTrue (← c₁.toExprProof) (← c₂.toExprProof)
   | .cooper₁ s =>
     let { c₁, c₂, c₃?, left } := s.pred
@@ -291,7 +362,7 @@ partial def LeCnstr.toExprProof (c' : LeCnstr) : ProofM Expr := caching c' do
     else
       mkConst ``Int.Linear.eq_le_subst_nonpos
     return mkApp8 thm
-        (← getContext) (toExpr x) (← mkPolyDecl c₁.p) (← mkPolyDecl c₂.p) (← mkPolyDecl c'.p)
+        (← getContext) (← mkVarDecl x) (← mkPolyDecl c₁.p) (← mkPolyDecl c₂.p) (← mkPolyDecl c'.p)
         eagerReflBoolTrue
         (← c₁.toExprProof) (← c₂.toExprProof)
   | .ofLeDiseq c₁ c₂ =>
@@ -350,7 +421,7 @@ partial def DiseqCnstr.toExprProof (c' : DiseqCnstr) : ProofM Expr := caching c'
     return mkApp5 (mkConst ``Int.Linear.diseq_neg) (← getContext) (← mkPolyDecl c.p) (← mkPolyDecl c'.p) eagerReflBoolTrue (← c.toExprProof)
   | .subst x c₁ c₂  =>
     return mkApp8 (mkConst ``Int.Linear.eq_diseq_subst)
-      (← getContext) (toExpr x) (← mkPolyDecl c₁.p) (← mkPolyDecl c₂.p) (← mkPolyDecl c'.p)
+      (← getContext) (← mkVarDecl x) (← mkPolyDecl c₁.p) (← mkPolyDecl c₂.p) (← mkPolyDecl c'.p)
       eagerReflBoolTrue (← c₁.toExprProof) (← c₂.toExprProof)
   | .reorder c => withUnordered <| c.toExprProof
   | .commRingNorm c e p =>
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/VarRename.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/VarRename.lean
new file mode 100644
index 0000000000..f65b4018b3
--- /dev/null
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/VarRename.lean
@@ -0,0 +1,42 @@
+/-
+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
+-/
+module
+
+prelude
+public import Init.Data.Int.Linear
+public import Lean.Meta.Tactic.Grind.Arith.VarRename
+
+namespace Int.Linear
+open Lean.Meta.Grind.Arith
+
+public def Poly.renameVars (p : Poly) (f : VarRename) : Poly :=
+  match p with
+  | .num .. => p
+  | .add k x p => .add k (f x) (renameVars p f)
+
+public def Expr.renameVars (e : Expr) (f : VarRename) : Expr :=
+  match e with
+  | .num .. => e
+  | .var x => .var (f x)
+  | .neg a => .neg (renameVars a f)
+  | .add a b => .add (renameVars a f) (renameVars b f)
+  | .sub a b => .sub (renameVars a f) (renameVars b f)
+  | .mulL k a => .mulL k (renameVars a f)
+  | .mulR a k => .mulR (renameVars a f) k
+
+public def Poly.collectVars (p : Poly) : VarCollector :=
+  match p with
+  | .num .. => id
+  | .add _ x p => collectVar x >> p.collectVars
+
+public def Expr.collectVars (e : Expr) : VarCollector :=
+  match e with
+  | .num .. => id
+  | .var x => collectVar x
+  | .neg a | .mulL _ a | .mulR a _ => a.collectVars
+  | .add a b | .sub a b => a.collectVars >> b.collectVars
+
+end Int.Linear
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Linear/Proof.lean b/src/Lean/Meta/Tactic/Grind/Arith/Linear/Proof.lean
index 1e4e198844..06ef915623 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/Linear/Proof.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Linear/Proof.lean
@@ -115,10 +115,10 @@ private abbrev withProofContext (x : ProofM Expr) : LinearM Expr := do
 where
   go : ProofM Expr := do
     let h ← x
-    let h ← mkLetOfMap (← get).polyMap h `p (mkConst ``Grind.Linarith.Poly) toExpr
-    let h ← mkLetOfMap (← get).exprMap h `e (mkConst ``Grind.Linarith.Expr) toExpr
-    let h ← mkLetOfMap (← get).ringPolyMap h `rp (mkConst ``Grind.CommRing.Poly) toExpr
-    let h ← mkLetOfMap (← get).ringExprMap h `re (mkConst ``Grind.CommRing.Expr) toExpr
+    let h := mkLetOfMap (← get).polyMap h `p (mkConst ``Grind.Linarith.Poly) toExpr
+    let h := mkLetOfMap (← get).exprMap h `e (mkConst ``Grind.Linarith.Expr) toExpr
+    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), (← getRingContext)] h
 
 /--
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/ProofUtil.lean b/src/Lean/Meta/Tactic/Grind/Arith/ProofUtil.lean
index 1a15f88a19..b07a792038 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/ProofUtil.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/ProofUtil.lean
@@ -13,7 +13,7 @@ public section
 namespace Lean.Meta.Grind.Arith
 
 def mkLetOfMap {_ : Hashable α} {_ : BEq α} (m : Std.HashMap α Expr) (e : Expr)
-    (varPrefix : Name) (varType : Expr) (toExpr : α → Expr) : GoalM Expr := do
+    (varPrefix : Name) (varType : Expr) (toExpr : α → Expr) : Expr := Id.run do
   if m.isEmpty then
     return e
   else
diff --git a/src/Lean/Meta/Tactic/Grind/Arith/VarRename.lean b/src/Lean/Meta/Tactic/Grind/Arith/VarRename.lean
new file mode 100644
index 0000000000..5dbd3d7336
--- /dev/null
+++ b/src/Lean/Meta/Tactic/Grind/Arith/VarRename.lean
@@ -0,0 +1,48 @@
+/-
+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
+-/
+module
+
+prelude
+public import Init.Prelude
+public import Init.Data.Array.QSort
+public import Std.Data.HashSet
+public section
+namespace Lean.Meta.Grind.Arith
+
+abbrev Var : Type := Nat
+abbrev FoundVars := Std.HashSet Nat
+
+abbrev VarCollector := FoundVars → FoundVars
+
+def collectVar (x : Var) : VarCollector := (·.insert x)
+
+instance : AndThen VarCollector where
+  andThen c₁ c₂ := fun s => c₂ () (c₁ s)
+
+def collectMapVars {_ : BEq α} {_ : Hashable α} (m : Std.HashMap α Expr) (k : α → VarCollector) : VarCollector := fun s => Id.run do
+  let mut s := s
+  for (a, _) in m do
+    s := k a s
+  return s
+
+def FoundVars.toArray (s : FoundVars) : Array Var :=
+  Std.HashSet.toArray s |>.qsort
+
+structure VarRename where
+  map : Std.HashMap Var Var
+
+instance : CoeFun VarRename (fun _ => Var → Var) where
+  coe := fun s x => s.map[x]?.getD 0
+
+def mkVarRename (new2old : Array Var) : VarRename := Id.run do
+  let mut old2new : Std.HashMap Var Var := {}
+  let mut new := 0
+  for old in new2old do
+    old2new := old2new.insert old new
+    new := new + 1
+  { map := old2new }
+
+end Lean.Meta.Grind.Arith
diff --git a/tests/lean/run/grind_cutsat_trim_context.lean b/tests/lean/run/grind_cutsat_trim_context.lean
new file mode 100644
index 0000000000..f10972fbb1
--- /dev/null
+++ b/tests/lean/run/grind_cutsat_trim_context.lean
@@ -0,0 +1,14 @@
+/--
+trace: [grind.debug.proof] fun h h_1 h_2 h_3 h_4 h_5 h_6 h_7 h_8 =>
+      let ctx := RArray.leaf (f 2);
+      let p_1 := Poly.add 1 0 (Poly.num 0);
+      let p_2 := Poly.add (-1) 0 (Poly.num 1);
+      let p_3 := Poly.num 1;
+      le_unsat ctx p_3 (eagerReduce (Eq.refl true)) (le_combine ctx p_2 p_1 p_3 (eagerReduce (Eq.refl true)) h_8 h_1)
+-/
+#guard_msgs in -- `cutsat` context should contain only `f 2`
+open Lean Int Linear in
+set_option trace.grind.debug.proof true in
+example (f : Nat → Int) :
+    f 1 <= 0 → f 2 <= 0 → f 3 <= 0 → f 4 <= 0 → f 5 <= 0 → f 6 <= 0 → f 7 <= 0 → f 8 <= 0 → -1 * f 2 + 1 <= 0 → False := by
+  grind