Commit 2025-07-08 14:14 f1001e49

View on Github →

chore(Data/Set/Card): adjust naming and simp set (#26791) Renames:

  • Set.ncard_coe_Finset -> Set.ncard_coe_finset
  • Set.Nat.card_coe_set_eq -> Nat.card_coe_set_eq Additionally, make the latter simp, so that Nat.card of a coerced set to type is no longer simp-normal, and make ncard_univ simp so that Set.ncard univ is no longer simp-normal. The other simp changes in this PR are all for the simpNF linter, since a good chunk of simp lemmas are now provable.

Estimated changes

modified theorem Set.natCard_inv
modified theorem Set.natCard_smul_set
added theorem Nat.card_coe_set_eq
deleted theorem Set.Nat.card_coe_set_eq
modified theorem Set.ncard_coe
deleted theorem Set.ncard_coe_Finset
added theorem Set.ncard_coe_finset
modified theorem Set.ncard_univ
modified theorem Nat.card_univ
modified theorem Set.natCard_graphOn