Bump mathlib, get rid of warnings

Signed-off-by: zeramorphic <[email protected]>

ConNF/Model/CountZero.lean

@@ -104,7 +104,7 @@ theorem path_eq_zeroPath (A : ExtendedIndex 0) : A = zeroPath := by
   · rfl
   · change (_ : TypeIndex) < _ at h h'
     cases' β with β
-    · simp only [not_lt_none] at h
+    · cases lt_irrefl _ h
     have := h'.trans_le (le_of_path A)
     cases (Params.Λ_zero_le β).not_lt (coe_lt_coe.mp this)
 
@@ -122,7 +122,8 @@ theorem eq_zero_of_leLevel (β : Λ) [i : LeLevel β] : β = 0 :=
 theorem eq_bot_zero_of_lt (γ β : TypeIndex) [iβ : LeLevel β] [iγ : LeLevel γ] (h : γ < β) :
     γ = ⊥ ∧ β = 0 := by
   cases' β with β
-  · simp only [not_lt_none] at h
+  · change γ < ⊥ at h
+    cases not_lt_bot h
   cases eq_zero_of_leLevel β
   cases' γ with γ
   · exact ⟨rfl, rfl⟩

lake-manifest.json

@@ -5,7 +5,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "dc4a6b1ac3cd502988e283d5c9c5fdf261125a07",
+   "rev": "c0efc1fd2a0bec51bd55c5b17348af13d7419239",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "26b4e42e8e9c45c3ded44a4d161161bef430d446",
+   "rev": "622d52c803db99ff4ea4fb442c1db9e91aed944c",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "d366a602cc4a325a6f9db3a3991dfa6d6cf409c5",
+   "rev": "68b518c9b352fbee16e6d632adcb7a6d0760e2b7",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "56d9d0abdd71d592042b5769f5401030eb53c475",
+   "rev": "bd8361bbeb9dc7de717cede1d6f3dd6eefe9722c",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
    "inputRev": null,
@@ -85,17 +85,27 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "c74a052aebee847780e165611099854de050adf7",
+   "rev": "f93115d0209de6db335725dee900d379f40c0317",
    "name": "UnicodeBasic",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.lean"},
+  {"url": "https://github.com/dupuisf/BibtexQuery",
+   "type": "git",
+   "subDir": null,
+   "scope": "",
+   "rev": "bd8747df9ee72fca365efa5bd3bd0d8dcd083b9f",
+   "name": "BibtexQuery",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "master",
+   "inherited": true,
+   "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/doc-gen4",
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "5cf3352cd6090e58c5ee878c786af8b87e8bdd65",
+   "rev": "b941c425f6f0f1dc45fe13b850ffa7db1bb20d04",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lean-toolchain

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