Skip to content
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: Make Set/Finset lemmas match lattice lemma names #7378

Closed
wants to merge 3 commits into from
Closed

[Merged by Bors] - chore: Make Set/Finset lemmas match lattice lemma names #7378

wants to merge 3 commits into from

Conversation

YaelDillies
Copy link
Collaborator

Rename union_eq_left_iff_subset to union_eq_left to match sup_eq_left. Similarly for the right and inter versions.

Open in Gitpod

@YaelDillies YaelDillies added the awaiting-review The author would like community review of the PR label Sep 27, 2023
@YaelDillies YaelDillies removed the request for review from int-y1 September 27, 2023 14:38
eric-wieser
eric-wieser approved these changes Sep 28, 2023
View reviewed changes
Copy link
Member

@eric-wieser eric-wieser left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

These renames look reasonable, thanks! Thanks for not renaming too many lemmas at once.

Since this is somewhat bike-sheddy, I'll let someone else make the final call.

maintainer merge

@github-actions
Copy link

🚀 Pull request has been placed on the maintainer queue by eric-wieser.

jcommelin
jcommelin reviewed Sep 29, 2023
View reviewed changes
Copy link
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks 🎉

bors merge

@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review The author would like community review of the PR labels Sep 29, 2023
bors bot pushed a commit that referenced this pull request Sep 29, 2023
@YaelDillies
chore: Make Set/Finset lemmas match lattice lemma names (#7378)
54ed55f 
Rename `union_eq_left_iff_subset` to `union_eq_left` to match `sup_eq_left`. Similarly for the `right` and `inter` versions.
@bors
Copy link

bors bot commented Sep 29, 2023

Build failed:

@jcommelin
Copy link
Member

bors d+

@bors
Copy link

bors bot commented Sep 30, 2023

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

@YaelDillies
Copy link
Collaborator Author

bors merge

bors bot pushed a commit that referenced this pull request Oct 1, 2023
@YaelDillies
chore: Make Set/Finset lemmas match lattice lemma names (#7378)
aef0410 
Rename `union_eq_left_iff_subset` to `union_eq_left` to match `sup_eq_left`. Similarly for the `right` and `inter` versions.
@bors
Copy link

bors bot commented Oct 1, 2023

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

@bors bors bot changed the title chore: Make Set/Finset lemmas match lattice lemma names [Merged by Bors] - chore: Make Set/Finset lemmas match lattice lemma names Oct 1, 2023
@bors bors bot closed this Oct 1, 2023
@bors bors bot deleted the inter_eq_left branch October 1, 2023 13:37
eric-wieser
eric-wieser reviewed Oct 7, 2023
View reviewed changes
Mathlib/Data/Set/Basic.lean
sup_eq_right
#align set.union_eq_right_iff_subset Set.union_eq_right_iff_subset
#align set.union_eq_right Set.union_eq_right
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Note that this incorrectly changed the lean3 name, but #7529 fixed it.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I tried to pay attention not to do that, but apparently not enough 😦

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

@eric-wieser eric-wieser eric-wieser approved these changes

@jcommelin jcommelin jcommelin left review comments

Assignees
No one assigned
Labels
delegated ready-to-merge This PR has been sent to bors.
Projects
No open projects
Discrete correlation inequalities
Status: Merged
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
4 participants
@YaelDillies @jcommelin @eric-wieser @leanprover-community-mathlib4-bot