feat(Data/Set/Card): Fintype.card s = s.ncard (leanprover-community#38426)

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`.

Author: SnirBroshi

Mathlib/Data/Set/Card.lean

@@ -589,6 +589,10 @@ theorem ncard_def (s : Set α) : s.ncard = ENat.toNat s.encard := rfl
 theorem Finite.cast_ncard_eq (hs : s.Finite) : s.ncard = s.encard := by
   rwa [ncard, ENat.coe_toNat_eq_self, ne_eq, encard_eq_top_iff, Set.Infinite, not_not]
 
+variable (s) in
+theorem coe_ncard_eq_encard [Finite s] : s.ncard = s.encard :=
+  s.toFinite.cast_ncard_eq
+
 lemma ncard_le_encard (s : Set α) : s.ncard ≤ s.encard := ENat.coe_toNat_le_self _
 
 @[simp] theorem _root_.Nat.card_coe_set_eq (s : Set α) : Nat.card s = s.ncard := rfl
@@ -602,6 +606,10 @@ theorem ncard_eq_toFinset_card' (s : Set α) [Fintype s] :
     s.ncard = s.toFinset.card := by
   simp [← _root_.Nat.card_coe_set_eq, Nat.card_eq_fintype_card]
 
+variable (s) in
+theorem fintypeCard_eq_ncard [Fintype s] : Fintype.card s = s.ncard := by
+  rw [ncard_eq_toFinset_card', toFinset_card]
+
 lemma cast_ncard {s : Set α} (hs : s.Finite) :
     (s.ncard : Cardinal) = Cardinal.mk s := @Nat.cast_card _ hs