diff --git a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean
index 45b1084b6e..cc25c82de9 100644
--- a/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean
+++ b/src/Lean/Meta/Tactic/Grind/Arith/Cutsat/Proof.lean
@@ -65,19 +65,6 @@ def mkNatExprDecl (e : Int.OfNat.Expr) : ProofM Expr := do
   modify fun s => { s with natExprMap := s.natExprMap.insert e x }
   return x
 
-private def mkLetOfMap {_ : Hashable α} {_ : BEq α} (m : Std.HashMap α Expr) (e : Expr)
-    (varPrefix : Name) (varType : Expr) (toExpr : α → Expr) : GoalM Expr := do
-  if m.isEmpty then
-    return e
-  else
-    let as := m.toArray
-    let mut e := e.abstract <| as.map (·.2)
-    let mut i := as.size
-    for (p, _) in as.reverse do
-      e := mkLet (varPrefix.appendIndexAfter i) varType (toExpr p) e
-      i := i - 1
-    return e
-
 private def toContextExprCore (vars : PArray Expr) (type : Expr) : MetaM Expr :=
   if h : 0 < vars.size then
     RArray.toExpr type id (RArray.ofFn (vars[·]) h)