Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-07-09 13:36 ee018175

View on Github →

chore(data/set/basic): use decidable_pred (∈ s) instead of decidable_pred s. (#8211) The latter exploits the fact that sets are functions to Prop, and is an annoying form as lemmas are never stated about it. In future we should consider removing the set.decidable_mem instance which encourages this misuse. Making this change reveals a collection of pointless decidable arguments requiring that finset membership be decidable; something which is always true anyway. Two proofs in data/pequiv caused a crash inside the C++ portion of the finish tactic; it was easier to just write the simple proofs manually than to debug the C++ code.

Estimated changes