mathlib3

c42a9ad1 - chore(data/finsupp/basic): lemmas about sub and neg on filter and erase (#9228)