mathlib3

feat(data/finsupp/basic): Lemmas regarding `finsupp.filter`

#17012

Open