chore: move to v4.16.0-rc2

Algorithm/Data/Classes/Dict.lean

@@ -40,11 +40,11 @@ instance [Dict C ι α] : AssocArray (Dict.AssocArray C) ι (Option α) none whe
   getElem a i _ := (Dict.toAssocArray.symm a)[i]?
   toDFinsupp' a := .mk' ((Dict.toAssocArray.symm a)[·]?)
     (.mk ⟨toMultiset (Dict.toAssocArray.symm a), fun i ↦ by
-      simpa [mem_toMultiset, or_iff_not_imp_left] using getElem?_neg _ _ ⟩)
+      simp [mem_toMultiset, or_iff_not_imp_left] ⟩)
   coe_toDFinsupp'_eq_getElem := by simp
   setElem c i x := Dict.toAssocArray <| alterElem (Dict.toAssocArray.symm c) i (fun _ ↦ x)
   getElem_setElem_self := by simp
   getElem_setElem_of_ne _ _ _ _ hij := by simp [hij]
-  getElem_default _ := by simpa [default] using getElem?_neg _ _ (not_mem_empty _)
+  getElem_default _ := by simpa [default] using getElem?_neg (cont := C) _ _ (not_mem_empty _)
 
 end Dict

Algorithm/Data/Classes/ToList.lean

@@ -62,7 +62,7 @@ lemma get?_toList : a.toList.get? = a.get? := by
   rw [get?_eq_get?_toList]
 
 lemma getLast?_toList : a.toList.getLast? = a.back? := by
-  rw [back?, getElem?_eq_getElem?_toList, List.getLast?_eq_getElem?]
+  rw [back?, ← getElem?_toList, List.getLast?_eq_getElem?]
 
 lemma dropLast_toList : a.toList.dropLast = a.pop.toList := by
   simp
@@ -276,7 +276,8 @@ instance : Front (Array α) α where
   frontD c := c.getD 0
   front c h := c.get 0 (by simp_rw [isEmpty_iff_size_eq_zero, size] at h; omega)
   frontD_def := by simp
-  front_mem _ := by simp [Array.get?, size, ← ne_eq, ← List.length_pos_iff_ne_nil]
+  front_mem _ := by
+    simp [Array.get?, size, ← ne_eq, ← Array.toList_eq_nil_iff, ← List.length_pos_iff_ne_nil]
 
 instance : Back (Array α) α where
   back? := Array.back?

Algorithm/Data/PairingHeap.lean

@@ -132,7 +132,7 @@ lemma Heap.le_of_wf [r : IsRefl α (le · ·)] [t : IsTrans α (le · ·)] [Tota
 @[simp]
 lemma Heap.coe_toListUnordered_combine (x : Heap α) :
     ((x.combine le).toListUnordered : Multiset α) = x.toListUnordered := by
-  induction x using Heap.combine.induct le with
+  induction x using Heap.combine.induct with
   | case1 a₁ c₁ a₂ c₂ s ih =>
     match hc : combine le s, noSibling_combine le s with
     | .nil, _ =>

lake-manifest.json

@@ -5,20 +5,20 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "0291556f04e89d46cd2999f0f4c1164c81778207",
+   "rev": "8c60540fe18528a8a857d4d88094b005af61d97b",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0",
+   "inputRev": "v4.16.0-rc2",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/mathlib4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "9837ca9d65d9de6fad1ef4381750ca688774e608",
+   "rev": "15f16b1ec50f425147926be1aede7b4baa725380",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0",
+   "inputRev": "v4.16.0-rc2",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/mhuisi/lean4-cli",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "470c41643209208d325a5a7315116f293c7443fb",
+   "rev": "b64b8eab8cfcf24c398e84b11c77b6555b61095a",
    "name": "UnicodeBasic",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "46376bc3c8f46ac1a1fd7712856b0f7bd6166098",
+   "rev": "9e99cb8cd9ba6906472634e6973c7e27482a70bb",
    "name": "BibtexQuery",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "f8ed91f3a9d806648ae6a03ab98c8b87e8bedc7e",
+   "rev": "26b1d510d9b5238d36b521d5367c707146fecd9d",
    "name": "MD4Lean",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,10 +65,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2c57364ef83406ea86d0f78ce3e342079a2fece5",
+   "rev": "1622a8693b31523c8f82db48e01b14c74bc1f155",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0",
+   "inputRev": "v4.16.0-rc1",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/LeanSearchClient",
@@ -85,30 +85,30 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "9a0b533c2fbd6195df067630be18e11e4349051c",
+   "rev": "f72319c9686788305a8ab059f3c4d8c724785c83",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0",
+   "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": "2689851f387bb2cef351e6825fe94a56a304ca13",
+   "rev": "79402ad9ab4be9a2286701a9880697e2351e4955",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0",
+   "inputRev": "v4.16.0-rc1",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/quote4",
@@ -125,10 +125,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "e8dc5fc16c625fc4fe08f42d625523275ddbbb4b",
+   "rev": "c104265c34eb8181af14e8dbc14c2f034292cb02",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "algorithm",

lakefile.lean

@@ -1,6 +1,10 @@
 import Lake
+
 open Lake DSL
 
+require "leanprover-community" / "mathlib" @ git "v4.16.0-rc2"
+require "leanprover" / "doc-gen4" @ git "v4.16.0-rc2"
+
 abbrev algorithmOnlyLinters : Array LeanOption := #[
   ⟨`linter.hashCommand, true⟩,
   ⟨`linter.oldObtain, true,⟩,
@@ -25,9 +29,6 @@ abbrev algorithmLeanOptions := #[
 
 package algorithm where
 
-require "leanprover-community" / "mathlib" @ git "v4.15.0"
-require "leanprover" / "doc-gen4" @ git "v4.15.0"
-
 lean_lib Mutable where
   roots := #[`Mutable]
   precompileModules := true

lean-toolchain

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