These proofs (and probably others) are causing CI failures. We can revert this after leanprover/lean4#9825 is fixed.

cf. [#mathlib4 > Failing CI @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Failing.20CI/near/533684295)

* grind lemma

* more

* chore(Cache): enable FRO cache (#17)

* chore: revert "enable FRO cache (#17)"

This reverts commit 1da13d9.

* Restore regression

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

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

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

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

* adaptation notes

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

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

* fix; bad merge?

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

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

* deprecation

* Update lean-toolchain for leanprover/lean4#9633

* chore: update test error message outputs

* adaptation note about Xor'

* shake --update

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

* fix

* fix test output

* fix test output

* fix test output

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

* fix

* Update lean-toolchain for leanprover/lean4#9587

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

* Bump batteries

* Fix warning

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

* update test

* fix test

* fix merge?

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

* fix

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

* deprecations

* shake --fix

* fix imports

* remove Shake again?

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

* fix

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

* lake update aesop

* lake update aesop

* deprecations

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

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

* Update lean-toolchain for leanprover/lean4#9800

* Update lean-toolchain for leanprover/lean4#9800

* Update lean-toolchain for leanprover/lean4#9800

* addressing some cases of mathlib4#380

* fix tests

* Update lean-toolchain for leanprover/lean4#9800

* Update lean-toolchain for leanprover/lean4#9800

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

* fix (all?) `protected` regressions

* Update lean-toolchain for leanprover/lean4#9800

* fix

* adaptation note?

* noncomputable

* revert grind proof

* remove upstreamed

* fixes

* feat: better statement of flip_map_app

* sad adaptation note

* update adaptation note

* fix merge

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

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

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

* fixes

* fix

* fix toolchain?

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

* use legacy lemma for now

* revert bad changes

* upstream LE/LT (Subtype p) instances

* chore(Cache): use FRO cache (v2) (#30)

* chore(Cache): enable FRO cache

* feat: only print "packing" when actually packing

* feat: always prefix with repo in FRO cache

* fix

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

* chore: trigger rebuild to test cache

* chore: use `cache put!` in CI to debug

* shake --update

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

* empty

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

* Revert "chore: use `cache put!` in CI to debug"

This reverts commit 7c6202b.

* redundant grind warnings

* revert leanprover-community#28272: add back grind proofs

* fix test

* chore: adaptations for nightly-2025-08-13

* fixes

* empty commit

* restore test

---------

Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: Mac Malone <tydeu@hatpress.net>
Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Mac Malone <mac@lean-fro.org>
Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: Joseph Rotella <7482866+jrr6@users.noreply.github.com>
Co-authored-by: github-actions <github-actions@github.com>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>

* fix test output

* fix test output

* fix test output

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

* fix

* Update lean-toolchain for leanprover/lean4#9587

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

* Bump batteries

* Fix warning

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

* update test

* fix test

* fix merge?

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

* fix

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

* deprecations

* shake --fix

* fix imports

* remove Shake again?

* chore: adaptations for nightly-2025-08-04 (#26)

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

* Update lean-toolchain for leanprover/lean4#9084

* Update Batteries branch for testing leanprover-community/batteries#1306

* chore: adaptation to batteries#1306

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

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

* chore: update 'unknown identifier' test ouputs

* chore: update 'tactic failed' test outputs

* fix(scripts/create-adaptation-pr): improve find_remote (leanprover-community#26974)

The old one was a syntax error and would've found a `mathlib4-nightly-testing` remote as a `mathlib4` remote (due to substring); this one is a bit more strict and works at least on my machine :-)

* Merge master into nightly-testing

* Update lean-toolchain for leanprover/lean4#9423

* Update lean-toolchain for leanprover/lean4#9424

* chore: update tactic error test outputs

* Update lean-toolchain for leanprover/lean4#9423

* Merge master into nightly-testing

* Merge master into nightly-testing

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

* fixes

* fixes

* Merge master into nightly-testing

* Merge master into nightly-testing

* fix

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

* Merge master into nightly-testing

* adaptation notes for breakages in batteries

* update Cache

* fix

* lake update

* Merge master into nightly-testing

* deprecation

* fixes for Shake

* shake

* shake --update

* fix noisy build detection

* Merge master into nightly-testing

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

* Merge master into nightly-testing

* Merge master into nightly-testing

* fix

* revert commenting out

* fix noisy test

* Merge master into nightly-testing

* Merge master into nightly-testing

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

* Merge master into nightly-testing

* Merge master into nightly-testing

* Merge master into nightly-testing

* fixes for changes to Lean.Grind.NatModule

* oops

* Merge master into nightly-testing

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

* fix

* fix(scripts/create-adaption-pr.sh): fetch `master` if necessary (leanprover-community#27293)

Makes sure that `master` is available, in particular when the remote has been automatically added.

* chore: make create-adapation-pr.sh robust to running on nightly-testing fork (leanprover-community#27411)

cf recent failures at [#nightly-testing > Mathlib bump branch reminders @ 💬](https://leanprover.zulipchat.com/#narrow/channel/428973-nightly-testing/topic/Mathlib.20bump.20branch.20reminders/near/530460702)

* fix da script

* `lake exe mk_all`

* hmm let's see what breaks

* not these

* hmm..?

* hmm this one as well

* more changes that turn out to be necessary

* Restore files from testing/nightly-testing

* Restore files from testing/nightly-testing

* Restore files from testing/nightly-testing

* Revert accidentals

* `mk_all`

* fix `@[to_additive]`

* Restore files from testing/nightly-testing

* re-add changes

* restore some more stuff carefully

* these

* try fix things

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

* fix by restoring mathlib change

* restore master versions of mis-merged files

* restore master versions of mis-merged files

* fix merge

* comment out with adaptation note

* huh?

* lake update

* lake update

* fix import

* shaking

* shaking

* shaking

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

* lake update

* mk_all

* fix merges

* more missed changes (#18)

* Merge master into nightly-testing

* feat: establish examples of harmonic functions (leanprover-community#26844)

If `f : ℂ → F` is complex-differentiable, then show that `f` is harmonic. If `F = ℂ`, then so is its real part, imaginary part, and complex conjugate. If `f` has no zero, then `log ‖f‖` is harmonic.

This material is used in [Project VD](https://github.com/kebekus/ProjectVD), which aims to formalize Value Distribution Theory for meromorphic functions on the complex plane. It is one of the ingredients in the proof of Jensen's Formula in complex analysis.

* chore: replace `Monoid.IsTorsionFree` with `IsMulTorsionFree` (leanprover-community#24311)

From Toric

* fix tests

---------

Co-authored-by: Stefan Kebekus <kebekus@users.noreply.github.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

* fix test (#19)

* last fix I swear

* unnecessary duplicate imports

* these are actual unused imports (because of core changes?)

* test fix

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

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

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

* grind lemma

* more

* chore(Cache): enable FRO cache (#17)

* chore: revert "enable FRO cache (#17)"

This reverts commit 1da13d9.

* Restore regression

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

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

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

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

* adaptation notes

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

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

* fix; bad merge?

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

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

* deprecation

* Update lean-toolchain for leanprover/lean4#9633

* chore: update test error message outputs

* adaptation note about Xor'

* shake --update

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

* fix

* fix test output

* fix test output

* fix test output

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

* fix

* Update lean-toolchain for leanprover/lean4#9587

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

* Bump batteries

* Fix warning

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

* update test

* fix test

* fix merge?

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

* fix

---------

Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: F. G. Dorais <fgdorais@gmail.com>
Co-authored-by: Joseph Rotella <7482866+jrr6@users.noreply.github.com>
Co-authored-by: Rob23oba <robin.arnez@web.de>
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: github-actions <github-actions@github.com>
Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>
Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com>
Co-authored-by: Stefan Kebekus <kebekus@users.noreply.github.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Co-authored-by: Mac Malone <tydeu@hatpress.net>
Co-authored-by: Mac Malone <mac@lean-fro.org>
Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>

* remove Shake

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

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

* Update lean-toolchain for leanprover/lean4#9084

* Update Batteries branch for testing leanprover-community/batteries#1306

* chore: adaptation to batteries#1306

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

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

* chore: update 'unknown identifier' test ouputs

* chore: update 'tactic failed' test outputs

* fix(scripts/create-adaptation-pr): improve find_remote (leanprover-community#26974)

The old one was a syntax error and would've found a `mathlib4-nightly-testing` remote as a `mathlib4` remote (due to substring); this one is a bit more strict and works at least on my machine :-)

* Merge master into nightly-testing

* Update lean-toolchain for leanprover/lean4#9423

* Update lean-toolchain for leanprover/lean4#9424

* chore: update tactic error test outputs

* Update lean-toolchain for leanprover/lean4#9423

* Merge master into nightly-testing

* Merge master into nightly-testing

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

* fixes

* fixes

* Merge master into nightly-testing

* Merge master into nightly-testing

* fix

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

* Merge master into nightly-testing

* adaptation notes for breakages in batteries

* update Cache

* fix

* lake update

* Merge master into nightly-testing

* deprecation

* fixes for Shake

* shake

* shake --update

* fix noisy build detection

* Merge master into nightly-testing

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

* Merge master into nightly-testing

* Merge master into nightly-testing

* fix

* revert commenting out

* fix noisy test

* Merge master into nightly-testing

* Merge master into nightly-testing

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

* Merge master into nightly-testing

* Merge master into nightly-testing

* Merge master into nightly-testing

* fixes for changes to Lean.Grind.NatModule

* oops

* Merge master into nightly-testing

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

* fix

* fix(scripts/create-adaption-pr.sh): fetch `master` if necessary (leanprover-community#27293)

Makes sure that `master` is available, in particular when the remote has been automatically added.

* chore: make create-adapation-pr.sh robust to running on nightly-testing fork (leanprover-community#27411)

cf recent failures at [#nightly-testing > Mathlib bump branch reminders @ 💬](https://leanprover.zulipchat.com/#narrow/channel/428973-nightly-testing/topic/Mathlib.20bump.20branch.20reminders/near/530460702)

* fix da script

* `lake exe mk_all`

* hmm let's see what breaks

* not these

* hmm..?

* hmm this one as well

* more changes that turn out to be necessary

* Restore files from testing/nightly-testing

* Restore files from testing/nightly-testing

* Restore files from testing/nightly-testing

* Revert accidentals

* `mk_all`

* fix `@[to_additive]`

* Restore files from testing/nightly-testing

* re-add changes

* restore some more stuff carefully

* these

* try fix things

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

* fix by restoring mathlib change

* restore master versions of mis-merged files

* restore master versions of mis-merged files

* fix merge

* comment out with adaptation note

* huh?

* lake update

* lake update

* fix import

* shaking

* shaking

* shaking

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

* lake update

* mk_all

* fix merges

* more missed changes (#18)

* Merge master into nightly-testing

* feat: establish examples of harmonic functions (leanprover-community#26844)

If `f : ℂ → F` is complex-differentiable, then show that `f` is harmonic. If `F = ℂ`, then so is its real part, imaginary part, and complex conjugate. If `f` has no zero, then `log ‖f‖` is harmonic.

This material is used in [Project VD](https://github.com/kebekus/ProjectVD), which aims to formalize Value Distribution Theory for meromorphic functions on the complex plane. It is one of the ingredients in the proof of Jensen's Formula in complex analysis.

* chore: replace `Monoid.IsTorsionFree` with `IsMulTorsionFree` (leanprover-community#24311)

From Toric

* fix tests

---------

Co-authored-by: Stefan Kebekus <kebekus@users.noreply.github.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

* fix test (#19)

* last fix I swear

* unnecessary duplicate imports

* these are actual unused imports (because of core changes?)

* test fix

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

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

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

* grind lemma

* more

* chore(Cache): enable FRO cache (#17)

* chore: revert "enable FRO cache (#17)"

This reverts commit 1da13d9.

* Restore regression

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

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

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

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

* adaptation notes

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

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

* fix; bad merge?

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

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

* deprecation

* Update lean-toolchain for leanprover/lean4#9633

* chore: update test error message outputs

* adaptation note about Xor'

* shake --update

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

* fix

* fix test output

* fix test output

* fix test output

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

* fix

* Update lean-toolchain for leanprover/lean4#9587

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

* Bump batteries

* Fix warning

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

* update test

* fix test

* fix merge?

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

* fix

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

* deprecations

* shake --fix

* fix imports

* remove Shake again?

---------

Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: F. G. Dorais <fgdorais@gmail.com>
Co-authored-by: Joseph Rotella <7482866+jrr6@users.noreply.github.com>
Co-authored-by: Rob23oba <robin.arnez@web.de>
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: github-actions <github-actions@github.com>
Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>
Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com>
Co-authored-by: Stefan Kebekus <kebekus@users.noreply.github.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Co-authored-by: Mac Malone <tydeu@hatpress.net>
Co-authored-by: Mac Malone <mac@lean-fro.org>
Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>

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

* fix

* chore: adaptations for nightly-2025-08-06 (#29)

* Update lean-toolchain for leanprover/lean4#9084

* Update Batteries branch for testing leanprover-community/batteries#1306

* chore: adaptation to batteries#1306

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

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

* chore: update 'unknown identifier' test ouputs

* chore: update 'tactic failed' test outputs

* fix(scripts/create-adaptation-pr): improve find_remote (leanprover-community#26974)

The old one was a syntax error and would've found a `mathlib4-nightly-testing` remote as a `mathlib4` remote (due to substring); this one is a bit more strict and works at least on my machine :-)

* Merge master into nightly-testing

* Update lean-toolchain for leanprover/lean4#9423

* Update lean-toolchain for leanprover/lean4#9424

* chore: update tactic error test outputs

* Update lean-toolchain for leanprover/lean4#9423

* Merge master into nightly-testing

* Merge master into nightly-testing

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

* fixes

* fixes

* Merge master into nightly-testing

* Merge master into nightly-testing

* fix

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

* Merge master into nightly-testing

* adaptation notes for breakages in batteries

* update Cache

* fix

* lake update

* Merge master into nightly-testing

* deprecation

* fixes for Shake

* shake

* shake --update

* fix noisy build detection

* Merge master into nightly-testing

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

* Merge master into nightly-testing

* Merge master into nightly-testing

* fix

* revert commenting out

* fix noisy test

* Merge master into nightly-testing

* Merge master into nightly-testing

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

* Merge master into nightly-testing

* Merge master into nightly-testing

* Merge master into nightly-testing

* fixes for changes to Lean.Grind.NatModule

* oops

* Merge master into nightly-testing

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

* fix

* fix(scripts/create-adaption-pr.sh): fetch `master` if necessary (leanprover-community#27293)

Makes sure that `master` is available, in particular when the remote has been automatically added.

* chore: make create-adapation-pr.sh robust to running on nightly-testing fork (leanprover-community#27411)

cf recent failures at [#nightly-testing > Mathlib bump branch reminders @ 💬](https://leanprover.zulipchat.com/#narrow/channel/428973-nightly-testing/topic/Mathlib.20bump.20branch.20reminders/near/530460702)

* fix da script

* `lake exe mk_all`

* hmm let's see what breaks

* not these

* hmm..?

* hmm this one as well

* more changes that turn out to be necessary

* Restore files from testing/nightly-testing

* Restore files from testing/nightly-testing

* Restore files from testing/nightly-testing

* Revert accidentals

* `mk_all`

* fix `@[to_additive]`

* Restore files from testing/nightly-testing

* re-add changes

* restore some more stuff carefully

* these

* try fix things

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

* fix by restoring mathlib change

* restore master versions of mis-merged files

* restore master versions of mis-merged files

* fix merge

* comment out with adaptation note

* huh?

* lake update

* lake update

* fix import

* shaking

* shaking

* shaking

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

* lake update

* mk_all

* fix merges

* more missed changes (#18)

* Merge master into nightly-testing

* feat: establish examples of harmonic functions (leanprover-community#26844)

If `f : ℂ → F` is complex-differentiable, then show that `f` is harmonic. If `F = ℂ`, then so is its real part, imaginary part, and complex conjugate. If `f` has no zero, then `log ‖f‖` is harmonic.

This material is used in [Project VD](https://github.com/kebekus/ProjectVD), which aims to formalize Value Distribution Theory for meromorphic functions on the complex plane. It is one of the ingredients in the proof of Jensen's Formula in complex analysis.

* chore: replace `Monoid.IsTorsionFree` with `IsMulTorsionFree` (leanprover-community#24311)

From Toric

* fix tests

---------

Co-authored-by: Stefan Kebekus <kebekus@users.noreply.github.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

* fix test (#19)

* last fix I swear

* unnecessary duplicate imports

* these are actual unused imports (because of core changes?)

* test fix

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

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

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

* grind lemma

* more

* chore(Cache): enable FRO cache (#17)

* chore: revert "enable FRO cache (#17)"

This reverts commit 1da13d9.

* Restore regression

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

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

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

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

* adaptation notes

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

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

* fix; bad merge?

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

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

* deprecation

* Update lean-toolchain for leanprover/lean4#9633

* chore: update test error message outputs

* adaptation note about Xor'

* shake --update

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

* fix

* fix test output

* fix test output

* fix test output

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

* fix

* Update lean-toolchain for leanprover/lean4#9587

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

* Bump batteries

* Fix warning

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

* update test

* fix test

* fix merge?

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

* fix

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

* deprecations

* shake --fix

* fix imports

* remove Shake again?

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

---------

Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: F. G. Dorais <fgdorais@gmail.com>
Co-authored-by: Joseph Rotella <7482866+jrr6@users.noreply.github.com>
Co-authored-by: Rob23oba <robin.arnez@web.de>
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: github-actions <github-actions@github.com>
Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>
Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com>
Co-authored-by: Stefan Kebekus <kebekus@users.noreply.github.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Co-authored-by: Mac Malone <tydeu@hatpress.net>
Co-authored-by: Mac Malone <mac@lean-fro.org>
Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>

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

* lake update aesop

* lake update aesop

* deprecations

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

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

* Update lean-toolchain for leanprover/lean4#9800

* Update lean-toolchain for leanprover/lean4#9800

* Update lean-toolchain for leanprover/lean4#9800

* addressing some cases of mathlib4#380

* fix tests

* Update lean-toolchain for leanprover/lean4#9800

* Update lean-toolchain for leanprover/lean4#9800

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

* fix (all?) `protected` regressions

* Update lean-toolchain for leanprover/lean4#9800

* fix

* adaptation note?

* noncomputable

* revert grind proof

* remove upstreamed

* fixes

* feat: better statement of flip_map_app

* sad adaptation note

* update adaptation note

* fix merge

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

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

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

* fixes

* fix

* fix toolchain?

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

* use legacy lemma for now

* revert bad changes

* upstream LE/LT (Subtype p) instances

* chore(Cache): use FRO cache (v2) (#30)

* chore(Cache): enable FRO cache

* feat: only print "packing" when actually packing

* feat: always prefix with repo in FRO cache

* fix

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

* chore: trigger rebuild to test cache

* chore: use `cache put!` in CI to debug

* shake --update

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

* empty

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

* Revert "chore: use `cache put!` in CI to debug"

This reverts commit 7c6202b.

* redundant grind warnings

* revert leanprover-community#28272: add back grind proofs

* fix test

* chore: adaptations for nightly-2025-08-13

* fixes

* restore test

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

* adaptation note about grind regression

* fix tests

* update test output

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

* bump proofwidgets

* bump proofwidgets

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

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

* Apply suggestions from code review

---------

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: Sebastian Ullrich <sebasti@nullri.ch>
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: F. G. Dorais <fgdorais@gmail.com>
Co-authored-by: Joseph Rotella <7482866+jrr6@users.noreply.github.com>
Co-authored-by: Rob23oba <robin.arnez@web.de>
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>
Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com>
Co-authored-by: Stefan Kebekus <kebekus@users.noreply.github.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Co-authored-by: Mac Malone <tydeu@hatpress.net>
Co-authored-by: Mac Malone <mac@lean-fro.org>
Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com>

These proofs (and probably others) are causing CI failures. We can revert this after leanprover/lean4#9825 is fixed.

cf. [#mathlib4 > Failing CI @ 💬](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Failing.20CI/near/533684295)

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

* deprecations

* shake --fix

* fix imports

* remove Shake again?

* chore: adaptations for nightly-2025-08-04 (#26)

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

* Update lean-toolchain for leanprover/lean4#9084

* Update Batteries branch for testing leanprover-community/batteries#1306

* chore: adaptation to batteries#1306

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

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

* chore: update 'unknown identifier' test ouputs

* chore: update 'tactic failed' test outputs

* fix(scripts/create-adaptation-pr): improve find_remote (leanprover-community#26974)

The old one was a syntax error and would've found a `mathlib4-nightly-testing` remote as a `mathlib4` remote (due to substring); this one is a bit more strict and works at least on my machine :-)

* Merge master into nightly-testing

* Update lean-toolchain for leanprover/lean4#9423

* Update lean-toolchain for leanprover/lean4#9424

* chore: update tactic error test outputs

* Update lean-toolchain for leanprover/lean4#9423

* Merge master into nightly-testing

* Merge master into nightly-testing

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

* fixes

* fixes

* Merge master into nightly-testing

* Merge master into nightly-testing

* fix

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

* Merge master into nightly-testing

* adaptation notes for breakages in batteries

* update Cache

* fix

* lake update

* Merge master into nightly-testing

* deprecation

* fixes for Shake

* shake

* shake --update

* fix noisy build detection

* Merge master into nightly-testing

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

* Merge master into nightly-testing

* Merge master into nightly-testing

* fix

* revert commenting out

* fix noisy test

* Merge master into nightly-testing

* Merge master into nightly-testing

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

* Merge master into nightly-testing

* Merge master into nightly-testing

* Merge master into nightly-testing

* fixes for changes to Lean.Grind.NatModule

* oops

* Merge master into nightly-testing

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

* fix

* fix(scripts/create-adaption-pr.sh): fetch `master` if necessary (leanprover-community#27293)

Makes sure that `master` is available, in particular when the remote has been automatically added.

* chore: make create-adapation-pr.sh robust to running on nightly-testing fork (leanprover-community#27411)

cf recent failures at [#nightly-testing > Mathlib bump branch reminders @ 💬](https://leanprover.zulipchat.com/#narrow/channel/428973-nightly-testing/topic/Mathlib.20bump.20branch.20reminders/near/530460702)

* fix da script

* `lake exe mk_all`

* hmm let's see what breaks

* not these

* hmm..?

* hmm this one as well

* more changes that turn out to be necessary

* Restore files from testing/nightly-testing

* Restore files from testing/nightly-testing

* Restore files from testing/nightly-testing

* Revert accidentals

* `mk_all`

* fix `@[to_additive]`

* Restore files from testing/nightly-testing

* re-add changes

* restore some more stuff carefully

* these

* try fix things

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

* fix by restoring mathlib change

* restore master versions of mis-merged files

* restore master versions of mis-merged files

* fix merge

* comment out with adaptation note

* huh?

* lake update

* lake update

* fix import

* shaking

* shaking

* shaking

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

* lake update

* mk_all

* fix merges

* more missed changes (#18)

* Merge master into nightly-testing

* feat: establish examples of harmonic functions (leanprover-community#26844)

If `f : ℂ → F` is complex-differentiable, then show that `f` is harmonic. If `F = ℂ`, then so is its real part, imaginary part, and complex conjugate. If `f` has no zero, then `log ‖f‖` is harmonic.

This material is used in [Project VD](https://github.com/kebekus/ProjectVD), which aims to formalize Value Distribution Theory for meromorphic functions on the complex plane. It is one of the ingredients in the proof of Jensen's Formula in complex analysis.

* chore: replace `Monoid.IsTorsionFree` with `IsMulTorsionFree` (leanprover-community#24311)

From Toric

* fix tests

---------

Co-authored-by: Stefan Kebekus <kebekus@users.noreply.github.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

* fix test (#19)

* last fix I swear

* unnecessary duplicate imports

* these are actual unused imports (because of core changes?)

* test fix

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

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

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

* grind lemma

* more

* chore(Cache): enable FRO cache (#17)

* chore: revert "enable FRO cache (#17)"

This reverts commit 1da13d9.

* Restore regression

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

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

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

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

* adaptation notes

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

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

* fix; bad merge?

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

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

* deprecation

* Update lean-toolchain for leanprover/lean4#9633

* chore: update test error message outputs

* adaptation note about Xor'

* shake --update

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

* fix

* fix test output

* fix test output

* fix test output

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

* fix

* Update lean-toolchain for leanprover/lean4#9587

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

* Bump batteries

* Fix warning

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

* update test

* fix test

* fix merge?

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

* fix

---------

Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: F. G. Dorais <fgdorais@gmail.com>
Co-authored-by: Joseph Rotella <7482866+jrr6@users.noreply.github.com>
Co-authored-by: Rob23oba <robin.arnez@web.de>
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: github-actions <github-actions@github.com>
Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>
Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com>
Co-authored-by: Stefan Kebekus <kebekus@users.noreply.github.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Co-authored-by: Mac Malone <tydeu@hatpress.net>
Co-authored-by: Mac Malone <mac@lean-fro.org>
Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>

* remove Shake

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

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

* Update lean-toolchain for leanprover/lean4#9084

* Update Batteries branch for testing leanprover-community/batteries#1306

* chore: adaptation to batteries#1306

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

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

* chore: update 'unknown identifier' test ouputs

* chore: update 'tactic failed' test outputs

* fix(scripts/create-adaptation-pr): improve find_remote (leanprover-community#26974)

The old one was a syntax error and would've found a `mathlib4-nightly-testing` remote as a `mathlib4` remote (due to substring); this one is a bit more strict and works at least on my machine :-)

* Merge master into nightly-testing

* Update lean-toolchain for leanprover/lean4#9423

* Update lean-toolchain for leanprover/lean4#9424

* chore: update tactic error test outputs

* Update lean-toolchain for leanprover/lean4#9423

* Merge master into nightly-testing

* Merge master into nightly-testing

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

* fixes

* fixes

* Merge master into nightly-testing

* Merge master into nightly-testing

* fix

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

* Merge master into nightly-testing

* adaptation notes for breakages in batteries

* update Cache

* fix

* lake update

* Merge master into nightly-testing

* deprecation

* fixes for Shake

* shake

* shake --update

* fix noisy build detection

* Merge master into nightly-testing

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

* Merge master into nightly-testing

* Merge master into nightly-testing

* fix

* revert commenting out

* fix noisy test

* Merge master into nightly-testing

* Merge master into nightly-testing

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

* Merge master into nightly-testing

* Merge master into nightly-testing

* Merge master into nightly-testing

* fixes for changes to Lean.Grind.NatModule

* oops

* Merge master into nightly-testing

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

* fix

* fix(scripts/create-adaption-pr.sh): fetch `master` if necessary (leanprover-community#27293)

Makes sure that `master` is available, in particular when the remote has been automatically added.

* chore: make create-adapation-pr.sh robust to running on nightly-testing fork (leanprover-community#27411)

cf recent failures at [#nightly-testing > Mathlib bump branch reminders @ 💬](https://leanprover.zulipchat.com/#narrow/channel/428973-nightly-testing/topic/Mathlib.20bump.20branch.20reminders/near/530460702)

* fix da script

* `lake exe mk_all`

* hmm let's see what breaks

* not these

* hmm..?

* hmm this one as well

* more changes that turn out to be necessary

* Restore files from testing/nightly-testing

* Restore files from testing/nightly-testing

* Restore files from testing/nightly-testing

* Revert accidentals

* `mk_all`

* fix `@[to_additive]`

* Restore files from testing/nightly-testing

* re-add changes

* restore some more stuff carefully

* these

* try fix things

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

* fix by restoring mathlib change

* restore master versions of mis-merged files

* restore master versions of mis-merged files

* fix merge

* comment out with adaptation note

* huh?

* lake update

* lake update

* fix import

* shaking

* shaking

* shaking

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

* lake update

* mk_all

* fix merges

* more missed changes (#18)

* Merge master into nightly-testing

* feat: establish examples of harmonic functions (leanprover-community#26844)

If `f : ℂ → F` is complex-differentiable, then show that `f` is harmonic. If `F = ℂ`, then so is its real part, imaginary part, and complex conjugate. If `f` has no zero, then `log ‖f‖` is harmonic.

This material is used in [Project VD](https://github.com/kebekus/ProjectVD), which aims to formalize Value Distribution Theory for meromorphic functions on the complex plane. It is one of the ingredients in the proof of Jensen's Formula in complex analysis.

* chore: replace `Monoid.IsTorsionFree` with `IsMulTorsionFree` (leanprover-community#24311)

From Toric

* fix tests

---------

Co-authored-by: Stefan Kebekus <kebekus@users.noreply.github.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

* fix test (#19)

* last fix I swear

* unnecessary duplicate imports

* these are actual unused imports (because of core changes?)

* test fix

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

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

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

* grind lemma

* more

* chore(Cache): enable FRO cache (#17)

* chore: revert "enable FRO cache (#17)"

This reverts commit 1da13d9.

* Restore regression

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

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

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

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

* adaptation notes

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

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

* fix; bad merge?

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

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

* deprecation

* Update lean-toolchain for leanprover/lean4#9633

* chore: update test error message outputs

* adaptation note about Xor'

* shake --update

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

* fix

* fix test output

* fix test output

* fix test output

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

* fix

* Update lean-toolchain for leanprover/lean4#9587

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

* Bump batteries

* Fix warning

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

* update test

* fix test

* fix merge?

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

* fix

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

* deprecations

* shake --fix

* fix imports

* remove Shake again?

---------

Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: F. G. Dorais <fgdorais@gmail.com>
Co-authored-by: Joseph Rotella <7482866+jrr6@users.noreply.github.com>
Co-authored-by: Rob23oba <robin.arnez@web.de>
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: github-actions <github-actions@github.com>
Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>
Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com>
Co-authored-by: Stefan Kebekus <kebekus@users.noreply.github.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Co-authored-by: Mac Malone <tydeu@hatpress.net>
Co-authored-by: Mac Malone <mac@lean-fro.org>
Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>

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

* fix

* chore: adaptations for nightly-2025-08-06 (#29)

* Update lean-toolchain for leanprover/lean4#9084

* Update Batteries branch for testing leanprover-community/batteries#1306

* chore: adaptation to batteries#1306

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

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

* chore: update 'unknown identifier' test ouputs

* chore: update 'tactic failed' test outputs

* fix(scripts/create-adaptation-pr): improve find_remote (leanprover-community#26974)

The old one was a syntax error and would've found a `mathlib4-nightly-testing` remote as a `mathlib4` remote (due to substring); this one is a bit more strict and works at least on my machine :-)

* Merge master into nightly-testing

* Update lean-toolchain for leanprover/lean4#9423

* Update lean-toolchain for leanprover/lean4#9424

* chore: update tactic error test outputs

* Update lean-toolchain for leanprover/lean4#9423

* Merge master into nightly-testing

* Merge master into nightly-testing

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

* fixes

* fixes

* Merge master into nightly-testing

* Merge master into nightly-testing

* fix

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

* Merge master into nightly-testing

* adaptation notes for breakages in batteries

* update Cache

* fix

* lake update

* Merge master into nightly-testing

* deprecation

* fixes for Shake

* shake

* shake --update

* fix noisy build detection

* Merge master into nightly-testing

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

* Merge master into nightly-testing

* Merge master into nightly-testing

* fix

* revert commenting out

* fix noisy test

* Merge master into nightly-testing

* Merge master into nightly-testing

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

* Merge master into nightly-testing

* Merge master into nightly-testing

* Merge master into nightly-testing

* fixes for changes to Lean.Grind.NatModule

* oops

* Merge master into nightly-testing

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

* fix

* fix(scripts/create-adaption-pr.sh): fetch `master` if necessary (leanprover-community#27293)

Makes sure that `master` is available, in particular when the remote has been automatically added.

* chore: make create-adapation-pr.sh robust to running on nightly-testing fork (leanprover-community#27411)

cf recent failures at [#nightly-testing > Mathlib bump branch reminders @ 💬](https://leanprover.zulipchat.com/#narrow/channel/428973-nightly-testing/topic/Mathlib.20bump.20branch.20reminders/near/530460702)

* fix da script

* `lake exe mk_all`

* hmm let's see what breaks

* not these

* hmm..?

* hmm this one as well

* more changes that turn out to be necessary

* Restore files from testing/nightly-testing

* Restore files from testing/nightly-testing

* Restore files from testing/nightly-testing

* Revert accidentals

* `mk_all`

* fix `@[to_additive]`

* Restore files from testing/nightly-testing

* re-add changes

* restore some more stuff carefully

* these

* try fix things

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

* fix by restoring mathlib change

* restore master versions of mis-merged files

* restore master versions of mis-merged files

* fix merge

* comment out with adaptation note

* huh?

* lake update

* lake update

* fix import

* shaking

* shaking

* shaking

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

* lake update

* mk_all

* fix merges

* more missed changes (#18)

* Merge master into nightly-testing

* feat: establish examples of harmonic functions (leanprover-community#26844)

If `f : ℂ → F` is complex-differentiable, then show that `f` is harmonic. If `F = ℂ`, then so is its real part, imaginary part, and complex conjugate. If `f` has no zero, then `log ‖f‖` is harmonic.

This material is used in [Project VD](https://github.com/kebekus/ProjectVD), which aims to formalize Value Distribution Theory for meromorphic functions on the complex plane. It is one of the ingredients in the proof of Jensen's Formula in complex analysis.

* chore: replace `Monoid.IsTorsionFree` with `IsMulTorsionFree` (leanprover-community#24311)

From Toric

* fix tests

---------

Co-authored-by: Stefan Kebekus <kebekus@users.noreply.github.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

* fix test (#19)

* last fix I swear

* unnecessary duplicate imports

* these are actual unused imports (because of core changes?)

* test fix

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

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

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

* grind lemma

* more

* chore(Cache): enable FRO cache (#17)

* chore: revert "enable FRO cache (#17)"

This reverts commit 1da13d9.

* Restore regression

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

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

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

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

* adaptation notes

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

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

* fix; bad merge?

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

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

* deprecation

* Update lean-toolchain for leanprover/lean4#9633

* chore: update test error message outputs

* adaptation note about Xor'

* shake --update

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

* fix

* fix test output

* fix test output

* fix test output

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

* fix

* Update lean-toolchain for leanprover/lean4#9587

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

* Bump batteries

* Fix warning

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

* update test

* fix test

* fix merge?

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

* fix

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

* deprecations

* shake --fix

* fix imports

* remove Shake again?

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

---------

Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: F. G. Dorais <fgdorais@gmail.com>
Co-authored-by: Joseph Rotella <7482866+jrr6@users.noreply.github.com>
Co-authored-by: Rob23oba <robin.arnez@web.de>
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: github-actions <github-actions@github.com>
Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>
Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com>
Co-authored-by: Stefan Kebekus <kebekus@users.noreply.github.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Co-authored-by: Mac Malone <tydeu@hatpress.net>
Co-authored-by: Mac Malone <mac@lean-fro.org>
Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>

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

* lake update aesop

* lake update aesop

* deprecations

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

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

* Update lean-toolchain for leanprover/lean4#9800

* Update lean-toolchain for leanprover/lean4#9800

* Update lean-toolchain for leanprover/lean4#9800

* addressing some cases of mathlib4#380

* fix tests

* Update lean-toolchain for leanprover/lean4#9800

* Update lean-toolchain for leanprover/lean4#9800

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

* fix (all?) `protected` regressions

* Update lean-toolchain for leanprover/lean4#9800

* fix

* adaptation note?

* noncomputable

* revert grind proof

* remove upstreamed

* fixes

* feat: better statement of flip_map_app

* sad adaptation note

* update adaptation note

* fix merge

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

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

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

* fixes

* fix

* fix toolchain?

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

* use legacy lemma for now

* revert bad changes

* upstream LE/LT (Subtype p) instances

* chore(Cache): use FRO cache (v2) (#30)

* chore(Cache): enable FRO cache

* feat: only print "packing" when actually packing

* feat: always prefix with repo in FRO cache

* fix

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

* chore: trigger rebuild to test cache

* chore: use `cache put!` in CI to debug

* shake --update

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

* empty

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

* Revert "chore: use `cache put!` in CI to debug"

This reverts commit 7c6202b.

* redundant grind warnings

* revert leanprover-community#28272: add back grind proofs

* fix test

* chore: adaptations for nightly-2025-08-13

* fixes

* restore test

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

* adaptation note about grind regression

* fix tests

* update test output

* feat: workflow for reporting `grind` regressions

This PR contains a (untested!) workflow that is supposed to build Mathlib with a few tactic analysis flags. It reports the results of these build steps to Zulip for the FRO (and in particular Kim).

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

* bump proofwidgets

* bump proofwidgets

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

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

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

* Update lean-toolchain for leanprover/lean4#9942

* Update lean-toolchain for leanprover/lean4#9942

* make `filter_upwards` more robust to side goals

* Update lean-toolchain for leanprover/lean4#9674

* simpler change to filter_upwards

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

* Apply suggestions from code review

* Use JS to generate uuid instead of uuidgen which appears not to be installed

* GH Problem Matcher wrapper doesn't like multiline arguments; wrap multiple steps instead.

* Hmm, maybe uuidgen exists and it was gh-problem-matcher that was the issue?

* Can we just `apt install` dependencies?

* Apparently Linux exposes uuids from the kernel. Nifty!

* Then we don't need to install uuidgen

* Try also implementing a docgen step for nightly testing

* Cut off the output after 9k bytes, otherwise Zulip complains

* Fixes

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

* Filter out the build progress lines.

* Switch `doc-gen4` version to "main", otherwise it complains there is no nightly-testing release.

* lake update

* cleanup imports

* Fix `git remote` complaining that `nightly-testing` already exists.

* Fix error message.

* fix tests

* shake --fix

* satisfy actionlint

* shellcheck

---------

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: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: F. G. Dorais <fgdorais@gmail.com>
Co-authored-by: Joseph Rotella <7482866+jrr6@users.noreply.github.com>
Co-authored-by: Rob23oba <robin.arnez@web.de>
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: github-actions <github-actions@github.com>
Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>
Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com>
Co-authored-by: Stefan Kebekus <kebekus@users.noreply.github.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Co-authored-by: Mac Malone <tydeu@hatpress.net>
Co-authored-by: Mac Malone <mac@lean-fro.org>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com>
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

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

* lake update aesop

* lake update aesop

* deprecations

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

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

* Update lean-toolchain for leanprover/lean4#9800

* Update lean-toolchain for leanprover/lean4#9800

* Update lean-toolchain for leanprover/lean4#9800

* addressing some cases of mathlib4#380

* fix tests

* Update lean-toolchain for leanprover/lean4#9800

* Update lean-toolchain for leanprover/lean4#9800

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

* fix (all?) `protected` regressions

* Update lean-toolchain for leanprover/lean4#9800

* fix

* adaptation note?

* noncomputable

* revert grind proof

* remove upstreamed

* fixes

* feat: better statement of flip_map_app

* sad adaptation note

* update adaptation note

* fix merge

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

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

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

* fixes

* fix

* fix toolchain?

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

* use legacy lemma for now

* revert bad changes

* upstream LE/LT (Subtype p) instances

* chore(Cache): use FRO cache (v2) (#30)

* chore(Cache): enable FRO cache

* feat: only print "packing" when actually packing

* feat: always prefix with repo in FRO cache

* fix

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

* chore: trigger rebuild to test cache

* chore: use `cache put!` in CI to debug

* shake --update

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

* empty

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

* Revert "chore: use `cache put!` in CI to debug"

This reverts commit 7c6202b.

* redundant grind warnings

* revert leanprover-community#28272: add back grind proofs

* fix test

* chore: adaptations for nightly-2025-08-13

* fixes

* restore test

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

* adaptation note about grind regression

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

* fix tests

* fix

* update test output

* feat: workflow for reporting `grind` regressions

This PR contains a (untested!) workflow that is supposed to build Mathlib with a few tactic analysis flags. It reports the results of these build steps to Zulip for the FRO (and in particular Kim).

* fix

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

* bump proofwidgets

* bump proofwidgets

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

* fix: namespace linter should not care about private names

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

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

* Update lean-toolchain for leanprover/lean4#9942

* Update lean-toolchain for leanprover/lean4#9915

* Update lean-toolchain for leanprover/lean4#9942

* make `filter_upwards` more robust to side goals

* Update lean-toolchain for leanprover/lean4#9674

* simpler change to filter_upwards

* fix

* fix test

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

* Update lean-toolchain for leanprover/lean4#9915

* Apply suggestions from code review

* Use JS to generate uuid instead of uuidgen which appears not to be installed

* GH Problem Matcher wrapper doesn't like multiline arguments; wrap multiple steps instead.

* Hmm, maybe uuidgen exists and it was gh-problem-matcher that was the issue?

* Can we just `apt install` dependencies?

* Apparently Linux exposes uuids from the kernel. Nifty!

* Then we don't need to install uuidgen

* Try also implementing a docgen step for nightly testing

* Cut off the output after 9k bytes, otherwise Zulip complains

* Fixes

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

* Update lean-toolchain for leanprover/lean4#9915

* Filter out the build progress lines.

* Switch `doc-gen4` version to "main", otherwise it complains there is no nightly-testing release.

* Update lean-toolchain for leanprover/lean4#9915

* lake update

* cleanup imports

* Fix `git remote` complaining that `nightly-testing` already exists.

* Fix error message.

* Update lean-toolchain for leanprover/lean4#9915

* fix tests

* shake --fix

* fix says

* .

* says

* chore: `curl --retry-all-errors` in `cache get`

* remove says

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

* Drop more noise from the grind report.

* lake update

* fix

* fix tests

* manual shake

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

* satisfy actionlint

* shellcheck

---------

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: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: github-actions <github-actions@github.com>
Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Co-authored-by: Mac Malone <tydeu@hatpress.net>
Co-authored-by: Mac Malone <mac@lean-fro.org>
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>
Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com>
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

* lake update aesop

* lake update aesop

* deprecations

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

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

* Update lean-toolchain for leanprover/lean4#9800

* Update lean-toolchain for leanprover/lean4#9800

* Update lean-toolchain for leanprover/lean4#9800

* addressing some cases of mathlib4#380

* fix tests

* Update lean-toolchain for leanprover/lean4#9800

* Update lean-toolchain for leanprover/lean4#9800

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

* fix (all?) `protected` regressions

* Update lean-toolchain for leanprover/lean4#9800

* fix

* adaptation note?

* noncomputable

* revert grind proof

* remove upstreamed

* fixes

* feat: better statement of flip_map_app

* sad adaptation note

* update adaptation note

* fix merge

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

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

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

* fixes

* fix

* fix toolchain?

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

* use legacy lemma for now

* revert bad changes

* upstream LE/LT (Subtype p) instances

* chore(Cache): use FRO cache (v2) (#30)

* chore(Cache): enable FRO cache

* feat: only print "packing" when actually packing

* feat: always prefix with repo in FRO cache

* fix

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

* chore: trigger rebuild to test cache

* chore: use `cache put!` in CI to debug

* shake --update

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

* empty

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

* Revert "chore: use `cache put!` in CI to debug"

This reverts commit 7c6202b.

* redundant grind warnings

* revert leanprover-community#28272: add back grind proofs

* fix test

* chore: adaptations for nightly-2025-08-13

* fixes

* restore test

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

* adaptation note about grind regression

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

* fix tests

* fix

* update test output

* feat: workflow for reporting `grind` regressions

This PR contains a (untested!) workflow that is supposed to build Mathlib with a few tactic analysis flags. It reports the results of these build steps to Zulip for the FRO (and in particular Kim).

* fix

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

* bump proofwidgets

* bump proofwidgets

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

* fix: namespace linter should not care about private names

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

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

* Update lean-toolchain for leanprover/lean4#9942

* Update lean-toolchain for leanprover/lean4#9915

* Update lean-toolchain for leanprover/lean4#9942

* make `filter_upwards` more robust to side goals

* Update lean-toolchain for leanprover/lean4#9674

* simpler change to filter_upwards

* fix

* fix test

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

* Update lean-toolchain for leanprover/lean4#9915

* Apply suggestions from code review

* Use JS to generate uuid instead of uuidgen which appears not to be installed

* GH Problem Matcher wrapper doesn't like multiline arguments; wrap multiple steps instead.

* Hmm, maybe uuidgen exists and it was gh-problem-matcher that was the issue?

* Can we just `apt install` dependencies?

* Apparently Linux exposes uuids from the kernel. Nifty!

* Then we don't need to install uuidgen

* Try also implementing a docgen step for nightly testing

* Cut off the output after 9k bytes, otherwise Zulip complains

* Fixes

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

* Update lean-toolchain for leanprover/lean4#9915

* Filter out the build progress lines.

* Switch `doc-gen4` version to "main", otherwise it complains there is no nightly-testing release.

* Update lean-toolchain for leanprover/lean4#9915

* lake update

* cleanup imports

* Fix `git remote` complaining that `nightly-testing` already exists.

* Fix error message.

* Update lean-toolchain for leanprover/lean4#9915

* fix tests

* shake --fix

* fix says

* .

* says

* chore: `curl --retry-all-errors` in `cache get`

* remove says

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

* Drop more noise from the grind report.

* lake update

* fix

* fix tests

* manual shake

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

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

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

* satisfy actionlint

* shellcheck

---------

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: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: github-actions <github-actions@github.com>
Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Co-authored-by: Mac Malone <tydeu@hatpress.net>
Co-authored-by: Mac Malone <mac@lean-fro.org>
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>
Co-authored-by: Kim Morrison <477956+kim-em@users.noreply.github.com>
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>

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

* fixes

* fix

* fix toolchain?

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

* use legacy lemma for now

* revert bad changes

* upstream LE/LT (Subtype p) instances

* chore(Cache): use FRO cache (v2) (#30)

* chore(Cache): enable FRO cache

* feat: only print "packing" when actually packing

* feat: always prefix with repo in FRO cache

* fix

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

* chore: trigger rebuild to test cache

* chore: use `cache put!` in CI to debug

* shake --update

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

* empty

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

* Revert "chore: use `cache put!` in CI to debug"

This reverts commit 7c6202b.

* redundant grind warnings

* revert leanprover-community#28272: add back grind proofs

* fix test

* chore: adaptations for nightly-2025-08-13

* fixes

* restore test

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

* adaptation note about grind regression

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

* fix tests

* fix

* update test output

* feat: workflow for reporting `grind` regressions

This PR contains a (untested!) workflow that is supposed to build Mathlib with a few tactic analysis flags. It reports the results of these build steps to Zulip for the FRO (and in particular Kim).

* fix

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

* bump proofwidgets

* bump proofwidgets

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

* fix: namespace linter should not care about private names

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

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

* Update lean-toolchain for leanprover/lean4#9942

* Update lean-toolchain for leanprover/lean4#9915

* Update lean-toolchain for leanprover/lean4#9942

* make `filter_upwards` more robust to side goals

* Update lean-toolchain for leanprover/lean4#9674

* simpler change to filter_upwards

* fix

* fix test

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

* Update lean-toolchain for leanprover/lean4#9915

* Apply suggestions from code review

* Use JS to generate uuid instead of uuidgen which appears not to be installed

* GH Problem Matcher wrapper doesn't like multiline arguments; wrap multiple steps instead.

* Hmm, maybe uuidgen exists and it was gh-problem-matcher that was the issue?

* Can we just `apt install` dependencies?

* Apparently Linux exposes uuids from the kernel. Nifty!

* Then we don't need to install uuidgen

* Try also implementing a docgen step for nightly testing

* Cut off the output after 9k bytes, otherwise Zulip complains

* Fixes

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

* Update lean-toolchain for leanprover/lean4#9915

* Filter out the build progress lines.

* Switch `doc-gen4` version to "main", otherwise it complains there is no nightly-testing release.

* Update lean-toolchain for leanprover/lean4#9915

* lake update

* cleanup imports

* Fix `git remote` complaining that `nightly-testing` already exists.

* Fix error message.

* Update lean-toolchain for leanprover/lean4#9915

* fix tests

* shake --fix

* fix says

* .

* says

* chore: `curl --retry-all-errors` in `cache get`

* remove says

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

* Drop more noise from the grind report.

* lake update

* fix

* fix tests

* manual shake

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

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

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

* feat: create `nightly-testing-daily` and `nightly-testing-green` branches

These two branches track the `nightly-testing-YYYY-MM-DD` tags and the latest successfully built `nightly-testing` commit, respectively. These can then be used for other CI actions such as tests that run every night.

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

* Switch the workflows over to nightly-testing-green branch

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

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

* satisfy actionlint

* shellcheck

* fix

* fix

* fix for nightly-2025-08-24 (#42)

* fix

* please rebuild yourself

* maybe that works?

* fix

* rat fixes

* fixes

* fixes

* fix

* .'

* fix

* not there yet

* comment out Int.shiftLeft_add'

* Revert "comment out Int.shiftLeft_add'"

This reverts commit b33c9d7.

* fix proof

* change Polynomial.eval signature

* workaround for initialization order issue

* fixes

* fix

* fix message

* Actually import the linters we want to run.

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

* remove upstream `Rat` material

* fix `sigmaProdDistrib`

* more `Rat` fixes

* `Rat.inv_def'` -> `Rat.inv_def`

* fixes

* comment out `rw_search` tests

* small test fix

* shake --fix

* Revert

---------

Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Co-authored-by: Mac Malone <tydeu@hatpress.net>
Co-authored-by: github-actions <github-actions@github.com>
Co-authored-by: Mac Malone <mac@lean-fro.org>
Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: Bryan Gin-ge Chen <bryangingechen@gmail.com>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>
Co-authored-by: Rob23oba <152706811+Rob23oba@users.noreply.github.com>
Co-authored-by: Rob23oba <robin.arnez@web.de>