chore: adaptations for nightly-2025-07-03 (#10)

* fix

* fixes

* chore: adaptations for nightly-2025-06-16 (leanprover-community#25994)

* 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 <[email protected]>

* 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

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

* fix upstream

* fix

* fix

* fixes

---------

Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>
Co-authored-by: github-actions <[email protected]>
Co-authored-by: mathlib4-bot <[email protected]>
Co-authored-by: Sebastian Ullrich <[email protected]>
Co-authored-by: Johan Commelin <[email protected]>
Co-authored-by: Jovan Gerbscheid <[email protected]>
Co-authored-by: Kim Morrison <[email protected]>
Co-authored-by: Joachim Breitner <[email protected]>
Co-authored-by: Mario Carneiro <[email protected]>
Co-authored-by: sgouezel <[email protected]>
Co-authored-by: Kyle Miller <[email protected]>

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

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

* fixes

* more fixes

* fixes!

* more fixes!

* hmm

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

* chore: adaptations for nightly-2025-06-17 (leanprover-community#26043)

* 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 <[email protected]>

* 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

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

* fix upstream

* fix

* fix

* fixes

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

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

* fixes

* more fixes

* fixes!

* more fixes!

* hmm

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

---------

Co-authored-by: Jovan Gerbscheid <[email protected]>
Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>
Co-authored-by: Johan Commelin <[email protected]>
Co-authored-by: github-actions <[email protected]>
Co-authored-by: Kim Morrison <[email protected]>
Co-authored-by: Joachim Breitner <[email protected]>
Co-authored-by: mathlib4-bot <[email protected]>
Co-authored-by: Sebastian Ullrich <[email protected]>
Co-authored-by: Mario Carneiro <[email protected]>
Co-authored-by: sgouezel <[email protected]>
Co-authored-by: Kyle Miller <[email protected]>
Co-authored-by: Rob23oba <[email protected]>

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

* chore: lint `show` (adaptation for leanprover/lean4#7395) (leanprover-community#25749)

Adds `show` as an exception to the unused tactic linter and adds a separate linter for `show`s that should be replaced by `change`.
Context: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/unused.20tactic.20linter.20for.20.60show.60/with/523701633

Co-authored-by: Christian Merten <[email protected]>
Co-authored-by: Kenny Lau <[email protected]>
Co-authored-by: Fabrizio Barroero <[email protected]>
Co-authored-by: Rob23oba <[email protected]>
Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>
Co-authored-by: Rob23oba <[email protected]>
Co-authored-by: Kim Morrison <[email protected]>

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

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

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

* Merge master into nightly-testing

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

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

* bump Qq and batteries

* meta adaptations

* bump aesop

* fix

* fix (adaptation note)

* Update lean-toolchain for leanprover/lean4#8699

* shake

* chore: adaptations for nightly-2025-06-18 (leanprover-community#26077)

* 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 <[email protected]>

* 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

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

* fix upstream

* fix

* fix

* fixes

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

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

* fixes

* more fixes

* fixes!

* more fixes!

* hmm

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

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

* chore: lint `show` (adaptation for leanprover/lean4#7395) (leanprover-community#25749)

Adds `show` as an exception to the unused tactic linter and adds a separate linter for `show`s that should be replaced by `change`.
Context: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/unused.20tactic.20linter.20for.20.60show.60/with/523701633

Co-authored-by: Christian Merten <[email protected]>
Co-authored-by: Kenny Lau <[email protected]>
Co-authored-by: Fabrizio Barroero <[email protected]>
Co-authored-by: Rob23oba <[email protected]>
Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>
Co-authored-by: Rob23oba <[email protected]>
Co-authored-by: Kim Morrison <[email protected]>

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

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

---------

Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>
Co-authored-by: Kim Morrison <[email protected]>
Co-authored-by: Joachim Breitner <[email protected]>
Co-authored-by: mathlib4-bot <[email protected]>
Co-authored-by: Johan Commelin <[email protected]>
Co-authored-by: Jovan Gerbscheid <[email protected]>
Co-authored-by: github-actions <[email protected]>
Co-authored-by: Sebastian Ullrich <[email protected]>
Co-authored-by: Mario Carneiro <[email protected]>
Co-authored-by: sgouezel <[email protected]>
Co-authored-by: Kyle Miller <[email protected]>
Co-authored-by: Rob23oba <[email protected]>
Co-authored-by: Rob23oba <[email protected]>
Co-authored-by: Christian Merten <[email protected]>
Co-authored-by: Kenny Lau <[email protected]>
Co-authored-by: Fabrizio Barroero <[email protected]>
Co-authored-by: Rob23oba <[email protected]>

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

* feat: add algebra shims for Grind.Nat/IntModule (leanprover-community#26133)

This PR adds shims so `grind` will understand Mathlib's `AddCommMonoid` and `AddCommGroup`. (Subsequent shims will connect up the order structures for modules and rings.)

* fix

* Update lean-toolchain for leanprover/lean4#8699

* fix: correct memoFix's use of unsafe code

* fix: adjust noncomputable annotations for new compiler

* fix: replace use of `open private _ in` with `open private _ from`

The implementation of `open private _ from` relies on specific
internals of the old compiler and will no longer work.

* remove mul_hmul

* chore: adjust one maxHeartbeats for the new compiler

* linter

* feat: generalize grind algebra shims (leanprover-community#26131)

This PR extends the shims converting from Mathlib to `Lean.Grind` typeclasses, now that `grind` knows about (non-commutative)-(semi)-rings.

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

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

* chore: adaptations for nightly-2025-06-20 (leanprover-community#26209)

* 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 <[email protected]>

* 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

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

* fix upstream

* fix

* fix

* fixes

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

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

* fixes

* more fixes

* fixes!

* more fixes!

* hmm

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

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

* chore: lint `show` (adaptation for leanprover/lean4#7395) (leanprover-community#25749)

Adds `show` as an exception to the unused tactic linter and adds a separate linter for `show`s that should be replaced by `change`.
Context: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/unused.20tactic.20linter.20for.20.60show.60/with/523701633

Co-authored-by: Christian Merten <[email protected]>
Co-authored-by: Kenny Lau <[email protected]>
Co-authored-by: Fabrizio Barroero <[email protected]>
Co-authored-by: Rob23oba <[email protected]>
Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>
Co-authored-by: Rob23oba <[email protected]>
Co-authored-by: Kim Morrison <[email protected]>

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

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

* Merge master into nightly-testing

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

* fix

* remove mul_hmul

* linter

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

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

---------

Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>
Co-authored-by: github-actions <[email protected]>
Co-authored-by: Joachim Breitner <[email protected]>
Co-authored-by: Kim Morrison <[email protected]>
Co-authored-by: Sebastian Ullrich <[email protected]>
Co-authored-by: mathlib4-bot <[email protected]>
Co-authored-by: Mario Carneiro <[email protected]>
Co-authored-by: Johan Commelin <[email protected]>
Co-authored-by: sgouezel <[email protected]>
Co-authored-by: Kyle Miller <[email protected]>
Co-authored-by: Rob23oba <[email protected]>
Co-authored-by: Rob23oba <[email protected]>
Co-authored-by: Christian Merten <[email protected]>
Co-authored-by: Kenny Lau <[email protected]>
Co-authored-by: Fabrizio Barroero <[email protected]>
Co-authored-by: Rob23oba <[email protected]>

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

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

* fix

* fixes

* fixes

* fixes

* updated lake manifest

* comment out tests

* chore: fix for nightly-testing (leanprover-community#26246)

* fix

* fix

* fix grind typeclasses

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

* lake update

* Update lean-toolchain for leanprover/lean4#8914

* fix grind instance

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

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

* chore: rm unused `Lean.Util.Paths` import & use updated batteries

* Ensure we checkout mathlib4 master, not nightly-testing master (which does not exist)

* merge lean-pr-testing-8804

* Bump dependencies and silence linter.

* Fixes

(Now `elabSimpArgs` already handles `*`, so we can delete the associated code.)

* lake update; disable unusedSimpArgs in Batteries

* lkae update aesop

* disable unusedSimpArgs in MathlibTest

* fix grind instance priorities

* comment out MathlibTest/zmod with adaptation note

* touch for CI

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

* Kick CI

* Bump batteries

* Guessing adaption for leanprover/lean4#8929

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

* fix: workflow merging master into nightly-testing

* fix

* chore: cache get uses tracking remote

* touch for new CI

* restart CI

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

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

* Teach Mathlib about `mrefine`

* Merge master into nightly-testing

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

* chore: update linter warning test outputs

* chore: remove excess line break in deprecation lint now that notes add their own line breaks

* chore: more test cleanup

* .

* cleanup adaptation notes

* fix

* fix

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

* chore: adaptations for nightly-2025-06-26 (#2)

* Merge master into nightly-testing

* Merge master into nightly-testing

* re-enable unusedSimpArgs

* re-enable unusedSimpArgs

* re-enable unusedSimpArgs

* re-enable unusedSimpArgs

* re-enable unusedSimpArgs

* chore: adaptations for nightly-2025-06-27 (#3)

* fix tests

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

* Merge master into nightly-testing

* lintining

* Merge master into nightly-testing

* unused simp args

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

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

* chore: adaptations for nightly-2025-06-28 (#5)

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

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

* Update Shake/Main.lean

Co-authored-by: Johan Commelin <[email protected]>

* 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

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

* fix upstream

* fix

* fix

* fixes

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

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

* fixes

* more fixes

* fixes!

* more fixes!

* hmm

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

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

* chore: lint `show` (adaptation for leanprover/lean4#7395) (leanprover-community#25749)

Adds `show` as an exception to the unused tactic linter and adds a separate linter for `show`s that should be replaced by `change`.
Context: https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/unused.20tactic.20linter.20for.20.60show.60/with/523701633

Co-authored-by: Christian Merten <[email protected]>
Co-authored-by: Kenny Lau <[email protected]>
Co-authored-by: Fabrizio Barroero <[email protected]>
Co-authored-by: Rob23oba <[email protected]>
Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>
Co-authored-by: Rob23oba <[email protected]>
Co-authored-by: Kim Morrison <[email protected]>

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

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

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

* Merge master into nightly-testing

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

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

* bump Qq and batteries

* meta adaptations

* bump aesop

* fix

* fix (adaptation note)

* Update lean-toolchain for leanprover/lean4#8699

* shake

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

* fix

* Update lean-toolchain for leanprover/lean4#8699

* fix: correct memoFix's use of unsafe code

* fix: adjust noncomputable annotations for new compiler

* fix: replace use of `open private _ in` with `open private _ from`

The implementation of `open private _ from` relies on specific
internals of the old compiler and will no longer work.

* remove mul_hmul

* chore: adjust one maxHeartbeats for the new compiler

* linter

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

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

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

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

* fix

* fixes

* fixes

* fixes

* updated lake manifest

* comment out tests

* chore: fix for nightly-testing (leanprover-community#26246)

* fix

* fix

* fix grind typeclasses

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

* lake update

* Update lean-toolchain for leanprover/lean4#8914

* fix grind instance

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

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

* chore: rm unused `Lean.Util.Paths` import & use updated batteries

* Ensure we checkout mathlib4 master, not nightly-testing master (which does not exist)

* merge lean-pr-testing-8804

* Bump dependencies and silence linter.

* Fixes

(Now `elabSimpArgs` already handles `*`, so we can delete the associated code.)

* lake update; disable unusedSimpArgs in Batteries

* lkae update aesop

* disable unusedSimpArgs in MathlibTest

* fix grind instance priorities

* comment out MathlibTest/zmod with adaptation note

* touch for CI

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

* Kick CI

* Bump batteries

* Guessing adaption for leanprover/lean4#8929

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

* fix: workflow merging master into nightly-testing

* fix

* chore: cache get uses tracking remote

* touch for new CI

* restart CI

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

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

* Teach Mathlib about `mrefine`

* Merge master into nightly-testing

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

* chore: update linter warning test outputs

* chore: remove excess line break in deprecation lint now that notes add their own line breaks

* chore: more test cleanup

* .

* cleanup adaptation notes

* fix

* fix

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

* Merge master into nightly-testing

* Merge master into nightly-testing

* re-enable unusedSimpArgs

* re-enable unusedSimpArgs

* re-enable unusedSimpArgs

* re-enable unusedSimpArgs

* re-enable unusedSimpArgs

* fix tests

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

* Merge master into nightly-testing

* lintining

* lint

---------

Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>
Co-authored-by: mathlib4-bot <[email protected]>
Co-authored-by: Johan Commelin <[email protected]>
Co-authored-by: github-actions <[email protected]>
Co-authored-by: sgouezel <[email protected]>
Co-authored-by: Kyle Miller <[email protected]>
Co-authored-by: Sebastian Ullrich <[email protected]>
Co-authored-by: Rob23oba <[email protected]>
Co-authored-by: Rob23oba <[email protected]>
Co-authored-by: Christian Merten <[email protected]>
Co-authored-by: Kenny Lau <[email protected]>
Co-authored-by: Fabrizio Barroero <[email protected]>
Co-authored-by: Rob23oba <[email protected]>
Co-authored-by: Cameron Zwarich <[email protected]>
Co-authored-by: Mac Malone <[email protected]>
Co-authored-by: Anne C.A. Baanen <[email protected]>
Co-authored-by: Joachim Breitner <[email protected]>
Co-authored-by: Sebastian Graf <[email protected]>
Co-authored-by: Joseph Rotella <[email protected]>

* Merge master into nightly-testing

* chore: robustify `open Mathlib` benchmark

* deprecations

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

* Merge master into nightly-testing

* fixes

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

* lake update

* lake update

* lake update

* lake update

* lake update

* .

* Merge master into nightly-testing

* Merge master into nightly-testing

* Merge master into nightly-testing

* Merge master into nightly-testing

* cleanup

* unusedSimpArgs

* bump toolchain

* lake update

* Merge master into nightly-testing

* Merge master into nightly-testing

* chore: adaptations for nightly-2025-07-01

* add adaptation note

* add adaptation note

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

* fixes

* Merge master into nightly-testing

* fixes

* update test output

* Merge master into nightly-testing

* Merge master into nightly-testing

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

* chore: adaptations for nightly-2025-07-03

---------

Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>
Co-authored-by: mathlib4-bot <[email protected]>
Co-authored-by: leanprover-community-mathlib4-bot <129911861+leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: github-actions <[email protected]>
Co-authored-by: Sebastian Ullrich <[email protected]>
Co-authored-by: Johan Commelin <[email protected]>
Co-authored-by: Jovan Gerbscheid <[email protected]>
Co-authored-by: Joachim Breitner <[email protected]>
Co-authored-by: Mario Carneiro <[email protected]>
Co-authored-by: sgouezel <[email protected]>
Co-authored-by: Kyle Miller <[email protected]>
Co-authored-by: Rob23oba <[email protected]>
Co-authored-by: Rob23oba <[email protected]>
Co-authored-by: Christian Merten <[email protected]>
Co-authored-by: Kenny Lau <[email protected]>
Co-authored-by: Fabrizio Barroero <[email protected]>
Co-authored-by: Rob23oba <[email protected]>
Co-authored-by: Cameron Zwarich <[email protected]>
Co-authored-by: Mac Malone <[email protected]>
Co-authored-by: Anne C.A. Baanen <[email protected]>
Co-authored-by: Sebastian Graf <[email protected]>
Co-authored-by: Joseph Rotella <[email protected]>

Author: 21 people

Mathlib/Data/Nat/Hyperoperation.lean

@@ -63,7 +63,7 @@ theorem hyperoperation_two (m k : ℕ) : hyperoperation 2 m k = m * k := by
 
 @[simp, grind =]
 theorem hyperoperation_three (m k : ℕ) : hyperoperation 3 m k = m ^ k := by
-  induction k with grind [Nat.pow_succ]
+  induction k with grind
 
 @[grind =]
 theorem hyperoperation_ge_two_eq_self (n m : ℕ) : hyperoperation (n + 2) m 1 = m := by
@@ -80,7 +80,8 @@ theorem hyperoperation_ge_three_one (n k : ℕ) : hyperoperation (n + 3) 1 k = 1
   | succ n ih =>
     cases k
     · grind
-    · rw [hyperoperation_recursion, ih]
+    · #adaptation_note /-- This will work by `grind` after nightly-2025-07-02. -/
+      rw [hyperoperation_recursion, ih]
 
 @[grind =]
 theorem hyperoperation_ge_four_zero (n k : ℕ) :

Mathlib/Logic/Function/Defs.lean

@@ -82,7 +82,7 @@ theorem Bijective.comp {g : β → φ} {f : α → β} : Bijective g → Bijecti
   | ⟨h_ginj, h_gsurj⟩, ⟨h_finj, h_fsurj⟩ => ⟨h_ginj.comp h_finj, h_gsurj.comp h_fsurj⟩
 
 /-- `LeftInverse g f` means that `g` is a left inverse to `f`. That is, `g ∘ f = id`. -/
-@[grind ]
+@[grind]
 def LeftInverse (g : β → α) (f : α → β) : Prop :=
   ∀ x, g (f x) = x
 
@@ -91,7 +91,7 @@ def HasLeftInverse (f : α → β) : Prop :=
   ∃ finv : β → α, LeftInverse finv f
 
 /-- `RightInverse g f` means that `g` is a right inverse to `f`. That is, `f ∘ g = id`. -/
-@[grind ]
+@[grind]
 def RightInverse (g : β → α) (f : α → β) : Prop :=
   LeftInverse f g
 

Mathlib/RingTheory/FreeCommRing.lean

@@ -125,9 +125,7 @@ protected theorem induction_on {motive : FreeCommRing α → Prop} (z : FreeComm
   have neg : ∀ x, motive x → motive (-x) := fun x ih => neg_one_mul x ▸ mul _ _ neg_one ih
   have one : motive 1 := neg_neg (1 : FreeCommRing α) ▸ neg _ neg_one
   FreeAbelianGroup.induction_on z (neg_add_cancel (1 : FreeCommRing α) ▸ add _ _ neg_one one)
-    (fun m => Multiset.induction_on m one fun a m ih => by
-      convert mul (FreeCommRing.of a) _ (of a) ih
-      apply of_cons)
+    (fun m => Multiset.induction_on m one fun a _ ih => mul (FreeCommRing.of a) _ (of a) ih)
     (fun _ ih => neg _ ih) add
 
 section lift

Mathlib/RingTheory/FreeRing.lean

@@ -89,11 +89,7 @@ protected theorem induction_on {C : FreeRing α → Prop} (z : FreeRing α) (hn1
   have hn : ∀ x, C x → C (-x) := fun x ih => neg_one_mul x ▸ hm _ _ hn1 ih
   have h1 : C 1 := neg_neg (1 : FreeRing α) ▸ hn _ hn1
   FreeAbelianGroup.induction_on z (neg_add_cancel (1 : FreeRing α) ▸ ha _ _ hn1 h1)
-    (fun m => List.recOn m h1 fun a m ih => by
-      -- Porting note: in mathlib, convert was not necessary, `exact hm _ _ (hb a) ih` worked fine
-      convert hm _ _ (hb a) ih
-      rw [of, ← FreeAbelianGroup.of_mul]
-      rfl)
+    (fun m => List.recOn m h1 fun a _ ih => hm _ _ (hb a) ih)
     (fun _ ih => hn _ ih) ha
 
 section lift

MathlibTest/FinCoercions.lean

@@ -14,9 +14,9 @@ set_option pp.mvars false
 error: type mismatch
   n
 has type
-  ℕ : Type
+  ℕ
 but is expected to have type
-  Fin 3 : Type
+  Fin 3
 ---
 info: fun n => sorry : (n : ℕ) → ?_ n
 -/

MathlibTest/ImplicitUniverses.lean

@@ -1,43 +1,54 @@
 import Mathlib.Tactic.TypeStar
 import Mathlib.Tactic.SuccessIfFailWithMsg
 
-private axiom test_sorry : ∀ {α}, α
-noncomputable example (_x _y : Type*) : test_sorry := by
-  success_if_fail_with_msg
-"type mismatch
+/--
+error: type mismatch
   _y
 has type
-  Type u_2 : Type (u_2 + 1)
-but is expected to have type
-  Type u_1 : Type (u_1 + 1)" (exact _x = _y)
-  exact test_sorry
+  Type u_2
+of sort `Type (u_2 + 1)` but is expected to have type
+  Type u_1
+of sort `Type (u_1 + 1)`
+-/
+#guard_msgs in
+noncomputable example (_x _y : Type*) : sorry := by
+  exact _x = _y
 
-noncomputable example (_x : Sort*) : test_sorry := by
-  success_if_fail_with_msg
-"type mismatch
+/--
+error: type mismatch
   Prop
 has type
-  Type : Type 1
-but is expected to have type
-  Sort u_1 : Type u_1" (exact _x = Prop)
-  exact test_sorry
+  Type
+of sort `Type 1` but is expected to have type
+  Sort u_1
+of sort `Type u_1`
+-/
+#guard_msgs in
+noncomputable example (_x : Sort*) : sorry := by
+  exact _x = Prop
 
-noncomputable example : test_sorry := by
-  success_if_fail_with_msg
-"type mismatch
+/--
+error: type mismatch
   y
 has type
-  Type u_2 : Type (u_2 + 1)
-but is expected to have type
-  Type u_1 : Type (u_1 + 1)" (exact ∀ x y : Type*, x = y)
-  exact test_sorry
+  Type u_2
+of sort `Type (u_2 + 1)` but is expected to have type
+  Type u_1
+of sort `Type (u_1 + 1)`
+-/
+#guard_msgs in
+noncomputable example : sorry := by
+  exact ∀ x y : Type*, x = y
 
-noncomputable example : test_sorry := by
-  success_if_fail_with_msg
-"type mismatch
+/--
+error: type mismatch
   Prop
 has type
-  Type : Type 1
-but is expected to have type
-  Sort u_1 : Type u_1" (exact ∀ x : Sort*, x = Prop)
-  exact test_sorry
+  Type
+of sort `Type 1` but is expected to have type
+  Sort u_1
+of sort `Type u_1`
+-/
+#guard_msgs in
+noncomputable example : sorry := by
+  exact ∀ x : Sort*, x = Prop

MathlibTest/Recall.lean

@@ -51,9 +51,10 @@ recall id (x : α) : α := x
 error: type mismatch
   @id
 has type
-  {α : Sort u_1} → α → α → ℕ : Type u_1
-but is expected to have type
-  {α : Sort u} → α → α : Sort (imax (u + 1) u)
+  {α : Sort u_1} → α → α → ℕ
+of sort `Type u_1` but is expected to have type
+  {α : Sort u} → α → α
+of sort `Sort (imax (u + 1) u)`
 -/
 #guard_msgs in recall id (_x _y : α) : ℕ := 0
 

MathlibTest/Use.lean

@@ -163,9 +163,10 @@ example : Baz 0 3 := by use 4
 error: type mismatch
   3
 has type
-  Nat : Type
-but is expected to have type
-  Baz 1 3 : Prop
+  Nat
+of sort `Type` but is expected to have type
+  Baz 1 3
+of sort `Prop`
 -/
 #guard_msgs in
 example : Baz 1 3 := by use (3 : Nat)

MathlibTest/linear_combination'.lean

@@ -206,9 +206,9 @@ error: Application type mismatch: In the application
 the argument
   0
 has type
-  ℝ : Type
+  ℝ
 but is expected to have type
-  ℤ : Type
+  ℤ
 -/
 #guard_msgs in
 example (x y : ℤ) (h1 : x * y + 2 * x = 1) (h2 : x = y) : x * y + 2 * x = 1 := by

MathlibTest/linear_combination.lean

@@ -319,9 +319,9 @@ error: Application type mismatch: In the application
 the argument
   0
 has type
-  ℝ : Type
+  ℝ
 but is expected to have type
-  ℤ : Type
+  ℤ
 -/
 #guard_msgs in
 example (x y : ℤ) (h1 : x * y + 2 * x = 1) (h2 : x = y) : x * y + 2 * x = 1 := by