mathlib

2445c98a - fix(data/finsupp/basic): add missing `decidable` arguments in lemma statements (#18241)

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 `def`s 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.