[Merged by Bors] - feat(Data/Set/Card): Fintype.card s = s.ncard

[SnirBroshi]

We have ↑(Fintype.card s) = s.encard but we don't yet have a theorem relating Fintype.card and Set.ncard.

This adds Fintype.card s = s.ncard for Fintype s, and also s.ncard = s.encard for Finite s.

---

(tagging simp is problematic since the aforementioned theorem (Set.coe_fintypeCard) is simp, and I'm not sure we should untag it)

[github-actions]

PR summary e120fe83a7

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ coe_ncard_eq_encard
+ fintypeCard_eq_ncard

You can run this locally as follows

## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

---

No changes to technical debt.

This script lives in the mathlib-ci repository. To run it locally, from your mathlib4 directory:

git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci
../mathlib-ci/scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[Vierkantor]

I agree with adding the lemma. This should probably be a @[simp] lemma, though. We can fix the simpNF linter by adding the following theorem:

variable (s) in
@[simp]
/-- `simpNF` form of `coe_fintypeCard`. -/
theorem ncard_eq_encard [Finite s] : s.ncard = s.encard := by
  have := Fintype.ofFinite s
  rw [← fintypeCard_eq_ncard, coe_fintypeCard]

and then removing the @[simp] from coe_fintypeCard.

(Note: this was the first proof I came up with, it might be simplifiable)

[b-mehta]

Tagging this simp may be a good idea, but it is a pretty big change, since it's declaring that Fintype.card ↑s is "bad". And that means that the lemmas here https://leanprover-community.github.io/mathlib4_docs/Mathlib/Data/Set/Finite/Basic.html#Cardinality should be viewed as deprecated (and the linter will yell at you until you un-simp them).
I'm 60% sure this is the right thing to do, but I think it could be wiser to make the simp change in a different PR, and keep this one as just adding the new lemma (which I'm 100% sure is the right thing to do).

[SnirBroshi]

With +31/-28 the linter is not angry anymore, though arguably we do want to add Set.ncard versions of the simp-lemmas that were untagged, and deprecate the old versions. Should the split be ("add the small lemma" + "change simpNF") + "add new Set.ncard simp lemmas" or should we postpone the simpNF changes to a new PR?

[Vierkantor]

I would say: this PR can add the lemma but not tag it as @[simp], and then we change simp-NF in the next PR.

[Vierkantor]

Thanks!

bors r+

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Lint style
• ci (staging) / Build
• ci (staging) / Post-Build Step
• ci (staging) / Post-CI job

[SnirBroshi]

this PR can add the lemma but not tag it as @[simp], and then we change simp-NF in the next PR.

simpNF PR: #39414