Commit 2021-12-08 18:44 1d0bb865

fix(data/finsupp/basic): add missing decidable arguments (#10672) finsupp is classical, meaning that defs 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.