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 Data.Nat.Multiplicity #2974
Conversation
Mathbin -> Mathlib fix certain import statements move "by" to end of line add import to Mathlib.lean
Mathlib/Data/Nat/Multiplicity.lean
Outdated
refine' binary_rec _ _ | ||
· contradiction | ||
refine' binaryRec _ _ | ||
· exact fun h => False.elim <| h rfl | ||
· intro b n ih h | ||
by_cases hn : n = 0 | ||
· subst hn | ||
simp at h | ||
simp [h, one_right h2.not_unit] |
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 is a non-terminal simp, right? Please replace it by a simp only
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.
That must have been from mathlib3 but it is fixed now.
Thanks! |
Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
Pull request successfully merged into master. Build succeeded:
|
Started but got pulled away. Feel free to jump in.