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 by Bors] - chore(data/finset/basic): move `disjoint` proofs earlier #16436

Closed

eric-wieser wants to merge 6 commits into master from eric-wieser/tidy-finset-disjoint

Member

eric-wieser commented Sep 8, 2022

This avoids repeating work for disj_union, and takes the stance that disjoint is part of the lattice API.


          chore(data/finset/basic): move disjoint proofs earlier

fe1c20b

This avoids repeating work for `disj_union`, and takes the stance that `disjoint` is part of the lattice API.

eric-wieser added awaiting-review awaiting-CI t-order labels

eric-wieser requested a review from YaelDillies

September 8, 2022 23:36

eric-wieser mentioned this pull request

[Merged by Bors] - refactor(order/bounded_order): relax typeclass requirements on disjoint and codisjoint #16434

Closed

2 tasks

eric-wieser commented

View reviewed changes

src/data/finset/basic.lean

Comment on lines +2164 to +2166

+              @[simp] lemma disjoint_map [decidable_eq α] [decidable_eq β] {s t : finset α} (f : α ↪ β) :
+                disjoint (s.map f) (t.map f) ↔ disjoint s t :=
+              by rw [disjoint_left, disjoint_left, ←map_disj_union_aux]

Member Author

eric-wieser Sep 8, 2022

This lemma along with disjoint_image are the main golfs from this change; but the longer term goal is to unify the hypothesis taken by finset.disj_union with disjoint.

eric-wieser commented

View reviewed changes

src/data/finset/basic.lean

-              end bUnion
-              /-! ### disjoint -/
-              --TODO@Yaël: Kill lemmas duplicate with `boolean_algebra`

Member Author

eric-wieser Sep 8, 2022

@YaelDillies, I assume this comment refers only to sdiff lemmas?

Collaborator

YaelDillies Sep 9, 2022

Absolutely.

eric-wieser commented

View reviewed changes

src/data/finset/basic.lean

@@ @@ -1339,7 +1412,17 @@ sup_eq_sdiff_sup_sdiff_sup_inf @@
               lemma erase_eq_empty_iff (s : finset α) (a : α) : s.erase a = ∅ ↔ s = ∅ ∨ s = {a} :=
               by rw [←sdiff_singleton_eq_erase, sdiff_eq_empty_iff_subset, subset_singleton_iff]
-              end decidable_eq
+              --TODO@Yaël: Kill lemmas duplicate with `boolean_algebra`

Member Author

eric-wieser Sep 8, 2022

(this comment moved along with the lemmas below)


          empty commit to try and avoid a timeout

327f93b

github-actions bot removed the awaiting-CI label

YaelDillies approved these changes

View reviewed changes

src/data/finset/basic.lean Outdated Show resolved Hide resolved

src/data/finset/basic.lean Show resolved Hide resolved

src/data/finset/basic.lean Show resolved Hide resolved


          Update src/data/finset/basic.lean

d872acd

Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

kmill approved these changes

View reviewed changes

Collaborator

kmill left a comment

Thanks!

bors r+

Collaborator

kmill commented Sep 22, 2022

bors r-

bors bot commented Sep 22, 2022

Canceled.


          Merge branch 'master' into eric-wieser/tidy-finset-disjoint

c6fb460

Collaborator

kmill commented Sep 22, 2022

bors r+

github-actions bot added ready-to-merge and removed awaiting-review labels

Collaborator

kmill commented Sep 22, 2022

Sorry, I think I didn't merge this carefully. Could you fix the merge? Then feel free to bors it.

bors r-
bors d+

bors bot commented Sep 22, 2022

✌️ 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.

bors bot commented Sep 22, 2022

Canceled.

github-actions bot added the delegated label

YaelDillies added 2 commits

September 22, 2022 16:56


          fix merge

7fe139a


          spurious whitespace

bf52b05

Collaborator

kmill commented Sep 22, 2022

Thanks @YaelDillies for fixing this PR. I'd have preferred if you had exercised less editorial control (i.e., not removing all the sections that Eric had introduced -- another section for symmetric differences would have sufficed), but the PR is fine as-is and I've made sure Eric is aware of your changes.

bors r+

Collaborator

YaelDillies commented Sep 22, 2022

I thought those sections were remnants of your merge? Pretty sure they got deleted in another PR rather than added here.

Collaborator

kmill commented Sep 22, 2022

@YaelDillies All you have to do to check is go to https://github.com/leanprover-community/mathlib/pull/16436/commits and look at the commits. The sections were introduced in the first commit and never removed until 7fe139a. You can also check what my merge did, which was just deciding where to put the new stuff about symmetric differences -- the merge wasn't careful in that I didn't bother to fix the required variables. I think it's good practice to read through git histories to keep track of who is doing what and whether anyone (including myself) has accidentally deleted other people's work.

bors bot pushed a commit that referenced this pull request


          chore(data/finset/basic): move disjoint proofs earlier (#16436)

e69886e

This avoids repeating work for `disj_union`, and takes the stance that `disjoint` is part of the lattice API.



Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

bors bot commented Sep 22, 2022

This PR was included in a batch that was canceled, it will be automatically retried

bors bot pushed a commit that referenced this pull request


          chore(data/finset/basic): move disjoint proofs earlier (#16436)

47009c4

This avoids repeating work for `disj_union`, and takes the stance that `disjoint` is part of the lattice API.



Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

bors bot commented Sep 23, 2022

Build failed (retrying...):

Run tests

bors bot pushed a commit that referenced this pull request


          chore(data/finset/basic): move disjoint proofs earlier (#16436)

21631f0

This avoids repeating work for `disj_union`, and takes the stance that `disjoint` is part of the lattice API.



Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

bors bot commented Sep 23, 2022

Build failed (retrying...):

Run tests

bors bot pushed a commit that referenced this pull request


          chore(data/finset/basic): move disjoint proofs earlier (#16436)

896ad4b

This avoids repeating work for `disj_union`, and takes the stance that `disjoint` is part of the lattice API.



Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

bors bot commented Sep 23, 2022

Build failed (retrying...):

Build mathlib

bors bot pushed a commit that referenced this pull request


          chore(data/finset/basic): move disjoint proofs earlier (#16436)

ee80bcd

This avoids repeating work for `disj_union`, and takes the stance that `disjoint` is part of the lattice API.



Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

bors bot commented Sep 23, 2022

Build failed (retrying...):

Build mathlib

bors bot pushed a commit that referenced this pull request


          chore(data/finset/basic): move disjoint proofs earlier (#16436)

24b50bf

This avoids repeating work for `disj_union`, and takes the stance that `disjoint` is part of the lattice API.



Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

bors bot commented Sep 23, 2022

Pull request successfully merged into master.

Build succeeded:

bors bot changed the title ~~chore(data/finset/basic): move disjoint proofs earlier~~ [Merged by Bors] - chore(data/finset/basic): move disjoint proofs earlier

bors bot closed this

bors bot deleted the eric-wieser/tidy-finset-disjoint branch

September 23, 2022 14:45

eric-wieser mentioned this pull request

[Merged by Bors] - chore(data/finset/basic): Scope variables over smaller sections #16613

Closed

bottine pushed a commit that referenced this pull request


          chore(data/finset/basic): move disjoint proofs earlier (#16436)

This avoids repeating work for `disj_union`, and takes the stance that `disjoint` is part of the lattice API.



Co-authored-by: Kyle Miller <kmill31415@gmail.com>
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment