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

The new delta deriving handler from leanprover/lean4#9800 makes it possible to address most of issue #380. There are still some cases that are not handled:
- Some definitions are abbreviations, so there is no point in deriving instances, since they already inherit instances. Plus, adding instances to abbreviations adds intances to the unfolded abbreviation, which might not be wanted.
- Deriving `Functor.Full` and `Functor.Faithful` often gives the wrong instance. For example, with `Skeleton` and `fromSkeleton`, the derived instances are in terms of `InducedCategory`, not `Skeleton. It might not ever be possible to derive instances in this situation.

The new delta deriving handler from leanprover/lean4#9800 makes it possible to address most of issue #380. There are still some cases that are not handled:
- Some definitions are abbreviations, so there is no point in deriving instances, since they already inherit instances. Plus, adding instances to abbreviations adds intances to the unfolded abbreviation, which might not be wanted.
- Deriving `Functor.Full` and `Functor.Faithful` often gives the wrong instance. For example, with `Skeleton` and `fromSkeleton`, the derived instances are in terms of `InducedCategory`, not `Skeleton`. It might not ever be possible to derive instances in this situation.

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

…community#28498)

The new delta deriving handler from leanprover/lean4#9800 makes it possible to address most of issue leanprover-community#380. There are still some cases that are not handled:
- Some definitions are abbreviations, so there is no point in deriving instances, since they already inherit instances. Plus, adding instances to abbreviations adds intances to the unfolded abbreviation, which might not be wanted.
- Deriving `Functor.Full` and `Functor.Faithful` often gives the wrong instance. For example, with `Skeleton` and `fromSkeleton`, the derived instances are in terms of `InducedCategory`, not `Skeleton`. It might not ever be possible to derive instances in this situation.

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

…community#28498)

The new delta deriving handler from leanprover/lean4#9800 makes it possible to address most of issue leanprover-community#380. There are still some cases that are not handled:
- Some definitions are abbreviations, so there is no point in deriving instances, since they already inherit instances. Plus, adding instances to abbreviations adds intances to the unfolded abbreviation, which might not be wanted.
- Deriving `Functor.Full` and `Functor.Faithful` often gives the wrong instance. For example, with `Skeleton` and `fromSkeleton`, the derived instances are in terms of `InducedCategory`, not `Skeleton`. It might not ever be possible to derive instances in this situation.