mathlib3

ee018175 - chore(data/set/basic): use `decidable_pred (∈ s)` instead of `decidable_pred s`. (#8211)

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.