chore: adaptations for nightly-2025-06-04 (#25431)

* Update lean-toolchain for testing leanprover/lean4#8347

* fixes for leanprover/lean4#8347

* Update lean-toolchain for testing leanprover/lean4#8397

* deprecations for leanprover/lean4#8397

* chore: bump to nightly-2025-05-19

* chore: adaptations for nightly-2025-05-19

* Trigger CI for leanprover/lean4#8347

* Update the style linter to use LinterOptions

* Fix test

* chore: adaptations for nightly-2025-05-19 (#25017)



Co-authored-by: Kim Morrison <[email protected]>
Co-authored-by: github-actions <[email protected]>
Co-authored-by: mathlib4-bot <[email protected]>
Co-authored-by: Anne C.A. Baanen <[email protected]>
Co-authored-by: Sebastian Ullrich <[email protected]>

* chore: bump to nightly-2025-05-20

* Merge master into nightly-testing

* feat: a `grind` test case (#25037)

Adds a test case for `grind` that was previously failing in the presence of Mathlib's typeclass shortcuts. Let's just keep it in Mathlib as a regression test.

Note that this is a PR to `bump/v4.21.0`, as it requires a recent nightly toolchain. (It can still be reviewed and bors'd as any other PR.)

* lake update

* fixes

* fixes

* fixes

* fixes

* fix

* fixes

* fixes

* shake --update

* chore: bump to nightly-2025-05-21

* Update lean-toolchain for testing leanprover/lean4#7352

* lake update

* Trigger CI for leanprover/lean4#7352

* chore: adaptations for nightly-2025-05-21

* chore: adaptations for nightly-2025-05-21 (#25079)



Co-authored-by: mathlib4-bot <[email protected]>
Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>
Co-authored-by: github-actions <[email protected]>
Co-authored-by: Anne C.A. Baanen <[email protected]>

* chore: adaptations for nightly-2025-05-21

* fix for leanprover/lean4#7352

* remove unneeded List.ofFn_succ from simp sets

* Merge master into nightly-testing

* Merge master into nightly-testing

* Revert "fix for leanprover/lean4#7352"

This reverts commit 38ca408.

* chore: fix some defeq abuse in theorem statements around the `Id` monad (#25098)

Follows on from leanprover/lean4#7352.

This also deprecates:
* `id.mk`, which looks like a porting error
* `Free(Add)(Magma|Semigroup).mul_map_seq`, which is a garbage lemma that both is not meaningfully about the free objects and has defeq abuse everywhere.

* chore: bump to nightly-2025-05-22

* update batteries

* chore: bump to nightly-2025-05-23

* Update lean-toolchain for testing leanprover/lean4#8449

* chore: adaptations for nightly-2025-05-22 (#25110)



Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>
Co-authored-by: Kim Morrison <[email protected]>
Co-authored-by: github-actions <[email protected]>

* remove now upstreamed `clear_value`

* Update lean-toolchain for testing leanprover/lean4#8457

* chore: update tests for `Format` bug fix

* Trigger CI for leanprover/lean4#8457

* lake update

* lake update

* fixes

* Merge master into nightly-testing

* chore: bump to nightly-2025-05-24

* fix

* chore: adaptations for nightly-2025-05-24 (#25147)



Co-authored-by: Kim Morrison <[email protected]>
Co-authored-by: mathlib4-bot <[email protected]>
Co-authored-by: Eric Wieser <[email protected]>
Co-authored-by: github-actions <[email protected]>

* chore: adaptations for nightly-2025-05-24

* Merge master into nightly-testing

* Update lean-toolchain for testing leanprover/lean4#8470

* chore: bump to nightly-2025-05-25

* chore: adaptations for nightly-2025-05-25

* chore: adaptations for nightly-2025-05-25 (#25184)



Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>
Co-authored-by: Eric Wieser <[email protected]>
Co-authored-by: Kim Morrison <[email protected]>
Co-authored-by: github-actions <[email protected]>

* unsimp `List.getElem?_length`

This is solved using `getElem?_neg` now.

* chore: adaptations for nightly-2025-05-25

* Trigger CI for leanprover/lean4#8470

* chore: bump to nightly-2025-05-26

* lake update

* deprecations

* Trigger CI for leanprover/lean4#8449

* Merge master into nightly-testing

* chore: bump to nightly-2025-05-27

* chore: adaptations for nightly-2025-05-27

* Update lean-toolchain for testing leanprover/lean4#8504

* chore: bump to nightly-2025-05-28

* chore: adaptations for nightly-2025-05-27 (#25234)



Co-authored-by: mathlib4-bot <[email protected]>
Co-authored-by: github-actions <[email protected]>
Co-authored-by: Kim Morrison <[email protected]>

* fix

* fix merge

* fix merge again

* deprecations

* deprecations

* fix Archive

* comment out test

* Fix and re-enable directory dependency lint test.

* chore: bump to nightly-2025-05-29

* Use the formatting from the master branch. (Seems to have been a merge that went wrong.)

* lake update

* chore: adaptations for nightly-2025-05-28 (#25295)



Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>
Co-authored-by: mathlib4-bot <[email protected]>
Co-authored-by: github-actions <[email protected]>

* fix

* Trigger CI for leanprover/lean4#8337

* fixes

* Merge master into nightly-testing

* chore: bump to nightly-2025-05-30

* chore: adaptations for nightly-2025-05-29 (#25306)



Co-authored-by: Kim Morrison <[email protected]>
Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>
Co-authored-by: mathlib4-bot <[email protected]>
Co-authored-by: github-actions <[email protected]>
Co-authored-by: Rob23oba <[email protected]>

* chore: bump to nightly-2025-05-31

* chore: bump to nightly-2025-06-01

* fix Archive

* chore: adaptations for nightly-2025-06-01 (#25355)



Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>
Co-authored-by: Anne C.A. Baanen <[email protected]>
Co-authored-by: github-actions <[email protected]>
Co-authored-by: mathlib4-bot <[email protected]>

* chore: bump to nightly-2025-06-02

* chore: adaptations for nightly-2025-06-02 (#25360)



Co-authored-by: Kim Morrison <[email protected]>
Co-authored-by: mathlib4-bot <[email protected]>
Co-authored-by: Anne C.A. Baanen <[email protected]>
Co-authored-by: github-actions <[email protected]>

* Update lean-toolchain for testing leanprover/lean4#8584

* chore: adaptations for nightly-2025-06-02

* chore: bump to nightly-2025-06-03

* fix

* fix

* Update lean-toolchain for testing leanprover/lean4#8610

* fix

* chore: bump to nightly-2025-06-04

* bump toolchain

---------

Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>
Co-authored-by: Kim Morrison <[email protected]>
Co-authored-by: github-actions <[email protected]>
Co-authored-by: mathlib4-bot <[email protected]>
Co-authored-by: Anne C.A. Baanen <[email protected]>
Co-authored-by: Sebastian Ullrich <[email protected]>
Co-authored-by: Eric Wieser <[email protected]>
Co-authored-by: Rob23oba <[email protected]>
Co-authored-by: Joseph Rotella <[email protected]>

Author: 9 people

Mathlib/Data/Int/Order/Basic.lean

@@ -16,8 +16,6 @@ open Nat
 
 namespace Int
 
-export private decNonneg from Init.Data.Int.Basic
-
 theorem le.elim {a b : ℤ} (h : a ≤ b) {P : Prop} (h' : ∀ n : ℕ, a + ↑n = b → P) : P :=
   Exists.elim (le.dest h) h'
 

Mathlib/Lean/Name.lean

@@ -58,10 +58,10 @@ def Lean.Name.decapitalize (n : Name) : Name :=
 /-- Whether the lemma has a name of the form produced by `Lean.Meta.mkAuxLemma`. -/
 def Lean.Name.isAuxLemma (n : Name) : Bool :=
   match n with
-  | .str _ s => "_proof_".isPrefixOf s
+  -- `mkAuxLemma` generally allows for arbitrary prefixes but these are the ones produced by core.
+  | .str _ s => "_proof_".isPrefixOf s || "_simp_".isPrefixOf s
   | _ => false
 
-/-- Unfold all lemmas created by `Lean.Meta.mkAuxLemma`.
-The names of these lemmas end in `_auxLemma.nn` where `nn` is a number. -/
+/-- Unfold all lemmas created by `Lean.Meta.mkAuxLemma`. -/
 def Lean.Meta.unfoldAuxLemmas (e : Expr) : MetaM Expr := do
   deltaExpand e Lean.Name.isAuxLemma

lake-manifest.json

@@ -5,10 +5,10 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "91ce5a8051438870cbb4e3c68cd12e23ace713b1",
+   "rev": "fde3fc21dd68a10791dea22b6f5b53c5a5a5962d",
    "name": "plausible",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "nightly-testing",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/LeanSearchClient",
@@ -25,7 +25,7 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "d554d45b37832f5f8e8797ac0b00be585c8aea49",
+   "rev": "e25fe66cf13e902ba550533ef681cc35a9f18dc2",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -35,27 +35,27 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "7518acaafc0ba29be6de6c3f37637fe4148b72cb",
+   "rev": "2d6d124aedc3023506a67e50bfd5582384d6bd17",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.61",
+   "inputRev": "v0.0.63-pre",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "c548baa6d2ed727c6e9b30ff627b7c67fda4a54c",
+   "rev": "c37af3a23d5798c560bce190bfd779710eaff1e1",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "master",
+   "inputRev": "nightly-testing",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "f827c08bdd5044b75f0fdc3178c0c600e818b76f",
+   "rev": "e1d2994e0acdee2f0c03c9d84d28a5df34aa0020",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -65,17 +65,17 @@
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",
-   "rev": "3aafa48516440d6038efb626660c74dec6e640da",
+   "rev": "3253675d6329e9c1ad6f762e8989f4b8a28ffa8f",
    "name": "batteries",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "main",
+   "inputRev": "nightly-testing",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
    "scope": "leanprover",
-   "rev": "1606fed39cd8bd366f8a192e6558972af869efa6",
+   "rev": "a0abd472348dd725adbb26732e79b26e7e220913",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",

lakefile.lean

@@ -7,17 +7,17 @@ open Lake DSL
 ## Mathlib dependencies on upstream projects
 -/
 
-require "leanprover-community" / "batteries" @ git "main"
+require "leanprover-community" / "batteries" @ git "nightly-testing"
 require "leanprover-community" / "Qq" @ git "master"
-require "leanprover-community" / "aesop" @ git "master"
-require "leanprover-community" / "proofwidgets" @ git "v0.0.62" -- ProofWidgets should always be pinned to a specific version
+require "leanprover-community" / "aesop" @ git "nightly-testing"
+require "leanprover-community" / "proofwidgets" @ git "v0.0.63-pre" -- ProofWidgets should always be pinned to a specific version
   with NameMap.empty.insert `errorOnBuild
     "ProofWidgets not up-to-date. \
     Please run `lake exe cache get` to fetch the latest ProofWidgets. \
     If this does not work, report your issue on the Lean Zulip."
 require "leanprover-community" / "importGraph" @ git "main"
 require "leanprover-community" / "LeanSearchClient" @ git "main"
-require "leanprover-community" / "plausible" @ git "main"
+require "leanprover-community" / "plausible" @ git "nightly-testing"
 
 /-!
 ## Options for building mathlib

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2025-06-02
+leanprover/lean4:nightly-2025-06-04