Mathlib v3 is deprecated. Go to Mathlib v4

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 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.

Estimated changes