mathlib3

ff5fa529 - chore(data/finsupp/basic): add coe_{neg,sub,smul} lemmas to match coe_{zero,add,fn_sum} (#6350)

chore(data/finsupp/basic): add coe_{neg,sub,smul} lemmas to match coe_{zero,add,fn_sum} (#6350) This also: * merges together `smul_apply'` and `smul_apply`, since the latter is just a special case of the former. * changes the implicitness of arguments to all of the `finsupp.*_apply` lemmas so that all the variables and none of the types are explicit The whitespace style here matches how `coe_add` is spaced.