Skip to content

feat: integer prerequisites for finite type lemmas#7378

Merged
TwoFX merged 3 commits intomasterfrom
markus/int-thy
Mar 7, 2025
Merged

feat: integer prerequisites for finite type lemmas#7378
TwoFX merged 3 commits intomasterfrom
markus/int-thy

Conversation

@TwoFX
Copy link
Copy Markdown
Member

@TwoFX TwoFX commented Mar 7, 2025 •
edited
Loading

This PR adds lemmas about Int that will be required in #7368.

Most notably, we add

@[simp] theorem neg_nonpos_iff (i : Int) : -i ≤ 0 ↔ 0 ≤ i

which causes some breakage but gets us closer to mathlib which has a more general version of this that applies to Int.

Note also that the mathlib adaptation branch deletes the (unused in mathlib) mathib lemma Int.zero_le_ofNat as there is now a syntactically different (but definitionally equal) Int.zero_le_ofNat in core.

@TwoFX TwoFX added the changelog-library Library label Mar 7, 2025
@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc March 7, 2025 12:05 Inactive
@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 7, 2025
ghost pushed a commit to leanprover-community/batteries that referenced this pull request Mar 7, 2025
Update lean-toolchain for testing leanprover/lean4#7378
8e7381f
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Mar 7, 2025
Update lean-toolchain for testing leanprover/lean4#7378
bc41439
@ghost ghost added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label Mar 7, 2025
@ghost
Copy link
Copy Markdown

ghost commented Mar 7, 2025 •
edited by ghost
Loading

Mathlib CI status (docs):

@github-actions github-actions bot temporarily deployed to lean-lang.org/lean4/doc March 7, 2025 13:08 Inactive
ghost pushed a commit to leanprover-community/batteries that referenced this pull request Mar 7, 2025
Trigger CI for leanprover/lean4#7378
86961b7
ghost pushed a commit to leanprover-community/mathlib4 that referenced this pull request Mar 7, 2025
Trigger CI for leanprover/lean4#7378
f4e3e56
@ghost ghost added builds-mathlib CI has verified that Mathlib builds against this PR and removed breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan labels Mar 7, 2025
@TwoFX TwoFX marked this pull request as ready for review March 7, 2025 16:08
@TwoFX TwoFX requested a review from kim-em as a code owner March 7, 2025 16:08
@TwoFX TwoFX added this pull request to the merge queue Mar 7, 2025
Merged via the queue into master with commit a8a5c6c Mar 7, 2025
23 checks passed
kim-em added a commit to leanprover-community/mathlib4 that referenced this pull request Mar 10, 2025
@jcommelin @kim-em
@TwoFX @nomeata @kmill @tydeu @jrr6 @kbuzzard @Kha @mattrobball @JovanGerb
chore: adaptations for nightly-2025-03-09 (#22758)
ec93745 
* chore: adaptations for nightly-2025-02-20

* Merge master into nightly-testing

* minor reverts

* more

* deprecation

* another

* more

* restore check-yaml

* .

* .

* chore: adaptations for nightly-2025-02-20 (#22144)

* lake update

* fixes

* fix namespace

* fix test

* Merge master into nightly-testing

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

* copy test from master

* Merge master into nightly-testing

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

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

* update

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

* didn't commit

* fix

* fix test

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

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

* fixes for leanprover/lean4#7013

* fixes for leanprover/lean4#7013

* Trigger CI for leanprover/lean4#7013

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

* update

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

* Trigger CI for leanprover/lean4#7046

* Switch from mk to ofBitVec

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

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

* lake update

* lake update

* fixes

* another maxheartbeats

* fix tests

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

* fix

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

* lake update

* fixes

* lake exe shake --fix

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

* Trigger CI for leanprover/lean4#7069

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

* remove upstreamed

* Trigger CI for leanprover/lean4#7059

* Trigger CI for leanprover/lean4#7059

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

* Trigger CI for leanprover/lean4#7069

* Trigger CI for leanprover/lean4#7069

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

* quite a bit more to go

* lake update

* fix merge

* fix

* adapt

* adapt

* Trigger CI for leanprover/lean4#7082

* Trigger CI for leanprover/lean4#7069

* lake update

* lake update

* fixes

* fixes

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

* Trigger CI for leanprover/lean4#7069

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

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

* fixes

* fixes 2

* fixes 3

* built mathlib

* Trigger CI for leanprover/lean4#7069

* fix simps test

* fixes for leanprover/lean4#7059

* fix: cache lib dir (adaption for lean4#7001) (#21967)

* fixes

* fixes for leanprover/lean4#7059

* restore broken files

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

* lake update

* lake update

* oops

* comment out broken files

* longFile

* oops, one more

* .

* searchPath

* .

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

* fixes

* update manifest

* fix

* fix

* Trigger CI for leanprover/lean4#7103

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

* lake update

* deprecations

* restore computability files broken by defeq yesterday

* fixes

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

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

* lake update

* fixes

* fix merge

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

* Merge master into nightly-testing

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

* fix merge

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

* minor reverts

* more

* deprecation

* another

* more

* restore check-yaml

* .

* .

---------

Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Johan Commelin <johan@commelin.net>
Co-authored-by: Markus Himmel <markus@lean-fro.org>
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: Mac Malone <mac@lean-fro.org>

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

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

* chore(Tactic/DeriveTraversable): adapt to `auxDeclToFullName` relocation

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

* fixes

* update batteries

* update proofwidgets

* Trigger CI for leanprover/lean4#7166

* Trigger CI for leanprover/lean4#7166

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

* lake update

* fixes

* deprecations

* .

* archive

* fix tests

* fix tests

* chore: adaptations for nightly-2025-02-24 (#22266)



Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>

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

* Trigger CI for leanprover/lean4#7166

* Trigger CI for leanprover/lean4#7166

* Trigger CI for leanprover/lean4#7166

* Trigger CI for leanprover/lean4#7166

* Adapt

* Trigger CI for leanprover/lean4#7166

* revert Mathlib/Data/Multiset/Basic, and refix

* Merge master into nightly-testing

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

* remove upstreamed

* fix

* fix tests

* Apply suggestions from code review

Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>

* chore: adaptations for nightly-2025-02-26 (#22347)



Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>

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

* Trigger CI for leanprover/lean4#7166

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

* fix

* I would not have guessed that this lemma already exists!

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

* fix

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

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

* Merge master into nightly-testing

* deprecation

* Trigger CI for leanprover/lean4#7166

* deprecation

* chore: adaptations for nightly-2025-03-02 (#22460)



Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Markus Himmel <markus@lean-fro.org>

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

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

* remove upstreamed

* chore: adaptations for nightly-2025-03-03

* Trigger CI for leanprover/lean4#7166

* chore: adaptations for nightly-2025-03-03 (#22493)



Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Johan Commelin <johan@commelin.net>

* bump toolchain and dependencies

* Trigger CI for leanprover/lean4#7166

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

* lake update

* Trigger CI for leanprover/lean4#7166

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

* fix?

* add adaptation notes to revert _root_

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

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

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

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

* Merge master into nightly-testing

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

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

* fixes for leanprover/lean4#7358

* fixes for leanprover/lean4#7358

* fixes for leanprover/lean4#7358

* Trigger CI for leanprover/lean4#7358

* Trigger CI for leanprover/lean4#7261

* fix Mathlib.Linter.getNamesFrom

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

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

* lake update

* add_div is protected

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

* More like that

* adapt

* Trigger CI for leanprover/lean4#7378

* Fix

* fix

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

* lake update

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

* chore(RingTheory/LocalRing/ResidueField/Ideal): increase `simp` prio, analogous to #22215

* process adaptation notes

---------

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: Markus Himmel <markus@lean-fro.org>
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: Mac Malone <mac@lean-fro.org>
Co-authored-by: Joseph Rotella <7482866+jrr6@users.noreply.github.com>
Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Co-authored-by: Matthew Ballard <matt@mrb.email>
Co-authored-by: Jovan Gerbscheid <jovan.gerbscheid@gmail.com>
kim-em added a commit to leanprover-community/mathlib4 that referenced this pull request Mar 12, 2025
@jcommelin @jrr6
@kmill @kim-em @nomeata @kbuzzard @TwoFX @Kha @mattrobball @JovanGerb
chore: adaptations for nightly-2025-03-11 (#22826)
2677da0 
* chore: bump to nightly-2025-02-21

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

* chore(Tactic/DeriveTraversable): adapt to `auxDeclToFullName` relocation

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

* fixes

* update batteries

* update proofwidgets

* Trigger CI for leanprover/lean4#7166

* Trigger CI for leanprover/lean4#7166

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

* lake update

* fixes

* deprecations

* .

* archive

* fix tests

* fix tests

* chore: adaptations for nightly-2025-02-24 (#22266)



Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>

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

* Trigger CI for leanprover/lean4#7166

* Trigger CI for leanprover/lean4#7166

* Trigger CI for leanprover/lean4#7166

* Trigger CI for leanprover/lean4#7166

* Adapt

* Trigger CI for leanprover/lean4#7166

* revert Mathlib/Data/Multiset/Basic, and refix

* Merge master into nightly-testing

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

* remove upstreamed

* fix

* fix tests

* Apply suggestions from code review

Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>

* chore: adaptations for nightly-2025-02-26 (#22347)



Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>

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

* Trigger CI for leanprover/lean4#7166

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

* fix

* I would not have guessed that this lemma already exists!

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

* fix

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

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

* Merge master into nightly-testing

* deprecation

* Trigger CI for leanprover/lean4#7166

* deprecation

* chore: adaptations for nightly-2025-03-02 (#22460)



Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Markus Himmel <markus@lean-fro.org>

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

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

* remove upstreamed

* chore: adaptations for nightly-2025-03-03

* Trigger CI for leanprover/lean4#7166

* chore: adaptations for nightly-2025-03-03 (#22493)



Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Johan Commelin <johan@commelin.net>

* bump toolchain and dependencies

* Trigger CI for leanprover/lean4#7166

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

* lake update

* Trigger CI for leanprover/lean4#7166

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

* fix?

* add adaptation notes to revert _root_

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

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

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

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

* Merge master into nightly-testing

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

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

* fixes for leanprover/lean4#7358

* fixes for leanprover/lean4#7358

* fixes for leanprover/lean4#7358

* Trigger CI for leanprover/lean4#7358

* Trigger CI for leanprover/lean4#7261

* fix Mathlib.Linter.getNamesFrom

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

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

* lake update

* add_div is protected

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

* More like that

* adapt

* Trigger CI for leanprover/lean4#7378

* Fix

* fix

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

* lake update

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

* chore(RingTheory/LocalRing/ResidueField/Ideal): increase `simp` prio, analogous to #22215

* process adaptation notes

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

* chore: adaptations for nightly-2025-03-10

* rm upstreamed

* rm upstreamed

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

---------

Co-authored-by: leanprover-community-mathlib4-bot <leanprover-community-mathlib4-bot@users.noreply.github.com>
Co-authored-by: Joseph Rotella <7482866+jrr6@users.noreply.github.com>
Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: Joachim Breitner <mail@joachim-breitner.de>
Co-authored-by: Kevin Buzzard <k.buzzard@imperial.ac.uk>
Co-authored-by: Markus Himmel <markus@lean-fro.org>
Co-authored-by: Sebastian Ullrich <sebasti@nullri.ch>
Co-authored-by: Matthew Ballard <matt@mrb.email>
Co-authored-by: Jovan Gerbscheid <jovan.gerbscheid@gmail.com>
@TwoFX TwoFX deleted the markus/int-thy branch August 4, 2025 07:20
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 kim-em is a code owner

Assignees

No one assigned

Labels

builds-mathlib CI has verified that Mathlib builds against this PR 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.

1 participant

@TwoFX