mathlib3

b46190f9 - chore(data/finsupp): minor review (#4712)

chore(data/finsupp): minor review (#4712) * add a few lemmas about injectivity of `coe_fn` etc; * simplify definition of `finsupp.on_finset`; * replace the proof of `support_on_finset` by `rfl`; * make `finsupp.mem_support_on_finset` a `simp` lemma.