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.

Estimated changes