Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-02-23 06:48 ec36fc06

View on Github →

fix(data/set/finite): add decidable assumptions (#6264) Yury's rule of thumb https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/classicalize/near/224871122 says that we should have decidable instances here, because the statements of the lemmas need them (rather than the proofs). I'm making this PR to see if anything breaks.

Estimated changes

modified theorem set.card_ne_eq
modified theorem set.to_finset_compl
modified theorem set.to_finset_inter
modified theorem set.to_finset_ne_eq_erase
modified theorem set.to_finset_union