chore: mathlib update to v4.2.0 (#20)

.gitignore

@@ -1,3 +1,4 @@
 /build
 /lake-packages/*
 /.cache
+*.olean

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

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

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»"}

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» {

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2023-07-12
+leanprover/lean4:v4.2.0