Commit 2026-05-24 16:25 07c26b07

View on Github →

chore(Data/Set/Card): make s.ncard the simpNF of Fintype.card s (#39414) Untags coe_fintypeCard : ↑(Fintype.card s) = s.encard as @[simp], and instead tags

  • fintypeCard_eq_ncard : Fintype.card s = s.ncard
  • coe_ncard_eq_encard : ↑(s.ncard) = s.encard Then untags simp lemmas which are no longer simpNF because of this change; simpNF versions of some of them will be introduced in future PRs.

Estimated changes

modified theorem Set.coe_fintypeCard