Skip to content

[Merged by Bors] - chore: fix some defeq abuse in theorem statements around the Id monad#25098

Closed
eric-wieser wants to merge 5 commits intomasterfrom
eric-wieser/Id.run
Closed

[Merged by Bors] - chore: fix some defeq abuse in theorem statements around the Id monad#25098
eric-wieser wants to merge 5 commits intomasterfrom
eric-wieser/Id.run

Conversation

@eric-wieser
Copy link
Copy Markdown
Member

@eric-wieser eric-wieser commented May 21, 2025 •
edited
Loading

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.

Open in Gitpod

@eric-wieser eric-wieser requested a review from kim-em May 21, 2025 23:01
@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented May 21, 2025

bors d+

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented May 21, 2025

✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@ghost ghost added the delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). label May 21, 2025
@github-actions
Copy link
Copy Markdown

github-actions bot commented May 21, 2025 •
edited
Loading

PR summary 79b3ab0509

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference

Declarations diff

+-+-+-+-+- id_traverse

You can run this locally as follows 
## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

Decrease in tech debt: (relative, absolute) = (2.00, 0.00)
Current number Change Type
1542 -2 porting notes

Current commit 79b3ab0509
Reference commit 83f3832c6c

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary
  • The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
  • The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

@eric-wieser eric-wieser added the auto-merge-after-CI Please do not add manually. Requests for a bot to merge automatically once CI is done. label May 21, 2025
@ghost
Copy link
Copy Markdown

ghost commented May 22, 2025

As this PR is labelled auto-merge-after-CI, we are now sending it to bors:

bors merge

@ghost ghost added the ready-to-merge This PR has been sent to bors. label May 22, 2025
mathlib-bors bot pushed a commit 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.
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented May 22, 2025

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore: fix some defeq abuse in theorem statements around the Id monad [Merged by Bors] - chore: fix some defeq abuse in theorem statements around the Id monad May 22, 2025
@mathlib-bors mathlib-bors bot closed this May 22, 2025
@mathlib-bors mathlib-bors bot deleted the eric-wieser/Id.run branch May 22, 2025 01:31
erdOne pushed a commit 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 added a commit 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.
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 that referenced this pull request Jun 4, 2025
@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 <kim@tqft.net>
Co-authored-by: github-actions <github-actions@github.com>
Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>

* 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 <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: github-actions <github-actions@github.com>
Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>

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

* 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 <kim@tqft.net>
Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: github-actions <github-actions@github.com>

* 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 <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: github-actions <github-actions@github.com>

* 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 <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: github-actions <github-actions@github.com>
Co-authored-by: Kim Morrison <kim@tqft.net>

* 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 <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: github-actions <github-actions@github.com>

* 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 <kim@tqft.net>
Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: github-actions <github-actions@github.com>
Co-authored-by: Rob23oba <robin.arnez@web.de>

* 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 <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>
Co-authored-by: github-actions <github-actions@github.com>
Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>

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

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



Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>
Co-authored-by: github-actions <github-actions@github.com>

* 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 <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: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Rob23oba <robin.arnez@web.de>
Co-authored-by: Joseph Rotella <7482866+jrr6@users.noreply.github.com>
jcommelin added a commit that referenced this pull request Jun 6, 2025
@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 <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>

* 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 <kim@tqft.net>
Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: github-actions <github-actions@github.com>

* 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 <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: github-actions <github-actions@github.com>

* 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 <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: github-actions <github-actions@github.com>
Co-authored-by: Kim Morrison <kim@tqft.net>

* 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 <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: github-actions <github-actions@github.com>

* 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 <kim@tqft.net>
Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: github-actions <github-actions@github.com>
Co-authored-by: Rob23oba <robin.arnez@web.de>

* 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 <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>
Co-authored-by: github-actions <github-actions@github.com>
Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>

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

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



Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: mathlib4-bot <github-mathlib4-bot@leanprover.zulipchat.com>
Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>
Co-authored-by: github-actions <github-actions@github.com>

* 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 <github-mathlib4-bot@leanprover.zulipchat.com>
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: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: github-actions <github-actions@github.com>
Co-authored-by: Rob23oba <robin.arnez@web.de>
Co-authored-by: Joseph Rotella <7482866+jrr6@users.noreply.github.com>
Co-authored-by: Anne C.A. Baanen <vierkantor@vierkantor.com>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Jovan Gerbscheid <jovan.gerbscheid@gmail.com>
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@kim-em kim-em Awaiting requested review from kim-em

Assignees

No one assigned

Labels

auto-merge-after-CI Please do not add manually. Requests for a bot to merge automatically once CI is done. delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). ready-to-merge This PR has been sent to bors.

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@eric-wieser @kim-em