Commit 2024-05-14 21:45 7a69696d
View on Github →chore(Data.Finset): un-@[simp] filter_{true,false}_of_mem (#12907)
These are okay @[simp] lemmas in principle but sometimes discharging the hypothesis is very expensive.
This PR adds some extra @[simp] lemmas instead; those should reduce the impact of the change quite a lot.
Zulip thread: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Near-timeout.20in.20.60mulEnergy_card_filter.60