Commit 2023-01-20 18:38 2445c98a

fix(data/finsupp/basic): add missing decidable arguments in lemma statements (#18241) The resulting lemmas are more general than they were before. In order to ensure that this doesn't regress again, open_locale classical is now also removed from these files. Instead, we use the approach of:

• Using the classical tactic in proofs
• Using by haveI := _; exact in definitions, as by classical; exact leaks classicality up to the end of the next section. In a few places this means that variables lines have to be repeated on defs as Lean doesn't look inside tactic blocks to work out which variables are used. I also switched some anonymous constructors for named constructors in order to make the proof / data distinction a little easier to see.