[Merged by Bors] - chore: Don't simplify Odd n to ¬ Even n, but the other way around#16024
[Merged by Bors] - chore: Don't simplify Odd n to ¬ Even n, but the other way around#16024YaelDillies wants to merge 4 commits intomasterfrom
Odd n to ¬ Even n, but the other way around#16024Conversation
This is simply not simpler
PR summary 2a5ef0c35bImport changes for modified filesNo significant changes to the import graph Import changes for all files
|
grunweg
left a comment
There was a problem hiding this comment.
Thanks for doing this; I agree the new direction of the lemmas makes much more sense.
AIUI, this PR just flips the direction of these simp lemmas (but does not un-simp anything); can you please adjust the PR title to match this?
maintainer merge
| cases even_or_odd n with | ||
| | inl h => exact Or.inl ⟨h, even_iff_not_odd.mp h⟩ | ||
| | inr h => exact Or.inr ⟨h, odd_iff_not_even.mp h⟩ | ||
| | inl h => exact Or.inl ⟨h, not_odd_iff_even.2 h⟩ |
There was a problem hiding this comment.
This is minor, and not something I will insist on, but: I do find using .mp(r) clearer in such situations.
If we agree to disagree/not fuss about this as this is too minor, then please do not make such such unrelated changes.
There was a problem hiding this comment.
Oh that's just a consequence of the grep I've done. It would be a bit complicated now to automatically find all the places where this change was not
|
🚀 Pull request has been placed on the maintainer queue by grunweg. |
Odd n to ¬ Even nOdd n to ¬ Even n, but the other way around
…#16024) This is simply not simpler From LeanAPAP
|
Pull request successfully merged into master. Build succeeded: |
Odd n to ¬ Even n, but the other way aroundOdd n to ¬ Even n, but the other way around
…#16024) This is simply not simpler From LeanAPAP
…#16024) This is simply not simpler From LeanAPAP
…#16024) This is simply not simpler From LeanAPAP
This is simply not simpler
From LeanAPAP