Fix definition dependency & Sort jsonl

.gitignore

@@ -1,3 +1,5 @@
 /build
 /lake-packages/*
-/.lake
+/.lake
+script/missing_informal.log
+script/__pycache__/

formal/Munkers.lean → formal/Munkres.lean

@@ -212,7 +212,7 @@ theorem exercise_23_9 {X Y : Type*}
 sorry
 
 theorem exercise_23_11 {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y]
-  (p : X → Y) (hq : QuotientMap p)
+  (p : X → Y) (hq : IsQuotientMap p)
   (hY : ConnectedSpace Y) (hX : ∀ y : Y, IsConnected (p ⁻¹' {y})) :
   ConnectedSpace X :=
 sorry

formal/Rudin.lean

@@ -76,7 +76,7 @@ theorem exercise_1_18a
   (n : ℕ)
   (h : n > 1)
   (x : EuclideanSpace ℝ (Fin n)) -- R^n
-  : ∃ (y : EuclideanSpace ℝ (Fin n)), y ≠ 0 ∧ (inner x y) = (0 : ℝ) :=
+  : ∃ (y : EuclideanSpace ℝ (Fin n)), y ≠ 0 ∧ (inner ℝ x y) = (0 : ℝ) :=
 sorry
 
 theorem exercise_1_18b

lake-manifest.json

@@ -1,21 +1,21 @@
 {"version": "1.1.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/leanprover-community/mathlib4.git",
+ [{"url": "https://github.com/leanprover-community/mathlib4",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "e04fe9d4ce0705c3e13ba74687cd32c8663792ad",
+   "rev": "c211948581bde9846a99e32d97a03f0d5307c31e",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": null,
+   "inputRev": "v4.20.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "ebfb31672ab0a5b6d00a018ff67d2ec51ed66f3a",
+   "rev": "2ac43674e92a695e96caac19f4002b25434636da",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "8d29bc2c3ebe1f863c2f02df816b4f3dd1b65226",
+   "rev": "6c62474116f525d2814f0157bb468bf3a4f9f120",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c96401869916619b86e2e54dbb8e8488bd6dd19c",
+   "rev": "a11bcb5238149ae5d8a0aa5e2f8eddf8a3a9b27d",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,17 +45,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a602d13aca2913724c7d47b2d7df0353620c4ee8",
+   "rev": "21e6a0522cd2ae6cf88e9da99a1dd010408ab306",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.53",
+   "inputRev": "v0.0.60",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "471ff276892c3451a1d693477107e9c3a0c8ab85",
+   "rev": "ddfca7829bf8aa4083cdf9633935dddbb28b7b2a",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "d892d7a88ad0ccf748fb8e651308ccd13426ba73",
+   "rev": "2865ea099ab1dd8d6fc93381d77a4ac87a85527a",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "242359385321fb424299299300c688f697f7ba5b",
+   "rev": "7a0d63fbf8fd350e891868a06d9927efa545ac1e",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,7 +85,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "dd423cf2b153b5b14cb017ee4beae788565a3925",
+   "rev": "f9e25dcbed001489c53bceeb1f1d50bbaf7451d4",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lakefile.lean

@@ -6,7 +6,7 @@ package «proofNet-lean4» {
 }
 
 require mathlib from git
-  "https://github.com/leanprover-community/mathlib4.git"
+  "https://github.com/leanprover-community/mathlib4.git" @ "v4.20.0"
 
 @[default_target]
 lean_lib «ProofNetLean4» {

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.18.0-rc1
+leanprover/lean4:v4.20.0