From 733fbd5ba9e027c337c2d83324285e8f9ce78631 Mon Sep 17 00:00:00 2001
From: SnO2WMaN <me@sno2wman.net>
Date: Tue, 31 Dec 2024 15:53:31 +0900
Subject: [PATCH 1/2] Update

---
 lake-manifest.json | 30 +++++++++++++++---------------
 lean-toolchain     |  2 +-
 2 files changed, 16 insertions(+), 16 deletions(-)

diff --git a/lake-manifest.json b/lake-manifest.json
index 5685cc4..88c8eaa 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "FormalizedFormalLogic",
-   "rev": "f9bc733f6cb954b99c76c698a3e4d191a8a667d5",
+   "rev": "3d99d24b572f61cb362e8f40f81697343e3562a6",
    "name": "arithmetization",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "FormalizedFormalLogic",
-   "rev": "a1bfd1fa480026f05e476050030c0b2d17983bb0",
+   "rev": "5d7d34c1d42d6ffa1a0c64ebcf2336754bae140b",
    "name": "foundation",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "3ece930d0a4a55679efa52b1a825ac93b2469a06",
+   "rev": "e423a1f0105a779265101af2bd177f5d8065c594",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -35,17 +35,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "42dc02bdbc5d0c2f395718462a76c3d87318f7fa",
+   "rev": "8e5cb8d424df462f84997dd68af6f40e347c3e35",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.15.0-rc1",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/LeanSearchClient",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "d7caecce0d0f003fd5e9cce9a61f1dd6ba83142b",
+   "rev": "003ff459cdd85de551f4dcf95cdfeefe10f20531",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -55,27 +55,27 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "119b022b3ea88ec810a677888528e50f8144a26e",
+   "rev": "ed3b856bd8893ade75cafe13e8544d4c2660f377",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "v4.15.0-rc1",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "1383e72b40dd62a566896a6e348ffe868801b172",
+   "rev": "2b000e02d50394af68cfb4770a291113d94801b5",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.46",
+   "inputRev": "v0.0.48",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "de91b59101763419997026c35a41432ac8691f15",
+   "rev": "a4a08d92be3de00def5298059bf707c72dfd3c66",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -85,17 +85,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "303b23fbcea94ac4f96e590c1cad6618fd4f5f41",
+   "rev": "ad942fdf0b15c38bface6acbb01d63855a2519ac",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "v4.14.0",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "0dc51ac7947ff6aa2c16bcffb64c46c7149d1276",
+   "rev": "f007bfe46ea8fb801ec907df9ab540054abcc5fd",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -105,7 +105,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "726b3c9ad13acca724d4651f14afc4804a7b0e4d",
+   "rev": "0c8ea32a15a4f74143e4e1e107ba2c412adb90fd",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
diff --git a/lean-toolchain b/lean-toolchain
index 57a4710..cf25a98 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.14.0-rc2
+leanprover/lean4:v4.15.0-rc1

From 55863611a463fb25bc02d792e55b0f947e53ccb9 Mon Sep 17 00:00:00 2001
From: SnO2WMaN <me@sno2wman.net>
Date: Tue, 31 Dec 2024 16:17:39 +0900
Subject: [PATCH 2/2] fx

---
 Incompleteness/Arith/First.lean | 16 ++++++++++++++--
 1 file changed, 14 insertions(+), 2 deletions(-)

diff --git a/Incompleteness/Arith/First.lean b/Incompleteness/Arith/First.lean
index 654b686..ef5eaf3 100644
--- a/Incompleteness/Arith/First.lean
+++ b/Incompleteness/Arith/First.lean
@@ -1,5 +1,17 @@
 import Incompleteness.Arith.D1
 
+
+namespace List.Vector
+
+variable {α : Type*}
+
+lemma cons_get {x : α} : (x ::ᵥ List.Vector.nil).get = ![x] := by
+  ext i;
+  simp;
+
+end List.Vector
+
+
 namespace LO.FirstOrder
 
 namespace Arith
@@ -13,8 +25,8 @@ lemma re_iff_sigma1 {P : ℕ → Prop} : RePred P ↔ 𝚺₁-Predicate P := by
       intro v; symm; simp; simpa [←Matrix.constant_eq_singleton'] using codeOfRePred_spec h (x := v 0)⟩
   · rintro ⟨φ, hφ⟩
     have := (sigma1_re id (φ.sigma_prop)).comp
-      (f := fun x : ℕ ↦ x ::ᵥ Mathlib.Vector.nil) (Primrec.to_comp <| Primrec.vector_cons.comp .id (.const _))
-    exact this.of_eq <| by intro x; symm; simpa [Mathlib.Vector.cons_get] using hφ ![x]
+      (f := fun x : ℕ ↦ x ::ᵥ List.Vector.nil) (Primrec.to_comp <| Primrec.vector_cons.comp .id (.const _))
+    exact this.of_eq <| by intro x; symm; simpa [List.Vector.cons_get] using hφ ![x];
 
 variable (T : Theory ℒₒᵣ) [𝐑₀ ≼ T] [Sigma1Sound T] [T.Delta1Definable]