mathlib3

4d56716d - fix(data/finsupp/basic): add missing decidable argument (#10649)

fix(data/finsupp/basic): add missing decidable argument (#10649) While `finsupp.erase` is classical and requires no decidability, `finset.erase` is not so. Without this argument, this lemma does not apply in the general case, and introduces mismatching decidable instances. With it, a `congr` is no longer needed elsewhere in mathlib.