chore: move to v4.15.0

Algorithm/Algebra/BigOperators/DFinsupp'.lean

@@ -6,8 +6,7 @@ Authors: Yuyang Zhao
 -/
 import Algorithm.Data.DFinsupp'.Basic
 import Mathlib.Algebra.BigOperators.GroupWithZero.Action
-import Mathlib.Algebra.BigOperators.GroupWithZero.Finset
-import Mathlib.Algebra.Group.Submonoid.Membership
+import Mathlib.Algebra.Group.Submonoid.BigOperators
 
 /-!
 Modified from `Mathlib.Data.DFinsupp.Basic`

Algorithm/Data/DFinsupp'/Defs.lean

@@ -1,4 +1,3 @@
-
 /-
 Copyright (c) 2024 Yuyang Zhao. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
@@ -251,7 +250,7 @@ variable (d) in
 and all other points to `d i`. -/
 def single (i : ι) (b : β i) : Π₀' i, [β i, d i] :=
   ⟨Function.update d i b, Trunc.mk
-    ⟨{i}, fun j => (Decidable.eq_or_ne j i).imp (by simp) fun h => Function.update_noteq h _ _⟩⟩
+    ⟨{i}, fun j => (Decidable.eq_or_ne j i).imp (by simp) fun h => Function.update_of_ne h _ _⟩⟩
 
 theorem single_eq_functionUpdate {i b} : ⇑(single d i b) = Function.update d i b :=
   rfl
@@ -362,7 +361,7 @@ def update : Π₀' i, [β i, d i] :=
         · simp
         · obtain hj | (hj : f j = d j) := s.prop j
           · exact Or.inl (Multiset.mem_cons_of_mem hj)
-          · exact Or.inr ((Function.update_noteq hi.symm b _).trans hj)⟩⟩
+          · exact Or.inr ((Function.update_of_ne hi.symm b _).trans hj)⟩⟩
 
 @[simp, norm_cast] lemma coe_update : (f.update i b : ∀ i : ι, β i) = Function.update f i b := rfl
 

Algorithm/Graph/Dijkstra.lean

@@ -456,7 +456,7 @@ lemma dijkstraStep_fst_getElem' (g : G) (c : Info → CostType)
   · push_neg at h
     simp? [Function.update_apply, h, Multiset.filterMap_filterMap] says
       simp only [ne_eq, h, not_false_eq_true,
-        Function.update_noteq, Function.update_apply, Multiset.filterMap_filterMap]
+        Function.update_of_ne, Function.update_apply, Multiset.filterMap_filterMap]
     congr!
     split; · rename_i snde; simp [snde, Ne.symm h.1]
     split; · simp

lake-manifest.json

@@ -5,20 +5,20 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "099b90e374ba73983c3fda87595be625f1931669",
+   "rev": "0291556f04e89d46cd2999f0f4c1164c81778207",
    "name": "«doc-gen4»",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0-rc1",
+   "inputRev": "v4.15.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/mathlib4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "41ff1f7899c971f91362710d4444e338b8acd644",
+   "rev": "9837ca9d65d9de6fad1ef4381750ca688774e608",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0-rc1",
+   "inputRev": "v4.15.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/mhuisi/lean4-cli",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "d55279d2ff01759fa75752fcf1a93d1db8db18ff",
+   "rev": "470c41643209208d325a5a7315116f293c7443fb",
    "name": "UnicodeBasic",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,7 +45,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "982700bcf78b93166e5b1af0b4b756b8acfdb54b",
+   "rev": "46376bc3c8f46ac1a1fd7712856b0f7bd6166098",
    "name": "BibtexQuery",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -55,7 +55,7 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "fe8e6e649ac8251f43c6f6f934f095ebebce7e7c",
+   "rev": "f8ed91f3a9d806648ae6a03ab98c8b87e8bedc7e",
    "name": "MD4Lean",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -65,17 +65,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "8e5cb8d424df462f84997dd68af6f40e347c3e35",
+   "rev": "2c57364ef83406ea86d0f78ce3e342079a2fece5",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0-rc1",
+   "inputRev": "v4.15.0",
    "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",
@@ -85,10 +85,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "ed3b856bd8893ade75cafe13e8544d4c2660f377",
+   "rev": "9a0b533c2fbd6195df067630be18e11e4349051c",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0-rc1",
+   "inputRev": "v4.15.0",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
@@ -105,30 +105,30 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "8b6048aa0a4a4b6bcf83597802d8dee734e64b7e",
+   "rev": "2689851f387bb2cef351e6825fe94a56a304ca13",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.15.0-rc1",
+   "inputRev": "v4.15.0",
    "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": "7805acf1864ba1a2e359f86a8f092ccf1438ad83",
+   "rev": "e8dc5fc16c625fc4fe08f42d625523275ddbbb4b",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.14.0",
+   "inputRev": "v4.15.0",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "algorithm",

lakefile.lean

@@ -25,8 +25,8 @@ abbrev algorithmLeanOptions := #[
 
 package algorithm where
 
-require "leanprover-community" / "mathlib" @ git "v4.15.0-rc1"
-require "leanprover" / "doc-gen4" @ git "v4.15.0-rc1"
+require "leanprover-community" / "mathlib" @ git "v4.15.0"
+require "leanprover" / "doc-gen4" @ git "v4.15.0"
 
 lean_lib Mutable where
   roots := #[`Mutable]

lean-toolchain

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