Commit 2021-02-04 18:03 b98b5f6b

chore(data/dfinsupp): add simp lemmas about sum_add_hom, remove commutativity requirement (#5939) Note that dfinsupp.sum_add_hom and dfinsupp.sum are not defeq, so its valuable to repeat these lemmas. The former is often easier to work with because there are no decidability requirements to juggle on equality with zero. dfinsupp.single_eq_of_sigma_eq was a handy lemma for constructing a term-mode proof of dfinsupp.single equality. A lot of the lemmas about lift_add_hom have to be repeated for sum_add_hom because the former simplifies to the latter before its lemmas get a chance to apply. At least the proofs can be reused.