chore: bump mathlib to 8589236, fix breaking changes (#628)

Bump `mathlib` dependency to
[8589236](leanprover-community/mathlib4@8589236):
chore: move Data/Nat/Lattice to Order (#39990) (2026-06-09)
Previously at:
[d90090f](leanprover-community/mathlib4@d90090f):
chore: bump toolchain to v4.31.0-rc2 (#40358) (2026-06-08)

Closes #627

Failure log from the validation run:
[download](https://github.com/leanprover-community/downstream-reports/actions/runs/27253259444/artifacts/7526847935)
_(link expires after 1 year)_

---

This PR bumps `mathlib` to an identified incompatible (first-known-bad)
commit (`8589236`) so you can reproduce and fix the incompatibility
locally by checking out this branch.

_Opened automatically by
[downstream-reports/track-incompatibility](https://github.com/leanprover-community/downstream-reports)
via [this workflow
run](https://github.com/leanprover/cslib/actions/runs/27305770390)._

---------

Co-authored-by: mathlib-nightly-testing[bot] <mathlib-nightly-testing[bot]@users.noreply.github.com>
Co-authored-by: Chris Henson <chrishenson.net@gmail.com>

Author: mathlib-nightly-testing[bot]

.github/CODEOWNERS

@@ -12,7 +12,7 @@
 ### Area access
 # Each area maintainer has access to parts that pertain them. They get automatically asked for
 # reviewing new PRs that touch those areas.
-/Cslib/Algorithms/ @fmontesi @sorrachai
+/Cslib/Algorithms/ @fmontesi @sorrachai @chenson2018
 /Cslib/Foundations/Logic/ @arademaker @fmontesi @chenson2018
 /Cslib/Logics/ @arademaker @fmontesi @chenson2018
 /Cslib/Languages/LambdaCalculus/ @chenson2018 @fmontesi

.github/workflows/lean_action_ci.yml

@@ -22,10 +22,10 @@ jobs:
         with:
           build-args: "--wfail --iofail"
           test-args: "--wfail --iofail"
-      - name: "lake exe mk_all --check --module"
+      - name: "lake exe mk_all --check"
         run: |
           set -e
-          lake exe mk_all --check --module
+          lake exe mk_all --check
       #- name: "lake shake"
       #  run: |
       #    set -e

CONTRIBUTING.md

@@ -126,7 +126,7 @@ CSLib uses a number of linters, mostly inherited from Batteries and Mathlib. The
 ## Imports
 
 There is a also a test that [Cslib.lean](/Cslib.lean) imports all files. You can ensure this by
-running `lake exe mk_all --module` locally, which will make the required changes.
+running `lake exe mk_all` locally, which will make the required changes.
 
 CSLib tests for minimized imports using `lake shake --add-public --keep-implied --keep-prefix`, which also comes with a `--fix` option.
 See `lake shake --help` for the special comment syntax used to preserve imports required for tactics or typeclasses.

Cslib/Algorithms/Lean/MergeSort/MergeSort.lean

@@ -8,7 +8,7 @@ module
 
 public import Cslib.Algorithms.Lean.TimeM
 public import Mathlib.Data.Nat.Cast.Order.Ring
-public import Mathlib.Data.Nat.Lattice
+public import Mathlib.Order.Lattice.Nat
 public import Mathlib.Data.Nat.Log
 
 /-!

Cslib/Foundations/Combinatorics/InfiniteGraphRamsey.lean

@@ -69,8 +69,8 @@ private lemma goodSelection_exists (ivs : InfVSet Vertex) :
   obtain ⟨v, h_v⟩ := Set.Infinite.nonempty ivs.inf
   let f u := color {v, u}
   obtain ⟨c, vs, h_inf, h_vs, h_col⟩ := infinite_pigeonhole_principle f <|
-    Set.Infinite.diff ivs.inf (finite_singleton v)
-  simp only [subset_diff] at h_vs
+    Set.Infinite.sdiff ivs.inf (finite_singleton v)
+  simp only [subset_sdiff] at h_vs
   let ivs' := InfVSet.mk vs h_inf
   use {vs := ivs', v := v, c := c}
   grind [GoodSelection]

Cslib/Foundations/Data/OmegaSequence/Init.lean

@@ -9,7 +9,7 @@ module
 public import Cslib.Foundations.Data.OmegaSequence.Defs
 public import Mathlib.Algebra.Order.Group.Nat
 public import Mathlib.Algebra.Order.Sub.Basic
-public import Mathlib.Data.Nat.Lattice
+public import Mathlib.Order.Lattice.Nat
 
 /-!
 # ω-sequences a.k.a. infinite sequences

Cslib/MachineLearning/PACLearning/Defs.lean

@@ -517,7 +517,7 @@ theorem error_map_eq_hypothesisError (P : Measure α) (h c : Set α)
   rw [Measure.map_apply_of_aemeasurable hf.aemeasurable]
   · congr 1; ext x
     simp only [Set.mem_preimage, Set.mem_setOf_eq, symmDiff_def, sup_eq_union,
-      Set.mem_union, Set.mem_diff]
+      Set.mem_union, Set.mem_sdiff]
     by_cases hx : x ∈ h <;> by_cases hcx : x ∈ c <;> simp_all
   · convert (hh.prod (measurableSet_singleton false)).union
       (hh.compl.prod (measurableSet_singleton true)) using 1

Cslib/MachineLearning/PACLearning/VCDimension.lean

@@ -59,12 +59,12 @@ theorem SetShatters.subset {C : ConceptClass α Bool} {W V : Set α}
     (hW : SetShatters C W) (hVW : V ⊆ W) : SetShatters C V := by
   intro V' hV'V
   obtain ⟨c, hc, hc_eq⟩ := hW (V' ∪ (W \ V))
-    (union_subset (hV'V.trans hVW) diff_subset)
+    (union_subset (hV'V.trans hVW) sdiff_subset)
   refine ⟨c, hc, ?_⟩
   rw [show V = W ∩ V from (inter_eq_self_of_subset_right hVW).symm,
     ← inter_assoc, hc_eq]
   ext x
-  simp only [mem_inter_iff, mem_union, mem_diff]
+  simp only [mem_inter_iff, mem_union, mem_sdiff]
   refine ⟨?_, fun h => ⟨Or.inl h, hV'V h⟩⟩
   rintro ⟨h1 | ⟨_, h2⟩, h3⟩
   · exact h1

CslibTests.lean

@@ -1,15 +1,13 @@
-module  -- shake: keep-all --deprecated_module: ignore
-
-public import CslibTests.Bisimulation
-public import CslibTests.CCS
-public import CslibTests.CLL
-public import CslibTests.DFA
-public import CslibTests.FreeMonad
-public import CslibTests.GrindLint
-public import CslibTests.HML
-public import CslibTests.HasFresh
-public import CslibTests.ImportWithMathlib
-public import CslibTests.LTS
-public import CslibTests.LambdaCalculus
-public import CslibTests.MLL
-public import CslibTests.Reduction
+import CslibTests.Bisimulation
+import CslibTests.CCS
+import CslibTests.CLL
+import CslibTests.DFA
+import CslibTests.FreeMonad
+import CslibTests.GrindLint
+import CslibTests.HML
+import CslibTests.HasFresh
+import CslibTests.ImportWithMathlib
+import CslibTests.LTS
+import CslibTests.LambdaCalculus
+import CslibTests.MLL
+import CslibTests.Reduction

lake-manifest.json

@@ -5,10 +5,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "d90090f647cae4f4ad4da99c0ac8bab2ca8c34ab",
+   "rev": "8589236b8b8cc82492e3306df39c0fb308e0523c",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "d90090f647cae4f4ad4da99c0ac8bab2ca8c34ab",
+   "inputRev": "8589236b8b8cc82492e3306df39c0fb308e0523c",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/plausible",
@@ -48,7 +48,7 @@
    "rev": "1537e3fc7e680d64e06fe5fb95c4c9edee7941c2",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.101",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
@@ -58,7 +58,7 @@
    "rev": "7897ea6e5cfc6522d355083bdfa798377ab35e11",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.31.0-rc2",
+   "inputRev": "master",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/quote4",
@@ -68,17 +68,17 @@
    "rev": "94346b7b49c36ae871639d1434232f057c193d60",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.31.0-rc2",
+   "inputRev": "master",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "460b61adc7d183e43db2b99ac6c1dede9f7a76df",
+   "rev": "0bbac0a875ac0fd9366cb5bd4211da92d960ac84",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v4.31.0-rc2",
+   "inputRev": "main",
    "inherited": true,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover/lean4-cli",