* 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>

* 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>

* 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>

* 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>

* 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>