Commit 2021-12-08 05:53 4d56716d

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.