update

Author: iehality

Incompleteness/Arith/FormalizedArithmetic.lean

@@ -250,7 +250,7 @@ noncomputable def nltNumeral (t : ⌜ℒₒᵣ⌝.Term) (n : V) : T ⊢ t ≮' 
 def ltComplete {n m : V} (h : n < m) : T ⊢ ↑n <' ↑m := by
   have : T ⊢ ↑n <' ↑m ⭤ _ := ltNumeral T n m
   apply andRight this ⨀ ?_
-  apply disj (i := m - (n + 1)) _ (by simpa using sub_succ_lt_self (by simp [h]))
+  apply disj (i := m - (n + 1)) _ (by simpa using sub_succ_lt_self h)
   simpa [nth_tSubstItr', h] using eqRefl T ↑n
 
 lemma lt_complete! {n m : V} (h : n < m) : T ⊢! ↑n <' ↑m := ⟨ltComplete T h⟩

Incompleteness/Arith/Second.lean

@@ -18,7 +18,7 @@ lemma substNumeral_app_quote (σ : Semisentence ℒₒᵣ 1) (n : ℕ) :
     substNumeral ⌜σ⌝ (n : V) = ⌜(σ/[‘↑n’] : Sentence ℒₒᵣ)⌝ := by
   dsimp [substNumeral]
   let w : Fin 1 → Semiterm ℒₒᵣ Empty 0 := ![‘↑n’]
-  have : ?[numeral (n : V)] = (⌜fun i : Fin 1 ↦ ⌜w i⌝⌝ : V) := nth_ext' 1 (by simp) (by simp) (by simp)
+  have : ?[numeral (n : V)] = (⌜fun i : Fin 1 ↦ ⌜w i⌝⌝ : V) := nth_ext' 1 (by simp) (by simp) (by simp [w])
   rw [Language.substs₁, this, quote_substs' (L := ℒₒᵣ)]
 
 lemma substNumeral_app_quote_quote (σ π : Semisentence ℒₒᵣ 1) :
@@ -108,7 +108,7 @@ theorem diagonal (θ : Semisentence ℒₒᵣ 1) :
     let Θ : V → Prop := fun x ↦ Semiformula.Evalbm V ![x] θ
     calc
       V ⊧/![] (fixpoint θ)
-      ↔ Θ (substNumeral ⌜diag θ⌝ ⌜diag θ⌝) := by simp [fixpoint_eq]
+      ↔ Θ (substNumeral ⌜diag θ⌝ ⌜diag θ⌝) := by simp [Θ, fixpoint_eq]
     _ ↔ Θ ⌜fixpoint θ⌝                     := by simp [substNumeral_app_quote_quote]; rfl
 
 end Diagonalization
@@ -133,7 +133,7 @@ theorem multidiagonal (θ : Fin k → Semisentence ℒₒᵣ k) :
     have ht : ∀ i, substNumerals (t i) t = ⌜multifixpoint θ i⌝ := by
       intro i; simp [t, multifixpoint, substNumerals_app_quote_quote]
     calc
-      V ⊧/![] (multifixpoint θ i) ↔ V ⊧/t (multidiag (θ i))                 := by simp [multifixpoint]
+      V ⊧/![] (multifixpoint θ i) ↔ V ⊧/t (multidiag (θ i))                 := by simp [t, multifixpoint]
       _                      ↔ V ⊧/(fun i ↦ substNumerals (t i) t) (θ i) := by simp [multidiag, ← funext_iff]
       _                      ↔ V ⊧/(fun i ↦ ⌜multifixpoint θ i⌝) (θ i) := by simp [ht]
 

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "FormalizedFormalLogic",
-   "rev": "f820bd432d95be117b857b9a00823b1de395fd88",
+   "rev": "d3e3fb955304f6f5c97abfac96f0e30e18b74f05",
    "name": "arithmetization",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -15,7 +15,7 @@
    "type": "git",
    "subDir": null,
    "scope": "FormalizedFormalLogic",
-   "rev": "0325e10aefcc4025554b4c188d268cd3d830ba21",
+   "rev": "54324e6e009f0d0a288897312d3feb1c0165ad19",
    "name": "foundation",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "e423a1f0105a779265101af2bd177f5d8065c594",
+   "rev": "8fac96b567d5b979e6a55c99158a99b20e968a96",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -35,10 +35,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "8e5cb8d424df462f84997dd68af6f40e347c3e35",
+   "rev": "1622a8693b31523c8f82db48e01b14c74bc1f155",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0-rc1",
+   "inputRev": "v4.16.0-rc1",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/LeanSearchClient",
@@ -55,47 +55,47 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "ed3b856bd8893ade75cafe13e8544d4c2660f377",
+   "rev": "f72319c9686788305a8ab059f3c4d8c724785c83",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0-rc1",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2b000e02d50394af68cfb4770a291113d94801b5",
+   "rev": "07f60e90998dfd6592688a14cd67bd4e384b77b2",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.48",
+   "inputRev": "v0.0.50",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a4a08d92be3de00def5298059bf707c72dfd3c66",
+   "rev": "79402ad9ab4be9a2286701a9880697e2351e4955",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "v4.16.0-rc1",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "ad942fdf0b15c38bface6acbb01d63855a2519ac",
+   "rev": "f0c584bcb14c5adfb53079781eeea75b26ebbd32",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.14.0",
+   "inputRev": "v4.15.0",
    "inherited": true,
-   "configFile": "lakefile.lean"},
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "f007bfe46ea8fb801ec907df9ab540054abcc5fd",
+   "rev": "5b23a1297aba9683f231c4b1a7ab4076af4ad53d",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.15.0-rc1
+leanprover/lean4:v4.16.0-rc2