-
Notifications
You must be signed in to change notification settings - Fork 297
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
Fixing walks_and_trees branch #9983
Conversation
{ simp only [multiset.singleton_eq_singleton, multiset.count_eq_zero, multiset.mem_singleton], | ||
exact ne.symm hne, }, | ||
{ simp only [multiset.singleton_eq_cons, multiset.count_eq_zero, multiset.mem_singleton], | ||
simp, exact ne.symm hne, }, |
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.
You should try to avoid non-terminal simp
s. You can likely switch this proof to end in simpa using ne.symm hne
. Likely you can even make the whole proof simpa [multiset.singleton_eq_singleton, multiset.count_eq_zero, multiset.mem_singleton] using ne.symm hne
.
nat.succ_eq_add_one, this, set.mem_Union, nat.nat_zero_eq_zero, finset.coe_bUnion, | ||
finset.mem_univ, set.Union_true, list.nodup_nil, set.mem_set_of_eq, exists_imp_distrib, | ||
iff_false, finset.mem_coe, false_and | ||
], |
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.
Mathlib doesn't seem to ever put the simp lemmas on their own line like this. If you could rewrap the lines so it's in the following form, I'd appreciate it:
simp! only [...............................
.........................................
.........................................]
sym
typosmultiset.singleton_eq_singleton
tomultiset.singleton_eq_cons
is_rotated_append
(already enunciated and proved indata.list
)