Commit 2022-08-19 16:44 aaf7dc2c

chore(data/multiset/basic): rename theorems, mark as simp (#15883) This PR does the following:

• rename coe_nil_eq_zero to coe_nil.
• rename singleton_eq_cons to cons_zero, flip direction, mark simp (we prefer {a} over a ::ₘ 0).
• add lemmas coe_singleton and singleton_eq_cons_iff.
• ditch singleton_coe in favor of cons_zero and coe_singleton.
• mark singleton_add, singleton_inj, nodup_singleton as simp.
• unmark count_singleton_self as simp, since it can now be solved automatically via count_eq_one_of_mem.