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: Order on the localization #3567
Conversation
Match leanprover-community/mathlib#18724 and leanprover-community/mathlib#18846 [`group_theory.monoid_localization`@`1f0096e6caa61e9c849ec2adbd227e960e9dff58`..`13b8e258f14bffb5def542aa78b803b0b80541aa`](https://leanprover-community.github.io/mathlib-port-status/file/group_theory/monoid_localization?range=1f0096e6caa61e9c849ec2adbd227e960e9dff58..13b8e258f14bffb5def542aa78b803b0b80541aa)
|
||
@[to_additive] | ||
theorem mk_left_injective (b : s) : Injective fun a => mk a b := fun c d h => by | ||
have : Nonempty s := ⟨b⟩ -- porting note: Needed to add this `have` |
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.
Do you know why? Did we misport a lemma and add this hypothesis unecessarily?
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.
No, I cannot find the lemma that uses it. It might be a matter of instance unification, again.
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 we're missing the fact that submonoids are inhabited (with 1) Nope, that's not it: lean3 can't find that either.
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.
In Lean3 this finds has_one.nonempty
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.
No fix in sight, then?
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 TC search just times out before it finds it
bors merge Thanks! |
Match leanprover-community/mathlib#18724 and leanprover-community/mathlib#18846 Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Pull request successfully merged into master. Build succeeded: |
Match leanprover-community/mathlib#18724 and leanprover-community/mathlib#18846 Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Match leanprover-community/mathlib#18724 and leanprover-community/mathlib#18846 Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Match leanprover-community/mathlib#18724 and leanprover-community/mathlib#18846 Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Match leanprover-community/mathlib#18724 and leanprover-community/mathlib#18846
group_theory.monoid_localization
@1f0096e6caa61e9c849ec2adbd227e960e9dff58
..13b8e258f14bffb5def542aa78b803b0b80541aa