* 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 <kim@tqft.net>
Co-authored-by: github-actions <github-actions@github.com>
Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>

* 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 <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: github-actions <github-actions@github.com>
Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>

* 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 <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: github-actions <github-actions@github.com>

* 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 <kim@tqft.net>
Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: github-actions <github-actions@github.com>

* 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 <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: github-actions <github-actions@github.com>

* 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 <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: github-actions <github-actions@github.com>
Co-authored-by: Kim Morrison <kim@tqft.net>

* 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 <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: github-actions <github-actions@github.com>

* 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 <kim@tqft.net>
Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: github-actions <github-actions@github.com>
Co-authored-by: Rob23oba <robin.arnez@web.de>

* 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 <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>
Co-authored-by: github-actions <github-actions@github.com>
Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>

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

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



Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>
Co-authored-by: github-actions <github-actions@github.com>

* 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 <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: github-actions <github-actions@github.com>
Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Rob23oba <robin.arnez@web.de>
Co-authored-by: Joseph Rotella <7482866+jrr6@users.noreply.github.com>

* 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 <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: github-actions <github-actions@github.com>

* 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 <kim@tqft.net>
Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: github-actions <github-actions@github.com>

* 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 <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: github-actions <github-actions@github.com>

* 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 <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: github-actions <github-actions@github.com>
Co-authored-by: Kim Morrison <kim@tqft.net>

* fix

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

* 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 <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: github-actions <github-actions@github.com>

* fix

* Trigger CI for leanprover/lean4#8337

* Trigger CI for leanprover/lean4#8519

* 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 <kim@tqft.net>
Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: github-actions <github-actions@github.com>
Co-authored-by: Rob23oba <robin.arnez@web.de>

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

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

* chore: remove simp attribute when value of argument can not be inferred by simp

* fix Archive

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



Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>
Co-authored-by: github-actions <github-actions@github.com>
Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>

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

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



Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>
Co-authored-by: github-actions <github-actions@github.com>

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

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

* change phrasing of comments

* chore(Geometry/Manifold): two simp-lemmas can be proven by simp

* fix two lint problems

* Trigger CI for leanprover/lean4#8519

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

* fix

* fix

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

* fix

* revert change in `Mathlib.Data.ZMOD.Basic`

* fix Mathlib/Data/List/EditDistance/Estimator.lean

* give specialized simp lemmas higher prio

* simp can prove these

* simp can prove these

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

* bump toolchain

* Adapt eqns

* Revert "Adapt eqns"

This reverts commit 34f1f7f.

* Simply remove check for now

* fix a bunch

* fixes?

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

* add `simp low` lemma `injOn_of_eq_iff_eq`

* wip

* wip

* wip

* fix

* Trigger CI for leanprover-community/batteries#1220

* Merge master into nightly-testing

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

* Kick CI

* Bump lean4-cli

* Bump import-graph

* Kick CI

* update lakefile

* chore: use more robust syntax quotation in Shake

* cleanup lakefile

---------

Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: github-actions <github-actions@github.com>
Co-authored-by: Rob23oba <robin.arnez@web.de>
Co-authored-by: Joseph Rotella <7482866+jrr6@users.noreply.github.com>
Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Jovan Gerbscheid <jovan.gerbscheid@gmail.com>
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>

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

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

* change phrasing of comments

* chore(Geometry/Manifold): two simp-lemmas can be proven by simp

* fix two lint problems

* Trigger CI for leanprover/lean4#8519

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

* fix

* fix

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

* fix

* revert change in `Mathlib.Data.ZMOD.Basic`

* fix Mathlib/Data/List/EditDistance/Estimator.lean

* give specialized simp lemmas higher prio

* simp can prove these

* simp can prove these

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

* bump toolchain

* Adapt eqns

* Revert "Adapt eqns"

This reverts commit 34f1f7f.

* Simply remove check for now

* fix a bunch

* fixes?

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

* add `simp low` lemma `injOn_of_eq_iff_eq`

* wip

* wip

* wip

* fix

* Trigger CI for leanprover-community/batteries#1220

* Merge master into nightly-testing

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

* Kick CI

* Bump lean4-cli

* Bump import-graph

* Kick CI

* update lakefile

* chore: use more robust syntax quotation in Shake

* Trigger CI for leanprover/lean4#8419

* Revert "chore: use more robust syntax quotation in Shake"

This reverts commit cd87328.

* fix(Shake): fix import syntax

@Kha this is deliberately using this approach because syntax quotations
are also not robust but for a different reason: they fail to parse the
new versions of the syntax (and do so at run time). And using all the
optional doohickeys will not be future proof. The current setup is
explicitly meant to ping me when there is a syntax change so I can
evaluate the right way to handle it. In this case we want all the
module options to be ignored (treated the same as a regular import
for the purpose of dependency tracking), we don't want to fail.

* cleanup lakefile

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

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

* fix

* how did this get dropped?!?!

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

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

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

* fix lakefile

* fix lint-style for new Lean.Options API

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

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

* merge lean-pr-testing-4

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

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

* Update Shake/Main.lean

Co-authored-by: Johan Commelin <johan@commelin.net>

* Apply suggestions from code review

* revert

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

* cleanup grind tests

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

* merge lean-pr-testing-8419

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

* merge lean-pr-testing-8653

* adaptation note

* oops

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

* remove nolint simpNF

* remove spurious file

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

* fix

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

* Merge master into nightly-testing

* fix

* remove upstreamed

* drop no-op `show`

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

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

* intentionally left blank

* fix tests

---------

Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: github-actions <github-actions@github.com>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Co-authored-by: Jovan Gerbscheid <jovan.gerbscheid@gmail.com>
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
Co-authored-by: Mario Carneiro <di.gama@gmail.com>
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>