Mathlib: Nat.card vs Fintype.card — which to state with, how to convert, and what simp does

Checked on Mathlib v4.35.0.

**Prefer Nat.card in statements.** It takes no instance argument, so no Decidable/Fintype instance-mismatch errors (the classic exact h failing because Subtype.fintype was built from a different DecidablePred). Group theory is stated with it: Subgroup.index H = Nat.card (G ⧸ H), Subgroup.card_mul_index : Nat.card H * H.index = Nat.card G, Subgroup.card_subgroup_dvd_card, Sylow.card_eq_multiplicity, card_sylow_modEq_one. Several need no finiteness at all because Nat.card of an infinite type is 0: orderOf_dvd_natCard (x : G) : orderOf x ∣ Nat.card G (vs orderOf_dvd_card needing [Fintype G]).

**Converting:** Nat.card_eq_fintype_card : Nat.card α = Fintype.card α (simp lemma) and Fintype.card_eq_nat_card (works for *any* Fintype instance, so rw [Fintype.card_eq_nat_card] at h ⊢ kills instance mismatches). Sets/Finsets: Nat.card_coe_set_eq : Nat.card s = s.ncard, Nat.card_eq_finsetCard (s : Finset α) : Nat.card s = s.card, Nat.card_eq_card_toFinset. Structural: Nat.card_congr (e : α ≃ β), Nat.card_prod, Nat.card_sum/Nat.card_fun (need [Finite α]), Nat.card_fin, Nat.card_zmod, Nat.card_pos ([Nonempty α] [Finite α]), Nat.card_eq_zero_of_infinite.

**simp trap:** with a Fintype instance around, simp rewrites Nat.card to Fintype.card and then stops: Nat.card {x // p x} = (univ.filter p).card is not closed by simp (and Fintype.card {x // p x} = … gives 'simp made no progress'). Use rw [Nat.card_eq_fintype_card, Fintype.card_subtype] or Nat.subtype_card _ (by simp). There is no Nat.card_subtype.