# Commit 2023-01-20 18:38 2445c98a

View on Github →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.