diff --git a/Smt/Data/Sexp.lean b/Smt/Data/Sexp.lean
index e4b67302..b536d9dd 100644
--- a/Smt/Data/Sexp.lean
+++ b/Smt/Data/Sexp.lean
@@ -83,9 +83,9 @@ partial def parseOneAux : List Substring → Except ParseError (Sexp × List Sub
       return (atom tk.toString, tks)
   | [] => throw <| .incomplete "expected a token, got none"
 
-partial def parseManyAux :=
+partial def parseManyAux : List Substring → Except ParseError (Array Sexp × List Substring) :=
   go #[]
-where go (stk : Array Sexp) : List Substring → Except ParseError (Array Sexp × List Substring)
+where go (stk : Array Sexp)
   | tk :: tks => do
     if tk.front == ')' then .ok (stk, tk :: tks)
     else
diff --git a/Smt/Reconstruct/Real/Polynorm.lean b/Smt/Reconstruct/Real/Polynorm.lean
index 53624d9a..1cc389ab 100644
--- a/Smt/Reconstruct/Real/Polynorm.lean
+++ b/Smt/Reconstruct/Real/Polynorm.lean
@@ -6,6 +6,7 @@ Authors: Abdalrhman Mohamed
 -/
 
 import Mathlib.Data.Real.Basic
+import Mathlib.Tactic.Ring.RingNF
 
 namespace Smt.Reconstruct.Real
 
diff --git a/Test/BitVec/Shift.expected b/Test/BitVec/Shift.expected
index 9d781ffb..f7f9bcd5 100644
--- a/Test/BitVec/Shift.expected
+++ b/Test/BitVec/Shift.expected
@@ -9,8 +9,8 @@ Test/BitVec/Shift.lean:5:8: warning: declaration uses 'sorry'
 goal: x ++ y = zeroExtend 6 x <<< 3#2 ||| zeroExtend 6 y
 
 query:
-(declare-const y (_ BitVec 3))
 (declare-const x (_ BitVec 3))
+(declare-const y (_ BitVec 3))
 (assert (distinct (concat x y) (bvor (bvshl ((_ zero_extend 3) x) #b11) ((_ zero_extend 3) y))))
 (check-sat)
 Test/BitVec/Shift.lean:10:8: warning: declaration uses 'sorry'
diff --git a/Test/Int/Binders.expected b/Test/Int/Binders.expected
index 4169c399..83c0b301 100644
--- a/Test/Int/Binders.expected
+++ b/Test/Int/Binders.expected
@@ -1,7 +1,7 @@
 goal: curryAdd a b = curryAdd b a
 
 query:
-(define-fun curryAdd ((a._@.Test.Int.Binders._hyg.3 Int) (a._@.Test.Int.Binders._hyg.5 Int)) Int (+ a._@.Test.Int.Binders._hyg.3 a._@.Test.Int.Binders._hyg.5))
+(define-fun curryAdd ((a._@.Test.Int.Binders._hyg.4 Int) (a._@.Test.Int.Binders._hyg.6 Int)) Int (+ a._@.Test.Int.Binders._hyg.4 a._@.Test.Int.Binders._hyg.6))
 (declare-const b Int)
 (declare-const a Int)
 (assert (distinct (curryAdd a b) (curryAdd b a)))
@@ -10,7 +10,7 @@ Test/Int/Binders.lean:5:0: warning: declaration uses 'sorry'
 goal: partCurryAdd a b = partCurryAdd b a
 
 query:
-(define-fun partCurryAdd ((a Int) (a._@.Test.Int.Binders._hyg.33 Int)) Int (+ a a._@.Test.Int.Binders._hyg.33))
+(define-fun partCurryAdd ((a Int) (a._@.Test.Int.Binders._hyg.36 Int)) Int (+ a a._@.Test.Int.Binders._hyg.36))
 (declare-const b Int)
 (declare-const a Int)
 (assert (distinct (partCurryAdd a b) (partCurryAdd b a)))
@@ -19,7 +19,7 @@ Test/Int/Binders.lean:11:0: warning: declaration uses 'sorry'
 goal: partCurryAdd' a b = partCurryAdd' b a
 
 query:
-(define-fun |partCurryAdd'| ((a Int) (a._@.Init.Prelude._hyg.2347 Int)) Int (+ a a._@.Init.Prelude._hyg.2347))
+(define-fun |partCurryAdd'| ((a Int) (a._@.Init.Prelude._hyg.2495 Int)) Int (+ a a._@.Init.Prelude._hyg.2495))
 (declare-const b Int)
 (declare-const a Int)
 (assert (distinct (+ a b) (+ b a)))
@@ -29,8 +29,8 @@ goal: mismatchNamesAdd a b = mismatchNamesAdd b a
 
 query:
 (define-fun mismatchNamesAdd ((a Int) (b Int)) Int (+ a b))
-(declare-const a Int)
 (declare-const b Int)
+(declare-const a Int)
 (assert (distinct (mismatchNamesAdd a b) (mismatchNamesAdd b a)))
 (check-sat)
 Test/Int/Binders.lean:25:0: warning: declaration uses 'sorry'
diff --git a/Test/Int/Let.expected b/Test/Int/Let.expected
index e945919e..cd2a1eac 100644
--- a/Test/Int/Let.expected
+++ b/Test/Int/Let.expected
@@ -19,7 +19,7 @@ goal: z 3 = 10
 
 query:
 (declare-fun f (Int) Int)
-(define-fun z ((x._@.Test.Int.Let._hyg.295 Int)) Int (f 10))
+(define-fun z ((x._@.Test.Int.Let._hyg.300 Int)) Int (f 10))
 (assert (= (f 10) 10))
 (assert (distinct (z 3) 10))
 (check-sat)
diff --git a/Test/Nat/Cong.expected b/Test/Nat/Cong.expected
index e3c5499f..768e190e 100644
--- a/Test/Nat/Cong.expected
+++ b/Test/Nat/Cong.expected
@@ -3,7 +3,7 @@ goal: x = y → f x = f y
 query:
 (define-sort Nat () Int)
 (declare-fun f (Nat) Nat)
-(assert (forall ((_uniq.1521 Nat)) (=> (>= _uniq.1521 0) (>= (f _uniq.1521) 0))))
+(assert (forall ((_uniq.1520 Nat)) (=> (>= _uniq.1520 0) (>= (f _uniq.1520) 0))))
 (declare-const x Nat)
 (assert (>= x 0))
 (declare-const y Nat)
diff --git a/Test/Nat/Sum'.expected b/Test/Nat/Sum'.expected
index c52d77fa..c934fc3b 100644
--- a/Test/Nat/Sum'.expected
+++ b/Test/Nat/Sum'.expected
@@ -1,6 +1,6 @@
 Test/Nat/Sum'.lean:7:12: error: tactic 'assumption' failed
 case zero.a
-_uniq✝¹¹⁶⁰³⁻⁰ :
+_uniq✝⁹⁹³⁹⁻⁰ :
   ¬((∀ (n : Int), sum n = if n = 0 then 0 else n + sum (if 1 ≤ n then n - 1 else 0)) ∧
       (∀ («_uniq.4976» : Int), «_uniq.4976» ≥ 0 → sum «_uniq.4976» ≥ 0) ∧ Smt.Reconstruct.Builtin.distinct [sum 0, 0])
 ⊢ ¬Smt.Reconstruct.andN' [Nat → Nat] ¬sum 0 = 0 * (0 + 1) / 2
@@ -11,7 +11,7 @@ query:
 (declare-const n Nat)
 (assert (>= n 0))
 (define-fun-rec sum ((n Nat)) Nat (ite (= n 0) 0 (+ n (sum (ite (<= 1 n) (- n 1) 0)))))
-(assert (forall ((_uniq.13678 Nat)) (=> (>= _uniq.13678 0) (>= (sum _uniq.13678) 0))))
+(assert (forall ((_uniq.12014 Nat)) (=> (>= _uniq.12014 0) (>= (sum _uniq.12014) 0))))
 (assert (= (sum n) (div (* n (+ n 1)) 2)))
 (assert (distinct (sum (+ n 1)) (div (* (+ n 1) (+ (+ n 1) 1)) 2)))
 (check-sat)
diff --git a/Test/Real/Density.expected b/Test/Real/Density.expected
index 5b62cbfd..0ec01b0f 100644
--- a/Test/Real/Density.expected
+++ b/Test/Real/Density.expected
@@ -6,3 +6,5 @@ query:
 (assert (not (=> (< x z) (exists ((y Real)) (and (< x y) (< y z))))))
 (check-sat)
 Test/Real/Density.lean:4:8: warning: declaration uses 'sorry'
+Test/Real/Density.lean:5:2: warning: 'smt_show' tactic does nothing
+note: this linter can be disabled with `set_option linter.unusedTactic false`
diff --git a/Test/Real/Inverse.expected b/Test/Real/Inverse.expected
index 3de7d30f..1409551a 100644
--- a/Test/Real/Inverse.expected
+++ b/Test/Real/Inverse.expected
@@ -5,3 +5,5 @@ query:
 (assert (not (=> (distinct x 0.0) (exists ((y Real)) (= (* x y) 1.0)))))
 (check-sat)
 Test/Real/Inverse.lean:4:8: warning: declaration uses 'sorry'
+Test/Real/Inverse.lean:5:2: warning: 'smt_show' tactic does nothing
+note: this linter can be disabled with `set_option linter.unusedTactic false`
diff --git a/Test/linarith.expected b/Test/linarith.expected
index 45481b77..3200e752 100644
--- a/Test/linarith.expected
+++ b/Test/linarith.expected
@@ -15,6 +15,7 @@ Test/linarith.lean:125:9: warning: unused variable `a`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
 Test/linarith.lean:125:13: warning: unused variable `c`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
+Test/linarith.lean:146:2: error: [arithPolyNorm]: could not prove x - y = -x + y
 Test/linarith.lean:168:34: warning: unused variable `z`
 note: this linter can be disabled with `set_option linter.unusedVariables false`
 Test/linarith.lean:169:5: warning: unused variable `h5`
diff --git a/lake-manifest.json b/lake-manifest.json
index 0283d11e..38c71683 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -1,4 +1,4 @@
-{"version": 7,
+{"version": "1.0.0",
  "packagesDir": ".lake/packages",
  "packages":
  [{"url": "https://github.com/abdoo8080/lean-cvc5.git",
@@ -13,7 +13,7 @@
   {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "rev": "551ff2d7dffd7af914cdbd01abbd449fe3e3d428",
+   "rev": "54bb04c3119f24fde14b9068c4b2e69db52a1450",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -22,7 +22,7 @@
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
-   "rev": "53156671405fbbd5402ed17a79bd129b961bd8d6",
+   "rev": "a7bfa63f5dddbcab2d4e0569c4cac74b2585e2c6",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -31,7 +31,7 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "53ba96ad7666d4a2515292974631629b5ea5dfee",
+   "rev": "06cca4bd36b2af743d4858c5cc31604aa9da26bc",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -40,10 +40,10 @@
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
-   "rev": "e6b6247c61280c77ade6bbf0bc3c66a44fe2e0c5",
+   "rev": "87c1e7a427d8e21b6eaf8401f12897f52e2c3be9",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.36",
+   "inputRev": "v0.0.38",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
@@ -58,7 +58,7 @@
   {"url": "https://github.com/leanprover-community/import-graph.git",
    "type": "git",
    "subDir": null,
-   "rev": "77e081815b30b0d30707e1c5b0c6a6761f7a2404",
+   "rev": "c29c3cdce415240e9dcec5c583ad5d36f83f9c71",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -67,10 +67,10 @@
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "type": "git",
    "subDir": null,
-   "rev": "b5eba595428809e96f3ed113bc7ba776c5f801ac",
+   "rev": "f0957a7575317490107578ebaee9efaf8e62a4ab",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.8.0",
+   "inputRev": "v4.9.0",
    "inherited": false,
    "configFile": "lakefile.lean"}],
  "name": "smt",
diff --git a/lakefile.lean b/lakefile.lean
index bd8d2606..5d333342 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -6,7 +6,7 @@ require cvc5 from
   git "https://github.com/abdoo8080/lean-cvc5.git" @ "main"
 
 require mathlib from
-  git "https://github.com/leanprover-community/mathlib4.git" @ "v4.8.0"
+  git "https://github.com/leanprover-community/mathlib4.git" @ "v4.9.0"
 
 def libcpp : String :=
   if System.Platform.isWindows then "libstdc++-6.dll"
diff --git a/lean-toolchain b/lean-toolchain
index ef1f67e9..4ef27c47 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.8.0
+leanprover/lean4:v4.9.0