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.
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
[Merged by Bors] - feat(data/{finset,set}/basic): More insert
and erase
lemmas
#14675
Conversation
ha.to_finset = {a} := | ||
finset.ext $ by simp | ||
|
||
@[simp] lemma finite.to_finset_insert [decidable_eq α] {s : set α} {a : α} |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I don't think this lemma is an improvement over the removed one; I suspect this is a case where we want both versions, one for each direction of rewrite
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Same thought here, so I restored it but unsimped and primed.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This largely looks good, although I'm worried that some of these lemmas might already exist with different names
Indeed, |
Thanks! bors merge |
Pull request successfully merged into master. Build succeeded: |
insert
and erase
lemmasinsert
and erase
lemmas
Also turn
finset.disjoint_iff_disjoint_coe
around and changeset.finite.to_finset_insert
take(insert a s).finite
instead ofs.finite
.