Commit 2024-05-01 11:05 9481bfd6
View on Github →chore: remove simp from Finset.filter_congr_decidable (#12576)
- This isn't used by simp in Mathlib
- It's doing something weird, replacing an arbitrary
DecidablePred
by the one found by inference (this might have been relevant before, but isn't now that we reuse more instances via unification). - The @[simp] had been removed on
bump/v4.8.0
, although I no longer remember why. Let's just get rid of it.