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: port Order.OmegaCompletePartialOrder #1168
Conversation
rwbarton
commented
Dec 22, 2022
•
edited by github-actions
bot
edited by github-actions
bot
- depends on: [Merged by Bors] - chore: bump to nightly-2023-01-06 #1397
leanprover/lean4#1937 makes this too unpleasant for now. |
Hopefully fixed after the bump to nightly-2023-01-06. |
This PR/issue depends on:
|
simp only [inf_le_iff, hf c, hg c, ωSup_le_iff, ← forall_or_left, ← forall_or_right, | ||
Function.comp_apply, Chain.map_coe, OrderHom.orderBot] -- something broken here |
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.
It seems like inf_le_iff
no longer applies. Trying to force it gets me to a @SemilatticeInf.toHasInf β Lattice.toSemilatticeInf = @Lattice.toHasInf β LinearOrder.toLattice
goal.
Also the lemma now known as OrderHom.instHasInfOrderHomToPreorderToPartialOrder_inf_coe
is missing from the simp call
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 fixed this problem with inf_le_iff
no longer applying.
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.
otherwise lgtm
Co-authored-by: Eric Rodriguez <37984851+ericrbg@users.noreply.github.com>
Thanks 🎉 bors merge |
- [x] depends on: #1397 Co-authored-by: Heather Macbeth <25316162+hrmacbeth@users.noreply.github.com> Co-authored-by: Johan Commelin <johan@commelin.net> Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com> Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com>
Pull request successfully merged into master. Build succeeded:
|