feat: missing basic API lemmas for Nat.card, Fintype.card (#20131)

`card_sigma` existed for `Fintype.card` and I've added it for `Nat.card`. This version uses `Finite` instead of `Fintype` for the dependent type, for generality.

`card_univ` existed for `Nat.card` and I've added it for `Fintype.card`.

I've added `card_subtype_true` for both `Nat.card` and `Fintype.card`.

I've renamed `empty_card` -> `card_empty`

With `Fintype.card` rewrite lemmas, one has to be careful about the instance to avoid unifying with a non-defeq instance. This can be solved by taking the instance as a (normal) implicit parameter. However, it is not clear that this is really necessary.

Author: JovanGerb

Mathlib/Algebra/BigOperators/Expect.lean

@@ -409,7 +409,7 @@ lemma expect_const [Nonempty ι] (a : M) : 𝔼 _i : ι, a = a := Finset.expect_
 
 lemma expect_ite_zero (p : ι → Prop) [DecidablePred p] (h : ∀ i j, p i → p j → i = j) (a : M) :
     𝔼 i, ite (p i) a 0 = ite (∃ i, p i) (a /ℚ Fintype.card ι) 0 := by
-  simp [univ.expect_ite_zero p (by simpa using h), card_univ]
+  simp [univ.expect_ite_zero p (by simpa using h)]
 
 variable [DecidableEq ι]
 
@@ -418,16 +418,16 @@ variable [DecidableEq ι]
   simp [Finset.expect_ite_mem, dens]
 
 lemma expect_dite_eq (i : ι) (f : ∀ j, i = j → M) :
-    𝔼 j, (if h : i = j then f j h else 0) = f i rfl /ℚ card ι := by simp [card_univ]
+    𝔼 j, (if h : i = j then f j h else 0) = f i rfl /ℚ card ι := by simp
 
 lemma expect_dite_eq' (i : ι) (f : ∀ j, j = i → M) :
-    𝔼 j, (if h : j = i then f j h else 0) = f i rfl /ℚ card ι := by simp [card_univ]
+    𝔼 j, (if h : j = i then f j h else 0) = f i rfl /ℚ card ι := by simp
 
 lemma expect_ite_eq (i : ι) (f : ι → M) :
-    𝔼 j, (if i = j then f j else 0) = f i /ℚ card ι := by simp [card_univ]
+    𝔼 j, (if i = j then f j else 0) = f i /ℚ card ι := by simp
 
 lemma expect_ite_eq' (i : ι) (f : ι → M) :
-    𝔼 j, (if j = i then f j else 0) = f i /ℚ card ι := by simp [card_univ]
+    𝔼 j, (if j = i then f j else 0) = f i /ℚ card ι := by simp
 
 end AddCommMonoid
 

Mathlib/Algebra/Group/AddChar.lean

@@ -323,7 +323,7 @@ variable {A R : Type*} [AddGroup A] [Fintype A] [CommSemiring R] [IsDomain R]
 lemma sum_eq_ite (ψ : AddChar A R) [Decidable (ψ = 0)] :
     ∑ a, ψ a = if ψ = 0 then ↑(card A) else 0 := by
   split_ifs with h
-  · simp [h, card_univ]
+  · simp [h]
   obtain ⟨x, hx⟩ := ne_one_iff.1 h
   refine eq_zero_of_mul_eq_self_left hx ?_
   rw [Finset.mul_sum]

Mathlib/Analysis/FunctionalSpaces/SobolevInequality.lean

@@ -95,7 +95,7 @@ variable {p : ℝ}
     T μ p f univ x =
     ∫⁻ (x : ∀ i, A i), (f x ^ (1 - (#ι - 1 : ℝ) * p)
     * ∏ i : ι, (∫⁻ t : A i, f (update x i t) ∂(μ i)) ^ p) ∂(.pi μ) := by
-  simp [T, lmarginal_univ, lmarginal_singleton, card_univ]
+  simp [T, lmarginal_singleton]
 
 @[simp] lemma T_empty (f : (∀ i, A i) → ℝ≥0∞) (x : ∀ i, A i) :
     T μ p f ∅ x = f x ^ (1 + p) := by
@@ -320,7 +320,7 @@ theorem lintegral_pow_le_pow_lintegral_fderiv_aux [Fintype ι]
     _ = ∫⁻ x, ∏ _i : ι, ‖u x‖ₑ ^ (1 / (#ι - 1 : ℝ)) := by
         -- express the left-hand integrand as a product of identical factors
         congr! 2 with x
-        simp_rw [prod_const, card_univ]
+        simp_rw [prod_const]
         norm_cast
     _ ≤ ∫⁻ x, ∏ i, (∫⁻ xᵢ, ‖fderiv ℝ u (update x i xᵢ)‖ₑ) ^ ((1 : ℝ) / (#ι - 1 : ℝ)) := ?_
     _ ≤ (∫⁻ x, ‖fderiv ℝ u x‖ₑ) ^ p := by

Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean

@@ -373,7 +373,7 @@ variable [Nonempty α]
     if t ⊆ s then (card α - #s : ℚ) / ((card α - #t) * (card α).choose #t) else 0 := by
     rintro t
     simp_rw [truncatedSup_singleton, le_iff_subset]
-    split_ifs <;> simp [card_univ]
+    split_ifs <;> simp
   simp_rw [← sub_eq_of_eq_add (Fintype.sum_div_mul_card_choose_card α), eq_sub_iff_add_eq,
     ← eq_sub_iff_add_eq', supSum, ← sum_sub_distrib, ← sub_div]
   rw [sum_congr rfl fun t _ ↦ this t, sum_ite, sum_const_zero, add_zero, filter_subset_univ,

Mathlib/Data/Fintype/Card.lean

@@ -347,6 +347,20 @@ theorem Fintype.card_lex (α : Type*) [Fintype α] : Fintype.card (Lex α) = Fin
 @[simp] lemma Fintype.card_additive (α : Type*) [Fintype α] : card (Additive α) = card α :=
   Finset.card_map _
 
+-- Note: The extra hypothesis `h` is there so that the rewrite lemma applies,
+-- no matter what instance of `Fintype (Set.univ : Set α)` is used.
+@[simp]
+theorem Fintype.card_setUniv [Fintype α] {h : Fintype (Set.univ : Set α)} :
+    @Fintype.card (Set.univ : Set α) h = Fintype.card α := by
+  apply Fintype.card_of_finset'
+  simp
+
+@[simp]
+theorem Fintype.card_subtype_true [Fintype α] {h : Fintype {_a : α // True}} :
+    @Fintype.card {_a // True} h = Fintype.card α := by
+  apply Fintype.card_of_subtype
+  simp
+
 /-- Given that `α ⊕ β` is a fintype, `α` is also a fintype. This is non-computable as it uses
 that `Sum.inl` is an injection, but there's no clear inverse if `α` is empty. -/
 noncomputable def Fintype.sumLeft {α β} [Fintype (α ⊕ β)] : Fintype α :=

Mathlib/Data/Set/Finite/Basic.lean

@@ -728,19 +728,18 @@ end
 
 /-! ### Cardinality -/
 
-theorem empty_card : Fintype.card (∅ : Set α) = 0 :=
+theorem card_empty : Fintype.card (∅ : Set α) = 0 :=
   rfl
 
-theorem empty_card' {h : Fintype.{u} (∅ : Set α)} : @Fintype.card (∅ : Set α) h = 0 := by
-  simp
+@[deprecated (since := "2025-02-05")] alias empty_card := card_empty
 
 theorem card_fintypeInsertOfNotMem {a : α} (s : Set α) [Fintype s] (h : a ∉ s) :
     @Fintype.card _ (fintypeInsertOfNotMem s h) = Fintype.card s + 1 := by
   simp [fintypeInsertOfNotMem, Fintype.card_ofFinset]
 
 @[simp]
 theorem card_insert {a : α} (s : Set α) [Fintype s] (h : a ∉ s)
-    {d : Fintype.{u} (insert a s : Set α)} : @Fintype.card _ d = Fintype.card s + 1 := by
+    {d : Fintype (insert a s : Set α)} : @Fintype.card _ d = Fintype.card s + 1 := by
   rw [← card_fintypeInsertOfNotMem s h]; congr!
 
 theorem card_image_of_inj_on {s : Set α} [Fintype s] {f : α → β} [Fintype (f '' s)]

Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean

@@ -252,7 +252,7 @@ theorem det_smul (A : Matrix n n R) (c : R) : det (c • A) = c ^ Fintype.card n
   calc
     det (c • A) = det ((diagonal fun _ => c) * A) := by rw [smul_eq_diagonal_mul]
     _ = det (diagonal fun _ => c) * det A := det_mul _ _
-    _ = c ^ Fintype.card n * det A := by simp [card_univ]
+    _ = c ^ Fintype.card n * det A := by simp
 
 @[simp]
 theorem det_smul_of_tower {α} [Monoid α] [DistribMulAction α R] [IsScalarTower α R R]

Mathlib/ModelTheory/Basic.lean

@@ -107,9 +107,11 @@ instance isAlgebraic_sum [L.IsAlgebraic] [L'.IsAlgebraic] : IsAlgebraic (L.sum L
   fun _ => instIsEmptySum
 
 @[simp]
-theorem empty_card : Language.empty.card = 0 := by simp only [card, mk_sum, mk_sigma, mk_eq_zero,
+theorem card_empty : Language.empty.card = 0 := by simp only [card, mk_sum, mk_sigma, mk_eq_zero,
   sum_const, mk_eq_aleph0, lift_id', mul_zero, add_zero]
 
+@[deprecated (since := "2025-02-05")] alias empty_card := card_empty
+
 instance isEmpty_empty : IsEmpty Language.empty.Symbols := by
   simp only [Language.Symbols, isEmpty_sum, isEmpty_sigma]
   exact ⟨fun _ => inferInstance, fun _ => inferInstance⟩

Mathlib/NumberTheory/NumberField/Units/DirichletTheorem.lean

@@ -151,7 +151,7 @@ theorem log_le_of_logEmbedding_le {r : ℝ} {x : (𝓞 K)ˣ} (hr : 0 ≤ r)
         (fun w _ => logEmbedding_component_le hr h w)).trans ?_
       rw [nsmul_eq_mul]
       refine mul_le_mul ?_ le_rfl hr (Fintype.card (InfinitePlace K)).cast_nonneg
-      simp [card_univ]
+      simp
   · have hyp := logEmbedding_component_le hr h ⟨w, hw⟩
     rw [logEmbedding_component, abs_mul, Nat.abs_cast] at hyp
     refine (le_trans ?_ hyp).trans ?_

Mathlib/SetTheory/Cardinal/Finite.lean

@@ -199,6 +199,10 @@ theorem card_eq_two_iff : Nat.card α = 2 ↔ ∃ x y : α, x ≠ y ∧ {x, y} =
 theorem card_eq_two_iff' (x : α) : Nat.card α = 2 ↔ ∃! y, y ≠ x :=
   toNat_eq_ofNat.trans (mk_eq_two_iff' x)
 
+@[simp]
+theorem card_subtype_true : Nat.card {_a : α // True} = Nat.card α :=
+  card_congr <| Equiv.subtypeUnivEquiv fun _ => trivial
+
 @[simp]
 theorem card_sum [Finite α] [Finite β] : Nat.card (α ⊕ β) = Nat.card α + Nat.card β := by
   have := Fintype.ofFinite α
@@ -217,6 +221,11 @@ theorem card_ulift (α : Type*) : Nat.card (ULift α) = Nat.card α :=
 theorem card_plift (α : Type*) : Nat.card (PLift α) = Nat.card α :=
   card_congr Equiv.plift
 
+theorem card_sigma {β : α → Type*} [Fintype α] [∀ a, Finite (β a)] :
+    Nat.card (Sigma β) = ∑ a, Nat.card (β a) := by
+  letI _ (a : α) : Fintype (β a) := Fintype.ofFinite (β a)
+  simp_rw [Nat.card_eq_fintype_card, Fintype.card_sigma]
+
 theorem card_pi {β : α → Type*} [Fintype α] : Nat.card (∀ a, β a) = ∏ a, Nat.card (β a) := by
   simp_rw [Nat.card, mk_pi, prod_eq_of_fintype, toNat_lift, map_prod]