diff --git a/.gitignore b/.gitignore
index 40da894..74b281e 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,3 +1,4 @@
 /build
 /lake-packages/*
 /.cache
+*.olean
\ No newline at end of file
diff --git a/ProvenZk/Ext/Fin.lean b/ProvenZk/Ext/Fin.lean
index 920e8fc..7239d64 100644
--- a/ProvenZk/Ext/Fin.lean
+++ b/ProvenZk/Ext/Fin.lean
@@ -18,7 +18,7 @@ theorem castSucc_def {i : Fin n} :
   Fin.mk (n := Nat.succ n) (i.val) (by cases i; linarith) = i.castSucc := by
   rfl
 
-theorem cast_last {n : Nat} : ↑n = Fin.last n := by
+theorem nat_cast_last {n : Nat} : ↑n = Fin.last n := by
   conv => lhs; whnf
   conv => rhs; whnf
   simp
diff --git a/ProvenZk/Ext/Vector/Basic.lean b/ProvenZk/Ext/Vector/Basic.lean
index 949fe98..3aabd2d 100644
--- a/ProvenZk/Ext/Vector/Basic.lean
+++ b/ProvenZk/Ext/Vector/Basic.lean
@@ -216,13 +216,13 @@ lemma snoc_get_castSucc {vs : Vector α n}: (vs.snoc v).get (Fin.castSucc i) = v
   induction n with
   | zero =>
     cases i using Fin.cases with
-    | H0 => cases vs using Vector.casesOn with | cons hd tl => simp
-    | Hs i => cases i using finZeroElim
+    | zero => cases vs using Vector.casesOn with | cons hd tl => simp
+    | succ i => cases i using finZeroElim
   | succ n ih =>
     cases vs using Vector.casesOn with | cons hd tl =>
     cases i using Fin.cases with
-    | H0 => simp
-    | Hs i => simp [Fin.castSucc_succ_eq_succ_castSucc, ih]
+    | zero => simp
+    | succ i => simp [Fin.castSucc_succ_eq_succ_castSucc, ih]
 
 theorem get_val_getElem {v : Vector α n} {i : Fin n}: v[i.val]'(i.prop) = v.get i := by
   rfl
diff --git a/lake-manifest.json b/lake-manifest.json
index a7b16c2..4b7cb34 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -1,39 +1,52 @@
-{"version": 4,
+{"version": 6,
  "packagesDir": "lake-packages",
  "packages":
  [{"git":
-   {"url": "https://github.com/EdAyers/ProofWidgets4",
-    "subDir?": null,
-    "rev": "c43db94a8f495dad37829e9d7ad65483d68c86b8",
-    "name": "proofwidgets",
-    "inputRev?": "v0.0.11"}},
-  {"git":
-   {"url": "https://github.com/mhuisi/lean4-cli.git",
-    "subDir?": null,
-    "rev": "5a858c32963b6b19be0d477a30a1f4b6c120be7e",
-    "name": "Cli",
-    "inputRev?": "nightly"}},
-  {"git":
    {"url": "https://github.com/leanprover-community/mathlib4.git",
     "subDir?": null,
-    "rev": "26d0eab43f05db777d1cf31abd31d3a57954b2a9",
+    "rev": "753159252c585df6b6aa7c48d2b8828d58388b79",
+    "opts": {},
     "name": "mathlib",
-    "inputRev?": "26d0eab43f05db777d1cf31abd31d3a57954b2a9"}},
+    "inputRev?": "v4.2.0",
+    "inherited": false}},
   {"git":
-   {"url": "https://github.com/gebner/quote4",
+   {"url": "https://github.com/leanprover-community/quote4",
     "subDir?": null,
-    "rev": "c0d9516f44d07feee01c1103c8f2f7c24a822b55",
+    "rev": "a387c0eb611857e2460cf97a8e861c944286e6b2",
+    "opts": {},
     "name": "Qq",
-    "inputRev?": "master"}},
+    "inputRev?": "master",
+    "inherited": true}},
   {"git":
-   {"url": "https://github.com/JLimperg/aesop",
+   {"url": "https://github.com/leanprover/lean4-cli",
     "subDir?": null,
-    "rev": "f04538ab6ad07642368cf11d2702acc0a9b4bcee",
-    "name": "aesop",
-    "inputRev?": "master"}},
+    "rev": "39229f3630d734af7d9cfb5937ddc6b41d3aa6aa",
+    "opts": {},
+    "name": "Cli",
+    "inputRev?": "nightly",
+    "inherited": true}},
+  {"git":
+   {"url": "https://github.com/leanprover-community/ProofWidgets4",
+    "subDir?": null,
+    "rev": "f1a5c7808b001305ba07d8626f45ee054282f589",
+    "opts": {},
+    "name": "proofwidgets",
+    "inputRev?": "v0.0.21",
+    "inherited": true}},
   {"git":
    {"url": "https://github.com/leanprover/std4",
     "subDir?": null,
-    "rev": "dff883c55395438ae2a5c65ad5ddba084b600feb",
+    "rev": "6747f41f28627bed83e6d5891683538211caa2c1",
+    "opts": {},
     "name": "std",
-    "inputRev?": "main"}}]}
+    "inputRev?": "main",
+    "inherited": true}},
+  {"git":
+   {"url": "https://github.com/leanprover-community/aesop",
+    "subDir?": null,
+    "rev": "6749fa4e776919514dae85bfc0ad62a511bc42a7",
+    "opts": {},
+    "name": "aesop",
+    "inputRev?": "master",
+    "inherited": true}}],
+ "name": "«proven-zk»"}
diff --git a/lakefile.lean b/lakefile.lean
index ac7ac19..b641c26 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -6,7 +6,7 @@ package «proven-zk» {
 }
 
 require mathlib from git
-  "https://github.com/leanprover-community/mathlib4.git"@"26d0eab43f05db777d1cf31abd31d3a57954b2a9"
+  "https://github.com/leanprover-community/mathlib4.git"@"v4.2.0"
 
 @[default_target]
 lean_lib «ProvenZk» {
diff --git a/lean-toolchain b/lean-toolchain
index 7e1c30c..2f868c6 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2023-07-12
+leanprover/lean4:v4.2.0