Skip to content

fix: replace bad simp lemmas for Id #7352

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Merged
kim-em merged 7 commits into from
May 22, 2025
Merged

fix: replace bad simp lemmas for Id #7352

kim-em merged 7 commits into from
May 22, 2025

Conversation

@eric-wieser
Copy link
Contributor

@eric-wieser eric-wieser commented Mar 5, 2025 •
edited
Loading

This PR reworks the simp set around the Id monad, to not elide or unfold pure and Id.run

In particular, it stops encoding the "defeq abuse" of Id X = X in the statements of theorems, instead using Id.run and pure to pass back and forth between these two spellings. Often when writing these with pure, they generalize to other lawful monads; though such changes were split off to other PRs.

This fixes the problem with the current simp set where Id.run (pure x) is simplified to Id.run x, instead of the desirable x.
This is particularly bad because the x is sometimes inferred with type Id X instead of X, which prevents other simp lemmas about X from firing.

Making Id reducible instead is not an option, as then the Monad instances would have nothing to key on.

@eric-wieser
Copy link
Contributor Author

eric-wieser commented Mar 5, 2025

changelog-library

@github-actions github-actions bot added the changelog-library Library label Mar 5, 2025
@eric-wieser eric-wieser requested review from TwoFX and tydeu as code owners March 6, 2025 01:26
@eric-wieser eric-wieser marked this pull request as draft March 6, 2025 01:48
@eric-wieser
Copy link
Contributor Author

eric-wieser commented Mar 6, 2025

I've split some helper lemmas to #7356, which are independent of this fix

@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Mar 6, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented Mar 6, 2025 •
edited
Loading

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 9ae2ac39c9512461643e268f0feff5654044776f --onto 5536281238dff2fb4e0a54da472d4f0d6496069e. You can force Mathlib CI using the force-mathlib-ci label. (2025-03-06 03:18:31)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e0fa6a1792458af81c8f421f5e75bfbc4117f617 --onto 7bfa8f6296ebfebc497d5b30d34f494bcc9782a2. You can force Mathlib CI using the force-mathlib-ci label. (2025-03-10 23:19:19)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase e0fa6a1792458af81c8f421f5e75bfbc4117f617 --onto 8fc8e8ed19ef218022f5a94cbf5e472e3b777e44. You can force Mathlib CI using the force-mathlib-ci label. (2025-03-11 23:53:26)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase d538e1cd90bc8dce3e8919d2ed496903577a63a9 --onto c1d145e9d70569274ac868805b4a8591d09718af. You can force Mathlib CI using the force-mathlib-ci label. (2025-03-14 01:21:44)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 5c333d88c01f71180f1ceeb00fcdad2bea1bdbf9 --onto c1d145e9d70569274ac868805b4a8591d09718af. You can force Mathlib CI using the force-mathlib-ci label. (2025-03-14 01:50:23)
  • 💥 Mathlib branch lean-pr-testing-7352 build failed against this PR. (2025-05-21 09:36:57) View Log
  • 💥 Mathlib branch lean-pr-testing-7352 build failed against this PR. (2025-05-21 10:36:00) View Log
  • 💥 Mathlib branch lean-pr-testing-7352 build failed against this PR. (2025-05-21 23:50:55) View Log
  • 💥 Mathlib branch lean-pr-testing-7352 build failed against this PR. (2025-05-22 11:21:37) View Log
  • ✅ Mathlib branch lean-pr-testing-7352 has successfully built against this PR. (2025-05-22 11:28:08) View Log
  • 💥 Mathlib branch lean-pr-testing-7352 build failed against this PR. (2025-05-22 11:31:30) View Log
  • ❗ Batteries CI can not be attempted yet, as the nightly-testing-2025-05-22 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Batteries CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2025-05-22 11:51:33)

@eric-wieser eric-wieser force-pushed the patch-43 branch 2 times, most recently from 729e005 to 439669c Compare March 10, 2025 22:51
@eric-wieser eric-wieser mentioned this pull request Mar 10, 2025
Merged
@eric-wieser eric-wieser mentioned this pull request Mar 14, 2025
Closed
github-merge-queue bot pushed a commit that referenced this pull request Mar 14, 2025
@eric-wieser
feat: mark forIn_pure_yield lemmas simp (#7433)
5c333d8 
This PR makes `simp` able to simplify basic `for` loops in monads other
than `Id`.

This is some prework for #7352, where the `Id` lemmas will be
deprecated.
sgraf812 pushed a commit that referenced this pull request Apr 23, 2025
fix: Remove simp annotations for Id.{pure_eq,map_eq,bind_eq}
ad6e42a 
This PR removes `simp` annotations for lemmas `Id.pure_eq`, `Id.map_eq`
and `Id.bind_eq` because they tend to break the abstraction of
computations in `Id`. In particular, they are problematic for
compositional reasoning about `do` notation.

While a better `simp` framework is on the horizon with #7352; this PR
simply adds the old simp lemmas wherever needed.

Breaking change: Remove the `simp` annotation from `Id.pure_eq`,
`Id.map_eq` and `Id.bind_eq`. Workaround: add manually to simp set.
sgraf812 pushed a commit that referenced this pull request Apr 23, 2025
fix: Remove simp annotations for Id.{pure_eq,map_eq,bind_eq}
8f30f49 
This PR removes `simp` annotations for lemmas `Id.pure_eq`, `Id.map_eq`
and `Id.bind_eq` because they tend to break the abstraction of
computations in `Id`. In particular, they are problematic for
compositional reasoning about `do` notation.

While a better `simp` framework is on the horizon with #7352; this PR
simply adds the old simp lemmas wherever needed.

Breaking change: Remove the `simp` annotation from `Id.pure_eq`,
`Id.map_eq` and `Id.bind_eq`. Workaround: add manually to simp set.
@sgraf812 sgraf812 mentioned this pull request Apr 23, 2025
Closed
sgraf812 pushed a commit that referenced this pull request Apr 23, 2025
fix: Remove simp annotations for Id.{pure_eq,map_eq,bind_eq}
c38cef0 
This PR removes `simp` annotations for lemmas `Id.pure_eq`, `Id.map_eq`
and `Id.bind_eq` because they tend to break the abstraction of
computations in `Id`. In particular, they are problematic for
compositional reasoning about `do` notation.

While a better `simp` framework is on the horizon with #7352; this PR
simply adds the old simp lemmas wherever needed.

Breaking change: Remove the `simp` annotation from `Id.pure_eq`,
`Id.map_eq` and `Id.bind_eq`. Workaround: add manually to simp set.
sgraf812 pushed a commit that referenced this pull request Apr 23, 2025
fix: Remove simp annotations for Id.{pure_eq,map_eq,bind_eq}
fc88a58 
This PR removes `simp` annotations for lemmas `Id.pure_eq`, `Id.map_eq`
and `Id.bind_eq` because they tend to break the abstraction of
computations in `Id`. In particular, they are problematic for
compositional reasoning about `do` notation.

While a better `simp` framework is on the horizon with #7352; this PR
simply adds the old simp lemmas wherever needed.

Breaking change: Remove the `simp` annotation from `Id.pure_eq`,
`Id.map_eq` and `Id.bind_eq`. Workaround: add manually to simp set.
eric-wieser and others added 3 commits May 16, 2025 23:20
@sgraf812 sgraf812 mentioned this pull request May 16, 2025
Closed
leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request May 21, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#7352
254ab91
leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request May 21, 2025
@leanprover-community-mathlib4-bot
Update lean-toolchain for testing leanprover/lean4#7352
03450b5
@eric-wieser eric-wieser mentioned this pull request May 21, 2025
Closed
@leanprover-community-bot leanprover-community-bot removed awaiting-mathlib We should not merge this until we have a successful Mathlib build breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels May 21, 2025
@leanprover-community-bot
Copy link
Collaborator

leanprover-community-bot commented May 21, 2025

@leanprover-community-bot leanprover-community-bot added the builds-mathlib CI has verified that Mathlib builds against this PR label May 21, 2025
@kim-em kim-em added this pull request to the merge queue May 21, 2025
@github-merge-queue github-merge-queue bot removed this pull request from the merge queue due to failed status checks May 21, 2025
@leanprover-community-bot leanprover-community-bot added breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan and removed builds-mathlib CI has verified that Mathlib builds against this PR labels May 21, 2025
mathlib-bors bot pushed a commit to leanprover-community/mathlib4 that referenced this pull request May 22, 2025
@eric-wieser
chore: fix some defeq abuse in theorem statements around the Id mon…
b9e5480 
…ad (#25098)

Follows on from leanprover/lean4#7352.

This also deprecates:
* `id.mk`, which looks like a porting error
* `Free(Add)(Magma|Semigroup).mul_map_seq`, which is a garbage lemma that both is not meaningfully about the free objects and has defeq abuse everywhere.
@kim-em kim-em added this pull request to the merge queue May 22, 2025
@github-merge-queue github-merge-queue bot removed this pull request from the merge queue due to failed status checks May 22, 2025
erdOne pushed a commit to leanprover-community/mathlib4 that referenced this pull request May 22, 2025
@eric-wieser @erdOne
chore: fix some defeq abuse in theorem statements around the Id mon…
d70aa15 
…ad (#25098)

Follows on from leanprover/lean4#7352.

This also deprecates:
* `id.mk`, which looks like a porting error
* `Free(Add)(Magma|Semigroup).mul_map_seq`, which is a garbage lemma that both is not meaningfully about the free objects and has defeq abuse everywhere.
@eric-wieser
Copy link
Contributor Author

eric-wieser commented May 22, 2025

Looks like this needs a rebase/ merge with master, and a proof needs a very small tweak

eric-wieser added a commit to leanprover-community/mathlib4 that referenced this pull request May 22, 2025
@eric-wieser
Revert "fix for leanprover/lean4#7352"
0fd2dee 
This reverts commit 38ca408.
eric-wieser added a commit to leanprover-community/mathlib4 that referenced this pull request May 22, 2025
@eric-wieser
chore: fix some defeq abuse in theorem statements around the Id mon…
6dfae22 
…ad (#25098)

Follows on from leanprover/lean4#7352.

This also deprecates:
* `id.mk`, which looks like a porting error
* `Free(Add)(Magma|Semigroup).mul_map_seq`, which is a garbage lemma that both is not meaningfully about the free objects and has defeq abuse everywhere.
@leanprover-community-bot leanprover-community-bot added builds-mathlib CI has verified that Mathlib builds against this PR breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan and removed breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan builds-mathlib CI has verified that Mathlib builds against this PR labels May 22, 2025
eric-wieser
eric-wieser commented May 22, 2025
View reviewed changes
@kim-em kim-em added this pull request to the merge queue May 22, 2025
Merged via the queue into leanprover:master with commit ae1ab94 May 22, 2025
14 checks passed
bwehlin pushed a commit to bwehlin/mathlib4 that referenced this pull request May 31, 2025
@eric-wieser
chore: fix some defeq abuse in theorem statements around the Id mon…
41b348e 
…ad (leanprover-community#25098)

Follows on from leanprover/lean4#7352.

This also deprecates:
* `id.mk`, which looks like a porting error
* `Free(Add)(Magma|Semigroup).mul_map_seq`, which is a garbage lemma that both is not meaningfully about the free objects and has defeq abuse everywhere.
jcommelin pushed a commit to leanprover-community/mathlib4 that referenced this pull request Jun 4, 2025
@leanprover-community-mathlib4-bot @kim-em
@Vierkantor @Kha @eric-wieser @Rob23oba @jrr6
chore: adaptations for nightly-2025-06-04 (#25431)
3780f5f 
* Update lean-toolchain for testing leanprover/lean4#8347

* fixes for leanprover/lean4#8347

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

* deprecations for leanprover/lean4#8397

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

* chore: adaptations for nightly-2025-05-19

* Trigger CI for leanprover/lean4#8347

* Update the style linter to use LinterOptions

* Fix test

* chore: adaptations for nightly-2025-05-19 (#25017)



Co-authored-by: Kim Morrison <[email protected]>
Co-authored-by: github-actions <[email protected]>
Co-authored-by: mathlib4-bot <[email protected]>
Co-authored-by: Anne C.A. Baanen <[email protected]>
Co-authored-by: Sebastian Ullrich <[email protected]>

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

* Merge master into nightly-testing

* feat: a `grind` test case (#25037)

Adds a test case for `grind` that was previously failing in the presence of Mathlib's typeclass shortcuts. Let's just keep it in Mathlib as a regression test.

Note that this is a PR to `bump/v4.21.0`, as it requires a recent nightly toolchain. (It can still be reviewed and bors'd as any other PR.)

* lake update

* fixes

* fixes

* fixes

* fixes

* fix

* fixes

* fixes

* shake --update

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

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

* lake update

* Trigger CI for leanprover/lean4#7352

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

* chore: adaptations for nightly-2025-05-21 (#25079)



Co-authored-by: mathlib4-bot <[email protected]>
Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>
Co-authored-by: github-actions <[email protected]>
Co-authored-by: Anne C.A. Baanen <[email protected]>

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

* fix for leanprover/lean4#7352

* remove unneeded List.ofFn_succ from simp sets

* Merge master into nightly-testing

* Merge master into nightly-testing

* Revert "fix for leanprover/lean4#7352"

This reverts commit 38ca408.

* chore: fix some defeq abuse in theorem statements around the `Id` monad (#25098)

Follows on from leanprover/lean4#7352.

This also deprecates:
* `id.mk`, which looks like a porting error
* `Free(Add)(Magma|Semigroup).mul_map_seq`, which is a garbage lemma that both is not meaningfully about the free objects and has defeq abuse everywhere.

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

* update batteries

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

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

* chore: adaptations for nightly-2025-05-22 (#25110)



Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>
Co-authored-by: Kim Morrison <[email protected]>
Co-authored-by: github-actions <[email protected]>

* remove now upstreamed `clear_value`

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

* chore: update tests for `Format` bug fix

* Trigger CI for leanprover/lean4#8457

* lake update

* lake update

* fixes

* Merge master into nightly-testing

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

* fix

* chore: adaptations for nightly-2025-05-24 (#25147)



Co-authored-by: Kim Morrison <[email protected]>
Co-authored-by: mathlib4-bot <[email protected]>
Co-authored-by: Eric Wieser <[email protected]>
Co-authored-by: github-actions <[email protected]>

* chore: adaptations for nightly-2025-05-24

* Merge master into nightly-testing

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

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

* chore: adaptations for nightly-2025-05-25

* chore: adaptations for nightly-2025-05-25 (#25184)



Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>
Co-authored-by: Eric Wieser <[email protected]>
Co-authored-by: Kim Morrison <[email protected]>
Co-authored-by: github-actions <[email protected]>

* unsimp `List.getElem?_length`

This is solved using `getElem?_neg` now.

* chore: adaptations for nightly-2025-05-25

* Trigger CI for leanprover/lean4#8470

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

* lake update

* deprecations

* Trigger CI for leanprover/lean4#8449

* Merge master into nightly-testing

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

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

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

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

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



Co-authored-by: mathlib4-bot <[email protected]>
Co-authored-by: github-actions <[email protected]>
Co-authored-by: Kim Morrison <[email protected]>

* fix

* fix merge

* fix merge again

* deprecations

* deprecations

* fix Archive

* comment out test

* Fix and re-enable directory dependency lint test.

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

* Use the formatting from the master branch. (Seems to have been a merge that went wrong.)

* lake update

* chore: adaptations for nightly-2025-05-28 (#25295)



Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>
Co-authored-by: mathlib4-bot <[email protected]>
Co-authored-by: github-actions <[email protected]>

* fix

* Trigger CI for leanprover/lean4#8337

* fixes

* Merge master into nightly-testing

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

* chore: adaptations for nightly-2025-05-29 (#25306)



Co-authored-by: Kim Morrison <[email protected]>
Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>
Co-authored-by: mathlib4-bot <[email protected]>
Co-authored-by: github-actions <[email protected]>
Co-authored-by: Rob23oba <[email protected]>

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

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

* fix Archive

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



Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>
Co-authored-by: Anne C.A. Baanen <[email protected]>
Co-authored-by: github-actions <[email protected]>
Co-authored-by: mathlib4-bot <[email protected]>

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

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



Co-authored-by: Kim Morrison <[email protected]>
Co-authored-by: mathlib4-bot <[email protected]>
Co-authored-by: Anne C.A. Baanen <[email protected]>
Co-authored-by: github-actions <[email protected]>

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

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

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

* fix

* fix

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

* fix

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

* bump toolchain

---------

Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>
Co-authored-by: Kim Morrison <[email protected]>
Co-authored-by: github-actions <[email protected]>
Co-authored-by: mathlib4-bot <[email protected]>
Co-authored-by: Anne C.A. Baanen <[email protected]>
Co-authored-by: Sebastian Ullrich <[email protected]>
Co-authored-by: Eric Wieser <[email protected]>
Co-authored-by: Rob23oba <[email protected]>
Co-authored-by: Joseph Rotella <[email protected]>
jcommelin added a commit to leanprover-community/mathlib4 that referenced this pull request Jun 6, 2025
@leanprover-community-mathlib4-bot @kim-em
@eric-wieser @Rob23oba @jrr6 @Vierkantor @Kha @jcommelin @JovanGerb @nomeata
chore: adaptations for nightly-2025-06-05 (#25490)
5a9a408 
* chore: adaptations for nightly-2025-05-21

* fix for leanprover/lean4#7352

* remove unneeded List.ofFn_succ from simp sets

* Merge master into nightly-testing

* Merge master into nightly-testing

* Revert "fix for leanprover/lean4#7352"

This reverts commit 38ca408.

* chore: fix some defeq abuse in theorem statements around the `Id` monad (#25098)

Follows on from leanprover/lean4#7352.

This also deprecates:
* `id.mk`, which looks like a porting error
* `Free(Add)(Magma|Semigroup).mul_map_seq`, which is a garbage lemma that both is not meaningfully about the free objects and has defeq abuse everywhere.

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

* update batteries

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

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

* chore: adaptations for nightly-2025-05-22 (#25110)



Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>
Co-authored-by: Kim Morrison <[email protected]>
Co-authored-by: github-actions <[email protected]>

* remove now upstreamed `clear_value`

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

* chore: update tests for `Format` bug fix

* Trigger CI for leanprover/lean4#8457

* lake update

* lake update

* fixes

* Merge master into nightly-testing

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

* fix

* chore: adaptations for nightly-2025-05-24 (#25147)



Co-authored-by: Kim Morrison <[email protected]>
Co-authored-by: mathlib4-bot <[email protected]>
Co-authored-by: Eric Wieser <[email protected]>
Co-authored-by: github-actions <[email protected]>

* chore: adaptations for nightly-2025-05-24

* Merge master into nightly-testing

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

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

* chore: adaptations for nightly-2025-05-25

* chore: adaptations for nightly-2025-05-25 (#25184)



Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>
Co-authored-by: Eric Wieser <[email protected]>
Co-authored-by: Kim Morrison <[email protected]>
Co-authored-by: github-actions <[email protected]>

* unsimp `List.getElem?_length`

This is solved using `getElem?_neg` now.

* chore: adaptations for nightly-2025-05-25

* Trigger CI for leanprover/lean4#8470

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

* lake update

* deprecations

* Trigger CI for leanprover/lean4#8449

* Merge master into nightly-testing

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

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

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

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

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



Co-authored-by: mathlib4-bot <[email protected]>
Co-authored-by: github-actions <[email protected]>
Co-authored-by: Kim Morrison <[email protected]>

* fix

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

* fix merge

* fix merge again

* deprecations

* deprecations

* fix Archive

* comment out test

* Fix and re-enable directory dependency lint test.

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

* Use the formatting from the master branch. (Seems to have been a merge that went wrong.)

* lake update

* chore: adaptations for nightly-2025-05-28 (#25295)



Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>
Co-authored-by: mathlib4-bot <[email protected]>
Co-authored-by: github-actions <[email protected]>

* fix

* Trigger CI for leanprover/lean4#8337

* Trigger CI for leanprover/lean4#8519

* fixes

* Merge master into nightly-testing

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

* chore: adaptations for nightly-2025-05-29 (#25306)



Co-authored-by: Kim Morrison <[email protected]>
Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>
Co-authored-by: mathlib4-bot <[email protected]>
Co-authored-by: github-actions <[email protected]>
Co-authored-by: Rob23oba <[email protected]>

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

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

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

* fix Archive

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



Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>
Co-authored-by: Anne C.A. Baanen <[email protected]>
Co-authored-by: github-actions <[email protected]>
Co-authored-by: mathlib4-bot <[email protected]>

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

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



Co-authored-by: Kim Morrison <[email protected]>
Co-authored-by: mathlib4-bot <[email protected]>
Co-authored-by: Anne C.A. Baanen <[email protected]>
Co-authored-by: github-actions <[email protected]>

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

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

* change phrasing of comments

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

* fix two lint problems

* Trigger CI for leanprover/lean4#8519

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

* fix

* fix

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

* fix

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

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

* give specialized simp lemmas higher prio

* simp can prove these

* simp can prove these

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

* bump toolchain

* Adapt eqns

* Revert "Adapt eqns"

This reverts commit 34f1f7f.

* Simply remove check for now

* fix a bunch

* fixes?

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

* add `simp low` lemma `injOn_of_eq_iff_eq`

* wip

* wip

* wip

* fix

* Trigger CI for leanprover-community/batteries#1220

* Merge master into nightly-testing

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

* Kick CI

* Bump lean4-cli

* Bump import-graph

* Kick CI

* update lakefile

* chore: use more robust syntax quotation in Shake

* cleanup lakefile

---------

Co-authored-by: mathlib4-bot <[email protected]>
Co-authored-by: leanprover-community-mathlib4-bot <[email protected]>
Co-authored-by: Kim Morrison <[email protected]>
Co-authored-by: Eric Wieser <[email protected]>
Co-authored-by: github-actions <[email protected]>
Co-authored-by: Rob23oba <[email protected]>
Co-authored-by: Joseph Rotella <[email protected]>
Co-authored-by: Anne C.A. Baanen <[email protected]>
Co-authored-by: Sebastian Ullrich <[email protected]>
Co-authored-by: Johan Commelin <[email protected]>
Co-authored-by: Jovan Gerbscheid <[email protected]>
Co-authored-by: Joachim Breitner <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@datokrat datokrat datokrat left review comments

@digama0 digama0 Awaiting requested review from digama0 digama0 is a code owner

@kim-em kim-em Awaiting requested review from kim-em kim-em is a code owner

@TwoFX TwoFX Awaiting requested review from TwoFX TwoFX is a code owner

@tydeu tydeu Awaiting requested review from tydeu tydeu is a code owner

@david-christiansen david-christiansen Awaiting requested review from david-christiansen david-christiansen is a code owner

@mhuisi mhuisi Awaiting requested review from mhuisi mhuisi is a code owner

@Kha Kha Awaiting requested review from Kha Kha is a code owner

@leodemoura leodemoura Awaiting requested review from leodemoura leodemoura is a code owner

@zwarich zwarich Awaiting requested review from zwarich

Assignees

No one assigned

Labels

breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@eric-wieser @leanprover-community-bot @datokrat @kim-em