chore: bump toolchain to v4.26.0

.github/workflows/docs.yml

@@ -26,8 +26,8 @@ jobs:
         run: |
           lake exe graph ./docbuild/algorithm.html
           cd docbuild
+          MATHLIB_NO_CACHE_ON_UPDATE=1 lake update doc-gen4
           lake build Algorithm:docs
-          lake build Algorithm:docsHeader
       - name: Setup Pages
         uses: actions/configure-pages@v4
       - name: Upload artifact

Algorithm/Data/Classes/MultiBag.lean

@@ -29,12 +29,10 @@ attribute [simp] count_eq_count_toMultiset toMultiset_insert
 section MultiBag.ReadOnly
 variable {C α : Type*} [MultiBag.ReadOnly C α] (c : C)
 
-variable [DecidableEq α]
+theorem count_eq_zero {a : α} {c : C} : count a c = 0 ↔ a ∉ c := by
+  classical exact count_eq_count_toMultiset a c ▸ count_toMultiset_eq_zero
 
-theorem count_eq_zero {a : α} {c : C} : count a c = 0 ↔ a ∉ c :=
-  count_eq_count_toMultiset a c ▸ count_toMultiset_eq_zero
-
-theorem count_ne_zero {a : α} {c : C} : count a c ≠ 0 ↔ a ∈ c :=
-  count_eq_count_toMultiset a c ▸ count_toMultiset_ne_zero
+theorem count_ne_zero {a : α} {c : C} : count a c ≠ 0 ↔ a ∈ c := by
+  classical exact count_eq_count_toMultiset a c ▸ count_toMultiset_ne_zero
 
 end MultiBag.ReadOnly

Algorithm/Data/DFinsupp'/Defs.lean

@@ -542,7 +542,8 @@ instance decidableDefault : DecidablePred (Eq (default : Π₀' i, [β i, d i]))
 
 theorem support_subset_iff {s : Set ι} {f : Π₀' i, [β i, d i]} :
     ↑f.support ⊆ s ↔ ∀ i ∉ s, f i = d i := by
-  simp [Set.subset_def]; exact forall_congr' fun i => not_imp_comm
+  simp? [Set.subset_def] says simp only [Set.subset_def, SetLike.mem_coe, mem_support_toFun, ne_eq]
+  exact forall_congr' fun i => not_imp_comm
 
 theorem support_single_ne {i : ι} {b : β i} (hb : b ≠ d i) :
     (single d i b).support = {i} := by

Algorithm/Data/UnionFind.lean

@@ -172,13 +172,15 @@ lemma find_snd_root (self : UnionFind ι P S) (i : ι) :
     (self.find i).snd.root = self.root :=
   rootCore_findAux_snd self.parent self.wf i _
 
+omit [DecidableEq ι] in
 lemma wellFounded_assocArraySet (parent : P) (wf : WellFounded fun j k : ι ↦ j ≠ k ∧ j = parent[k])
     (i r : ι) (hr : parent[r] = r) :
     WellFounded fun j k : ι ↦ j ≠ k ∧ j = parent[i ↦ r][k] := by
   refine ⟨fun x ↦ ?_⟩
   induction x using wf.induction with
   | h x ih =>
     refine ⟨x, fun p ⟨hpx, h⟩ ↦ ?_⟩
+    classical
     simp only [all_valid, getElem_setElem] at h
     split_ifs at h with hx
     · subst hx h
@@ -226,7 +228,6 @@ lemma setParent_root (parent : P) (size : S) (wf : WellFounded fun i j : ι ↦
     unfold rootCore
     dsimp
     split_ifs <;> aesop
-
 termination_by wf.wrap k
 decreasing_by simp_wf; tauto
 
@@ -470,7 +471,7 @@ def union (self : UnionFind ι P S) (i j : ι) : UnionFind ι P S :=
   MutableQuotient.map self (fun x ↦ x.union i j) fun _ _ h ↦ by
     simp only [UnionFindImpl.UnionFindWF.union_root]
     congr! 1
-    simp [h] -- `simp only [h]` made no progress
+    generalize_proofs h₁ h₂ h₃ h₄; revert h₁ h₂ h₃ h₄; rw [h]; intros
     rw [UnionFindImpl.UnionFindWF.size_eq_of_root_eq (h := h)]
     rw [UnionFindImpl.UnionFindWF.size_eq_of_root_eq (h := h)]
 

Algorithm/Graph/Dijkstra.lean

@@ -6,11 +6,12 @@ Authors: Yuyang Zhao
 import Algorithm.Data.Classes.ToList
 import Algorithm.Data.Classes.IndexedMinHeap
 import Algorithm.Data.Graph.AdjList
+import Mathlib.Algebra.Order.Monoid.Canonical.Defs
 import Mathlib.Algebra.Order.Monoid.WithTop
 import Mathlib.Data.Finset.Card
 import Mathlib.Data.Fintype.Basic
 import Mathlib.Data.Set.Lattice
-import Mathlib.Algebra.Order.Monoid.Canonical.Defs
+import Mathlib.Tactic.Order
 
 section -- should be in mathlb
 variable {γ : Type*}
@@ -415,7 +416,7 @@ lemma dijkstraStep_snd_getElem_eq_top (g : G) (c : Info → CostType)
     (heap : DistHeap) (res : DistArray) (hMinIdx : heap[minIdx heap] ≠ ⊤) (v : V) :
     (dijkstraStep g c heap res hMinIdx).2[v] = ⊤ ↔
       v ≠ minIdx heap ∧ res[v] = ⊤ := by
-  letI : DecidableEq V := by classical infer_instance
+  let +nondep : DecidableEq V := by classical infer_instance
   simp [dijkstraStep_snd_getElem]
   split_ifs with h
   · simpa [h]
@@ -493,7 +494,7 @@ lemma dijkstraStep_fst_getElem (g : G) (c : Info → CostType)
   · rintro ⟨x, hx, rfl, rfl, rfl⟩
     exact ⟨homOfStar x hx, rfl⟩
   · rintro ⟨⟨⟨v, x, hx⟩, ⟨fste, snde⟩⟩, rfl⟩
-    simp at fste snde; subst fste snde
+    simp only [EmbeddingLike.apply_eq_iff_eq] at fste snde; subst fste snde
     exact ⟨x, hx, rfl, rfl⟩
 
 lemma dijkstraStep_fst_getElem_eq_top (g : G) (c : Info → CostType)
@@ -504,8 +505,8 @@ lemma dijkstraStep_fst_getElem_eq_top (g : G) (c : Info → CostType)
     (spec₁ : ∀ v : V, heap[v] = ⊤ ∨ res[v] = ⊤) (v : V) :
     (dijkstraStep g c heap res hMinIdx).1[v] = ⊤ ↔
       (heap[v] = ⊤ ∧ v ∉ g..succSet {minIdx heap}) ∨ v = minIdx heap ∨ res[v] ≠ ⊤ := by
-  letI : DecidableEq V := by classical infer_instance
-  letI : DecidableEq Info := by classical infer_instance
+  let +nondep : DecidableEq V := by classical infer_instance
+  let +nondep : DecidableEq Info := by classical infer_instance
   dsimp
   rw [dijkstraStep_fst_getElem (spec₁ := spec₁)]
   simp? [hMinIdx, - not_or] says
@@ -542,8 +543,8 @@ lemma dijkstraStep_spec (g : G) (c : Info → CostType)
     (h : dijkstraStep.Spec g c init heap res) (hMinIdx : heap[minIdx heap] ≠ ⊤) :
     dijkstraStep.Spec g c init (dijkstraStep g c heap res hMinIdx).1
       (dijkstraStep g c heap res hMinIdx).2 := by
-  letI : DecidableEq V := by classical infer_instance
-  letI : DecidableEq Info := by classical infer_instance
+  let +nondep : DecidableEq V := by classical infer_instance
+  let +nondep : DecidableEq Info := by classical infer_instance
   obtain ⟨h₁, h₂, h₃, h₄⟩ := h
   have rMinIdx : res[minIdx heap] = ⊤ := (h₁ _).resolve_left hMinIdx
   constructor
@@ -655,11 +656,14 @@ lemma dijkstraStep_spec (g : G) (c : Info → CostType)
           exact ⟨v, t, hv, ht, p, e, .nil, rfl⟩
       obtain ⟨v, w, hv, hw, psv, evw, pwt, rfl⟩ := this _ rMinIdx p
       simp only [Quiver.Path.cost_comp, Quiver.Path.cost_cons, WithTop.coe_add, ← add_assoc]
-      apply le_add_right
       obtain ⟨d, hd, (⟨rfl, h₂⟩ | ⟨-, h₂⟩)⟩ := h₂ w hw; · exact (h₂ v hv).elim evw
       replace h₃ := (h₃ v hv).2 s inits psv
-      exact (getElem_minIdx_le heap w).trans <| hd.symm ▸
-        (min_le_right _ _).trans <| (h₂ v hv evw).trans (add_le_add_right h₃ _)
+      calc
+        heap[minIdx heap]
+          ≤ heap[w]                     := getElem_minIdx_le heap w
+        _ ≤ d                           := by order only [hd]
+        _ ≤ res[v] + c (evw : E g).info := h₂ v hv evw
+        _ ≤ _                           := by grw [h₃]; exact self_le_add_right _ _
   · intro v
     -- simp? [dijkstraStep_snd_getElem_eq_top, dijkstraStep_fst_getElem_eq_top (spec₁ := h₁), h₄]
     simp only [ne_eq, h₄, dijkstraStep_snd_support,
@@ -690,7 +694,7 @@ where
     else
       let hr := g..dijkstraStep c heap res hh
       have : Fintype.card {v : V | hr.2[v] = ⊤} < Fintype.card {v : V | res[v] = ⊤} := by
-        letI : DecidableEq V := by classical infer_instance
+        let +nondep : DecidableEq V := by classical infer_instance
         simp only [dijkstraStep_snd_getElem_eq_top, ne_eq, Set.coe_setOf, hr]
         exact Fintype.card_lt_of_injective_of_notMem (fun ⟨v, hv⟩ ↦ ⟨v, hv.2⟩)
           (by intro ⟨v, hv⟩ ⟨w, hw⟩; simp)

docbuild/lakefile.toml

@@ -10,4 +10,4 @@ path = "../"
 [[require]]
 scope = "leanprover"
 name = "doc-gen4"
-rev = "v4.26.0-rc2"
+rev = "v4.26.0"

docbuild/lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:v4.26.0-rc2
+leanprover/lean4:v4.26.0

lake-manifest.json

@@ -5,17 +5,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "d5c9558e75342a10d6321e6a8c798a14f68ae23c",
+   "rev": "2df2f0150c275ad53cb3c90f7c98ec15a56a1a67",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.26.0-rc2",
+   "inputRev": "v4.26.0",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "74835c84b38e4070b8240a063c6417c767e551ae",
+   "rev": "160af9e8e7d4ae448f3c92edcc5b6a8522453f11",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2ed4ba69b6127de8f5c2af83cccacd3c988b06bf",
+   "rev": "3591c3f664ac3719c4c86e4483e21e228707bfa2",
    "name": "LeanSearchClient",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,7 +35,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "6e3bb4bf31f731ab28891fe229eb347ec7d5dad3",
+   "rev": "e9f31324f15ead11048b1443e62c5deaddd055d2",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -45,17 +45,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "2aaad968dd10a168b644b6a5afd4b92496af4710",
+   "rev": "b4fb2aa5290ebf61bc5f80a5375ba642f0a49192",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.82",
+   "inputRev": "v0.0.83",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "9c70abdd9215b76019340fad65138e2e8d21843e",
+   "rev": "2f6d238744c4cb07fdc91240feaf5d4221a27931",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -65,7 +65,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "a31845b5557fd5e47d52b9e2977a1b0eff3c38c3",
+   "rev": "9312503909aa8e8bb392530145cc1677a6298574",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -75,7 +75,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "afe9302d9243cee630b0be95322b38b90342ddbf",
+   "rev": "24241822ef9d3e7f6a3bcc53ad136e12663db8f3",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -85,10 +85,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "7e1ced9e049a4fab2508980ec4877ca9c46dffc9",
+   "rev": "933fce7e893f65969714c60cdb4bd8376786044e",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.26.0-rc2",
+   "inputRev": "v4.26.0",
    "inherited": true,
    "configFile": "lakefile.toml"}],
  "name": "algorithm",