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] - chore(*): golf using acc_lift₂_iff
and well_founded_lift₂_iff
#18526
Conversation
src/order/rel_iso/basic.lean
Outdated
/-- `quotient.out` as a relation embedding between the lift of a relation and the relation. -/ | ||
@[simps] noncomputable def _root_.quotient.out_rel_embedding [s : setoid α] {r : α → α → Prop} (H) : | ||
@[simps] noncomputable def _root_.quotient.out_rel_embedding {s : setoid α} {r : α → α → Prop} (H) : |
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 think arguably []
was better, as it matches how lift₂
is defined. Is this change actually needed to make the rest of this PR work?
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.
Yes. antisymm_rel.setoid
is not an instance.
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 pushed some primed versions of the lemmas using {}
to match the quotient.mk
/ quotient.mk'
distinction.
bors d+
✌️ negiizhao can now approve this pull request. To approve and merge a pull request, simply reply with |
bors r+ |
…8526) Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Pull request successfully merged into master. Build succeeded: |
acc_lift₂_iff
and well_founded_lift₂_iff
acc_lift₂_iff
and well_founded_lift₂_iff
There is a further attempt in #18128, but maybe this is enough for many cases now.