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
feat(*): backport Nat.le from Lean4 #8756
Conversation
The corresponding PR to mathlib is leanprover-community/mathlib#8756. Co-authored-by: Gabriel Ebner <gebner@gebner.org>
cases nat.eq_or_lt_of_le m_lt_n with h succ_m_lt_n, | ||
{ -- the difficult case at the squashed position: we first obtain the values from | ||
-- the sequence | ||
subst 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.
cases nat.eq_or_lt_of_le m_lt_n with h succ_m_lt_n, | |
{ -- the difficult case at the squashed position: we first obtain the values from | |
-- the sequence | |
subst h, | |
rcases m_lt_n.eq_or_lt with rfl|succ_m_lt_n, | |
{ -- the difficult case at the squashed position: we first obtain the values from | |
-- the sequence |
and similar below
Unfortunately when we made |
|
This is the companion PR to leanprover-community/lean#603, updating mathlib3 to use the definition of Nat.le preferred in Lean4.
It's not always smooth sailing, and in particular it's now more awkward to use
cases
orinduction
on inequalities innat
.If anyone sees a way to do this better, please let me know!
Until we merge the PR to Lean3 itself, this PR won't build, but it does appear to build locally!