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] - feat: List.append_cons_inj_of_not_mem #6856

Closed
wants to merge 14 commits into from
Closed

[Merged by Bors] - feat: List.append_cons_inj_of_not_mem #6856

wants to merge 14 commits into from

Conversation

madvorak
Copy link
Collaborator

@madvorak madvorak commented Aug 29, 2023 •
edited
Loading

@madvorak
Copy link
Collaborator Author

Not ready to merge! Please only review.

@madvorak
Copy link
Collaborator Author

Should I move lemma match_xYz to a different file, so that I can use linarith to make the proof shorter?

@madvorak madvorak added RFC Request for comment and removed awaiting-review labels Sep 11, 2023
@bors bors bot changed the base branch from master to ScottCarnahan/BinomialRing2 September 17, 2023 03:26
@semorrison semorrison changed the base branch from ScottCarnahan/BinomialRing2 to master September 17, 2023 12:06
@madvorak madvorak changed the title feat(Data/List): match_xYz feat(Data/List): append_singleton_append Oct 15, 2023
@madvorak madvorak changed the title feat(Data/List): append_singleton_append feat: List.append_singleton_append_inj_of_nmem Nov 2, 2023
@madvorak madvorak added the awaiting-author A reviewer has asked the author a question or requested changes label Nov 25, 2023
@madvorak madvorak added awaiting-review awaiting-CI and removed awaiting-author A reviewer has asked the author a question or requested changes RFC Request for comment labels Nov 26, 2023
@madvorak madvorak added the awaiting-author A reviewer has asked the author a question or requested changes label Nov 26, 2023
@madvorak @eric-wieser
Update Mathlib/Data/List/Basic.lean
c64986e 
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@madvorak madvorak removed the awaiting-author A reviewer has asked the author a question or requested changes label Nov 29, 2023
YaelDillies
YaelDillies reviewed Dec 12, 2023
View reviewed changes
Mathlib/Data/List/Basic.lean Outdated Show resolved Hide resolved
Mathlib/Data/List/Basic.lean Outdated Show resolved Hide resolved
Mathlib/Data/List/Basic.lean Outdated Show resolved Hide resolved
madvorak and others added 2 commits December 12, 2023 16:27
@madvorak @YaelDillies
Update Mathlib/Data/List/Basic.lean
888ecfe 
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
@madvorak
the same rename in the private lemma
25f0f9f
@urkud
Copy link
Member

urkud commented Jan 23, 2024

I'm going to golf this.

@urkud
Copy link
Member

urkud commented Jan 23, 2024

I don't think that naming lists x₁ etc follows our naming conventions. Also please add a docstring.

@urkud urkud added awaiting-author A reviewer has asked the author a question or requested changes t-logic Logic (model theory, set theory, etc) and removed awaiting-review labels Jan 23, 2024
@urkud urkud self-assigned this Jan 23, 2024
@madvorak
Copy link
Collaborator Author

I'm going to golf this.

Wow, that was shortened much much much more than I expected!!

@madvorak madvorak added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes labels Jan 24, 2024
@madvorak @YaelDillies
Update Mathlib/Data/List/Basic.lean
a07b326 
Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
@madvorak madvorak changed the title feat: List.append_singleton_append_inj_of_nmem feat: List.append_cons_inj_of_not_mem Jan 25, 2024
@urkud
Copy link
Member

urkud commented Jan 26, 2024

@eric-wieser What do you think about variable names here? Otherwise LGTM (I'm not merging because I wrote the current proof).

YaelDillies
YaelDillies approved these changes Jan 30, 2024
View reviewed changes
Copy link
Collaborator

@YaelDillies YaelDillies left a comment

Choose a reason for hiding this comment

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

The names of the lists are a bit weird but nothing better comes to mind.

maintainer merge

@github-actions GitHub Actions
Copy link

🚀 Pull request has been placed on the maintainer queue by YaelDillies.

@dupuisf
Copy link
Contributor

dupuisf commented Jan 30, 2024

bors r+

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Jan 30, 2024
mathlib-bors bot pushed a commit that referenced this pull request Jan 30, 2024
@madvorak @urkud
feat: List.append_cons_inj_of_not_mem (#6856)
1c09c19 
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
@mathlib-bors
Copy link
Contributor

mathlib-bors bot commented Jan 30, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: List.append_cons_inj_of_not_mem [Merged by Bors] - feat: List.append_cons_inj_of_not_mem Jan 30, 2024
@mathlib-bors mathlib-bors bot closed this Jan 30, 2024
@mathlib-bors mathlib-bors bot deleted the list3 branch January 30, 2024 20:42
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@YaelDillies YaelDillies YaelDillies approved these changes

@eric-wieser eric-wieser Awaiting requested review from eric-wieser

Assignees

@urkud urkud

Labels
ready-to-merge This PR has been sent to bors. t-logic Logic (model theory, set theory, etc)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
5 participants
@madvorak @urkud @dupuisf @eric-wieser @YaelDillies