mathlib3

1d0bb865 - fix(data/finsupp/basic): add missing decidable arguments (#10672)

fix(data/finsupp/basic): add missing decidable arguments (#10672) `finsupp` is classical, meaning that `def`s should just use noncomputable decidable instances rather than taking arguments that make more work for mathematicians. However, this doesn't mean that lemma _statements_ should use noncomputable decidable instances, as this just makes the lemma less general and harder to apply (as shown by the `congr` removed elsewhere in the diff). These were found by removing `open_locale classical` from the top of the file, adding `by classical; exact` to some definitions, and then fixing the broken lemma statements. In future we should detect this type of mistake with a linter.