Commit 2024-05-01 13:16 7e5c6cb4
View on Github →chore: remove @[simp] from Fintype.card_fun (#12577)
On v4.8.0, Fintype.card_fun will no longer be a valid simp lemma, because the lhs will simplify via Fintype.card_pi. This PR cleans up pre-emptively.