From f922a5780847f8c30e13a69005e2e06b0febea03 Mon Sep 17 00:00:00 2001 From: KryptosAI <140749029+KryptosAI@users.noreply.github.com> Date: Wed, 18 Mar 2026 13:20:24 -0700 Subject: [PATCH 1/3] chore(Data/Finset/Card): rename `pred_card_le_card_erase` to `sub_one_card_le_card_erase` The name `pred_card_le_card_erase` suggests `Nat.pred` but the statement uses `- 1` (i.e., `Nat.sub 1`). Rename to `sub_one_card_le_card_erase` to match the actual statement. A deprecated alias is added for backwards compatibility. Updates downstream references in Powerset.lean, SubsetSum.lean, and EraseLead.lean. Addresses part of #21584. --- Mathlib/Algebra/Polynomial/EraseLead.lean | 2 +- Mathlib/Combinatorics/Additive/SubsetSum.lean | 2 +- Mathlib/Data/Finset/Card.lean | 4 +++- Mathlib/Data/Finset/Powerset.lean | 2 +- 4 files changed, 6 insertions(+), 4 deletions(-) diff --git a/Mathlib/Algebra/Polynomial/EraseLead.lean b/Mathlib/Algebra/Polynomial/EraseLead.lean index f724f76c61c19d..9be098f742fa08 100644 --- a/Mathlib/Algebra/Polynomial/EraseLead.lean +++ b/Mathlib/Algebra/Polynomial/EraseLead.lean @@ -80,7 +80,7 @@ theorem self_sub_C_mul_X_pow {R : Type*} [Ring R] (f : R[X]) : theorem eraseLead_ne_zero (f0 : 2 ≤ #f.support) : eraseLead f ≠ 0 := by rw [Ne, ← card_support_eq_zero, eraseLead_support] exact - (zero_lt_one.trans_le <| (tsub_le_tsub_right f0 1).trans Finset.pred_card_le_card_erase).ne.symm + (zero_lt_one.trans_le <| (tsub_le_tsub_right f0 1).trans Finset.sub_one_card_le_card_erase).ne.symm theorem lt_natDegree_of_mem_eraseLead_support {a : ℕ} (h : a ∈ (eraseLead f).support) : a < f.natDegree := by diff --git a/Mathlib/Combinatorics/Additive/SubsetSum.lean b/Mathlib/Combinatorics/Additive/SubsetSum.lean index 530007ec7ec027..0cc5c6c36129e3 100644 --- a/Mathlib/Combinatorics/Additive/SubsetSum.lean +++ b/Mathlib/Combinatorics/Additive/SubsetSum.lean @@ -106,7 +106,7 @@ theorem card_succ_choose_two_lt_card_subsetSum_of_pos (A_pos : ∀ x ∈ A, 0 < theorem card_choose_two_lt_card_subsetSum_of_nonneg (A_pos : ∀ x ∈ A, 0 ≤ x) : (#A).choose 2 < #A.subsetSum := by calc (#A).choose 2 - _ ≤ (#(A.erase 0) + 1).choose 2 := by grw [tsub_le_iff_right.1 <| pred_card_le_card_erase] + _ ≤ (#(A.erase 0) + 1).choose 2 := by grw [tsub_le_iff_right.1 <| sub_one_card_le_card_erase] _ < #(A.erase 0).subsetSum := card_succ_choose_two_lt_card_subsetSum_of_pos fun x hx => (A_pos x (mem_of_mem_erase hx)).lt_of_ne (ne_of_mem_erase hx).symm diff --git a/Mathlib/Data/Finset/Card.lean b/Mathlib/Data/Finset/Card.lean index d1c2c1e36ea902..e35c8ca4713bfd 100644 --- a/Mathlib/Data/Finset/Card.lean +++ b/Mathlib/Data/Finset/Card.lean @@ -153,7 +153,9 @@ theorem card_erase_lt_of_mem : a ∈ s → #(s.erase a) < #s := theorem card_erase_le : #(s.erase a) ≤ #s := Multiset.card_erase_le -theorem pred_card_le_card_erase : #s - 1 ≤ #(s.erase a) := by grind +theorem sub_one_card_le_card_erase : #s - 1 ≤ #(s.erase a) := by grind + +@[deprecated (since := "2026-03-18")] alias pred_card_le_card_erase := sub_one_card_le_card_erase /-- If `a ∈ s` is known, see also `Finset.card_erase_of_mem` and `Finset.erase_eq_of_notMem`. -/ theorem card_erase_eq_ite : #(s.erase a) = if a ∈ s then #s - 1 else #s := diff --git a/Mathlib/Data/Finset/Powerset.lean b/Mathlib/Data/Finset/Powerset.lean index d37121600efa7e..ee1930b8a85b5f 100644 --- a/Mathlib/Data/Finset/Powerset.lean +++ b/Mathlib/Data/Finset/Powerset.lean @@ -285,7 +285,7 @@ theorem powersetCard_sup [DecidableEq α] (u : Finset α) (n : ℕ) (hn : n < u. intro x hx simp only [mem_biUnion, id] obtain ⟨t, ht⟩ : ∃ t, t ∈ powersetCard n (u.erase x) := powersetCard_nonempty.2 - (le_trans (Nat.le_sub_one_of_lt hn) pred_card_le_card_erase) + (le_trans (Nat.le_sub_one_of_lt hn) sub_one_card_le_card_erase) refine ⟨insert x t, ?_, mem_insert_self _ _⟩ rw [← insert_erase hx, powersetCard_succ_insert (notMem_erase _ _)] exact mem_union_right _ (mem_image_of_mem _ ht) From b1348bbd33b77b2198071e3d6d4185c39048d386 Mon Sep 17 00:00:00 2001 From: William Weishuhn Date: Wed, 18 Mar 2026 16:39:14 -0700 Subject: [PATCH 2/3] style: fix line exceeding 100 character limit in EraseLead.lean Co-Authored-By: Claude Opus 4.6 (1M context) --- Mathlib/Algebra/Polynomial/EraseLead.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Mathlib/Algebra/Polynomial/EraseLead.lean b/Mathlib/Algebra/Polynomial/EraseLead.lean index 9be098f742fa08..229cebe692bacc 100644 --- a/Mathlib/Algebra/Polynomial/EraseLead.lean +++ b/Mathlib/Algebra/Polynomial/EraseLead.lean @@ -80,7 +80,8 @@ theorem self_sub_C_mul_X_pow {R : Type*} [Ring R] (f : R[X]) : theorem eraseLead_ne_zero (f0 : 2 ≤ #f.support) : eraseLead f ≠ 0 := by rw [Ne, ← card_support_eq_zero, eraseLead_support] exact - (zero_lt_one.trans_le <| (tsub_le_tsub_right f0 1).trans Finset.sub_one_card_le_card_erase).ne.symm + (zero_lt_one.trans_le <| + (tsub_le_tsub_right f0 1).trans Finset.sub_one_card_le_card_erase).ne.symm theorem lt_natDegree_of_mem_eraseLead_support {a : ℕ} (h : a ∈ (eraseLead f).support) : a < f.natDegree := by From 0d4ae075695e3f9d0d8e14cb1d2cc7bb70354ee7 Mon Sep 17 00:00:00 2001 From: William Weishuhn Date: Wed, 1 Apr 2026 18:32:39 -0700 Subject: [PATCH 3/3] refactor: align Finset card lemma names with statements --- Mathlib/Algebra/Polynomial/EraseLead.lean | 2 +- Mathlib/Combinatorics/Additive/SubsetSum.lean | 2 +- .../Combinatorics/SetFamily/AhlswedeZhang.lean | 2 +- Mathlib/Combinatorics/SetFamily/Shadow.lean | 4 ++-- Mathlib/Data/Finset/Card.lean | 18 +++++++++++------- Mathlib/Data/Finset/Powerset.lean | 2 +- Mathlib/Data/Set/Card.lean | 2 +- Mathlib/GroupTheory/Perm/Support.lean | 2 +- Mathlib/RingTheory/Ideal/Operations.lean | 2 +- 9 files changed, 20 insertions(+), 16 deletions(-) diff --git a/Mathlib/Algebra/Polynomial/EraseLead.lean b/Mathlib/Algebra/Polynomial/EraseLead.lean index 229cebe692bacc..55ec5038359457 100644 --- a/Mathlib/Algebra/Polynomial/EraseLead.lean +++ b/Mathlib/Algebra/Polynomial/EraseLead.lean @@ -81,7 +81,7 @@ theorem eraseLead_ne_zero (f0 : 2 ≤ #f.support) : eraseLead f ≠ 0 := by rw [Ne, ← card_support_eq_zero, eraseLead_support] exact (zero_lt_one.trans_le <| - (tsub_le_tsub_right f0 1).trans Finset.sub_one_card_le_card_erase).ne.symm + (tsub_le_tsub_right f0 1).trans Finset.card_sub_one_le_card_erase).ne.symm theorem lt_natDegree_of_mem_eraseLead_support {a : ℕ} (h : a ∈ (eraseLead f).support) : a < f.natDegree := by diff --git a/Mathlib/Combinatorics/Additive/SubsetSum.lean b/Mathlib/Combinatorics/Additive/SubsetSum.lean index 0cc5c6c36129e3..51ab9e8aab5ab7 100644 --- a/Mathlib/Combinatorics/Additive/SubsetSum.lean +++ b/Mathlib/Combinatorics/Additive/SubsetSum.lean @@ -106,7 +106,7 @@ theorem card_succ_choose_two_lt_card_subsetSum_of_pos (A_pos : ∀ x ∈ A, 0 < theorem card_choose_two_lt_card_subsetSum_of_nonneg (A_pos : ∀ x ∈ A, 0 ≤ x) : (#A).choose 2 < #A.subsetSum := by calc (#A).choose 2 - _ ≤ (#(A.erase 0) + 1).choose 2 := by grw [tsub_le_iff_right.1 <| sub_one_card_le_card_erase] + _ ≤ (#(A.erase 0) + 1).choose 2 := by grw [tsub_le_iff_right.1 <| card_sub_one_le_card_erase] _ < #(A.erase 0).subsetSum := card_succ_choose_two_lt_card_subsetSum_of_pos fun x hx => (A_pos x (mem_of_mem_erase hx)).lt_of_ne (ne_of_mem_erase hx).symm diff --git a/Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean b/Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean index 03901c0816c146..51dd93b77ce8aa 100644 --- a/Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean +++ b/Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean @@ -419,7 +419,7 @@ lemma supSum_of_univ_notMem (h𝒜₁ : 𝒜.Nonempty) (h𝒜₂ : univ ∉ 𝒜 simpa [eq_comm] using h𝒜₂ cases m · cases h𝒜₁.card_pos.ne hm - obtain ⟨s, 𝒜, hs, rfl, rfl⟩ := card_eq_succ.1 hm.symm + obtain ⟨s, 𝒜, hs, rfl, rfl⟩ := card_eq_add_one.1 hm.symm have h𝒜 : 𝒜.Nonempty := by by_contra! rfl; simp at h𝒜₃ rw [insert_eq, eq_sub_of_add_eq (supSum_union_add_supSum_infs _ _), singleton_infs, supSum_singleton (ne_of_mem_of_not_mem (mem_insert_self _ _) h𝒜₂), ih, ih, add_sub_cancel_right] diff --git a/Mathlib/Combinatorics/SetFamily/Shadow.lean b/Mathlib/Combinatorics/SetFamily/Shadow.lean index 80bdb4beebce16..0337ea0fdc149d 100644 --- a/Mathlib/Combinatorics/SetFamily/Shadow.lean +++ b/Mathlib/Combinatorics/SetFamily/Shadow.lean @@ -123,7 +123,7 @@ lemma mem_shadow_iterate_iff_exists_card : induction k generalizing t with | zero => simp | succ k ih => - simp only [mem_shadow_iff_insert_mem, ih, Function.iterate_succ_apply', card_eq_succ] + simp only [mem_shadow_iff_insert_mem, ih, Function.iterate_succ_apply', card_eq_add_one] aesop /-- `t ∈ ∂^k 𝒜` iff `t` is exactly `k` elements less than something from `𝒜`. @@ -234,7 +234,7 @@ lemma mem_upShadow_iterate_iff_exists_card : induction k generalizing t with | zero => simp | succ k ih => - simp only [mem_upShadow_iff_erase_mem, ih, Function.iterate_succ_apply', card_eq_succ, + simp only [mem_upShadow_iff_erase_mem, ih, Function.iterate_succ_apply', card_eq_add_one, subset_erase, erase_sdiff_comm, ← sdiff_insert] constructor · rintro ⟨a, hat, u, rfl, ⟨hut, hau⟩, htu⟩ diff --git a/Mathlib/Data/Finset/Card.lean b/Mathlib/Data/Finset/Card.lean index e35c8ca4713bfd..8e30cf38d8a1d5 100644 --- a/Mathlib/Data/Finset/Card.lean +++ b/Mathlib/Data/Finset/Card.lean @@ -153,9 +153,10 @@ theorem card_erase_lt_of_mem : a ∈ s → #(s.erase a) < #s := theorem card_erase_le : #(s.erase a) ≤ #s := Multiset.card_erase_le -theorem sub_one_card_le_card_erase : #s - 1 ≤ #(s.erase a) := by grind +theorem card_sub_one_le_card_erase : #s - 1 ≤ #(s.erase a) := by grind -@[deprecated (since := "2026-03-18")] alias pred_card_le_card_erase := sub_one_card_le_card_erase +@[deprecated (since := "2026-04-01")] alias pred_card_le_card_erase := card_sub_one_le_card_erase +@[deprecated (since := "2026-04-01")] alias sub_one_card_le_card_erase := card_sub_one_le_card_erase /-- If `a ∈ s` is known, see also `Finset.card_erase_of_mem` and `Finset.erase_eq_of_notMem`. -/ theorem card_erase_eq_ite : #(s.erase a) = if a ∈ s then #s - 1 else #s := @@ -740,7 +741,7 @@ lemma exists_of_one_lt_card_pi {ι : Type*} {α : ι → Type*} [∀ i, Decidabl obtain rfl | hne := eq_or_ne (a2 i) ai exacts [⟨a1, h1, hne⟩, ⟨a2, h2, hne⟩] -theorem card_eq_succ_iff_cons : +theorem card_eq_add_one_iff_cons : #s = n + 1 ↔ ∃ a t, ∃ (h : a ∉ t), cons a t h = s ∧ #t = n := ⟨cons_induction_on s (by simp) fun a s _ _ _ => ⟨a, s, by simp_all⟩, fun ⟨a, t, _, hs, _⟩ => by simpa [← hs]⟩ @@ -748,29 +749,32 @@ theorem card_eq_succ_iff_cons : section DecidableEq variable [DecidableEq α] -theorem card_eq_succ : #s = n + 1 ↔ ∃ a t, a ∉ t ∧ insert a t = s ∧ #t = n := +theorem card_eq_add_one : #s = n + 1 ↔ ∃ a t, a ∉ t ∧ insert a t = s ∧ #t = n := ⟨fun h => let ⟨a, has⟩ := card_pos.mp (h.symm ▸ Nat.zero_lt_succ _ : 0 < #s) ⟨a, s.erase a, s.notMem_erase a, insert_erase has, by simp only [h, card_erase_of_mem has, Nat.add_sub_cancel_right]⟩, fun ⟨_, _, hat, s_eq, n_eq⟩ => s_eq ▸ n_eq ▸ card_insert_of_notMem hat⟩ +@[deprecated (since := "2026-04-01")] alias card_eq_succ_iff_cons := card_eq_add_one_iff_cons +@[deprecated (since := "2026-04-01")] alias card_eq_succ := card_eq_add_one + theorem card_eq_two : #s = 2 ↔ ∃ x y, x ≠ y ∧ s = {x, y} := by constructor - · rw [card_eq_succ] + · rw [card_eq_add_one] grind [card_eq_one] · grind theorem card_eq_three : #s = 3 ↔ ∃ x y z, x ≠ y ∧ x ≠ z ∧ y ≠ z ∧ s = {x, y, z} := by constructor - · rw [card_eq_succ] + · rw [card_eq_add_one] grind [card_eq_two] · grind theorem card_eq_four : #s = 4 ↔ ∃ x y z w, x ≠ y ∧ x ≠ z ∧ x ≠ w ∧ y ≠ z ∧ y ≠ w ∧ z ≠ w ∧ s = {x, y, z, w} := by constructor - · rw [card_eq_succ] + · rw [card_eq_add_one] grind [card_eq_three] · grind diff --git a/Mathlib/Data/Finset/Powerset.lean b/Mathlib/Data/Finset/Powerset.lean index ee1930b8a85b5f..709f91935efccf 100644 --- a/Mathlib/Data/Finset/Powerset.lean +++ b/Mathlib/Data/Finset/Powerset.lean @@ -285,7 +285,7 @@ theorem powersetCard_sup [DecidableEq α] (u : Finset α) (n : ℕ) (hn : n < u. intro x hx simp only [mem_biUnion, id] obtain ⟨t, ht⟩ : ∃ t, t ∈ powersetCard n (u.erase x) := powersetCard_nonempty.2 - (le_trans (Nat.le_sub_one_of_lt hn) sub_one_card_le_card_erase) + (le_trans (Nat.le_sub_one_of_lt hn) card_sub_one_le_card_erase) refine ⟨insert x t, ?_, mem_insert_self _ _⟩ rw [← insert_erase hx, powersetCard_succ_insert (notMem_erase _ _)] exact mem_union_right _ (mem_image_of_mem _ ht) diff --git a/Mathlib/Data/Set/Card.lean b/Mathlib/Data/Set/Card.lean index bfa9dbaa385e5d..cff93d2b4f615c 100644 --- a/Mathlib/Data/Set/Card.lean +++ b/Mathlib/Data/Set/Card.lean @@ -1263,7 +1263,7 @@ theorem eq_insert_of_ncard_eq_succ {n : ℕ} (h : s.ncard = n + 1) : ∃ a t, a ∉ t ∧ insert a t = s ∧ t.ncard = n := by classical have hsf := finite_of_ncard_pos (n.zero_lt_succ.trans_eq h.symm) - rw [ncard_eq_toFinset_card _ hsf, Finset.card_eq_succ] at h + rw [ncard_eq_toFinset_card _ hsf, Finset.card_eq_add_one] at h obtain ⟨a, t, hat, hts, rfl⟩ := h simp only [Finset.ext_iff, Finset.mem_insert, Finite.mem_toFinset] at hts refine ⟨a, t, hat, ?_, ?_⟩ diff --git a/Mathlib/GroupTheory/Perm/Support.lean b/Mathlib/GroupTheory/Perm/Support.lean index e7c42d7a958e59..37e32d2802c5f0 100644 --- a/Mathlib/GroupTheory/Perm/Support.lean +++ b/Mathlib/GroupTheory/Perm/Support.lean @@ -601,7 +601,7 @@ theorem card_support_swap {x y : α} (hxy : x ≠ y) : #(swap x y).support = 2 : @[simp] theorem card_support_eq_two {f : Perm α} : #f.support = 2 ↔ IsSwap f := by constructor <;> intro h - · obtain ⟨x, t, hmem, hins, ht⟩ := card_eq_succ.1 h + · obtain ⟨x, t, hmem, hins, ht⟩ := card_eq_add_one.1 h obtain ⟨y, rfl⟩ := card_eq_one.1 ht rw [mem_singleton] at hmem refine ⟨x, y, hmem, ?_⟩ diff --git a/Mathlib/RingTheory/Ideal/Operations.lean b/Mathlib/RingTheory/Ideal/Operations.lean index c619bd730cd522..897cb0a66b2df6 100644 --- a/Mathlib/RingTheory/Ideal/Operations.lean +++ b/Mathlib/RingTheory/Ideal/Operations.lean @@ -1076,7 +1076,7 @@ theorem subset_union_prime' {R : Type u} [CommRing R] {s : Finset ι} {f : ι | succ n ih => classical replace hn : ∃ (i : ι) (t : Finset ι), i ∉ t ∧ insert i t = s ∧ t.card = n := - Finset.card_eq_succ.1 hn + Finset.card_eq_add_one.1 hn rcases hn with ⟨i, t, hit, rfl, hn⟩ replace hp : IsPrime (f i) ∧ ∀ x ∈ t, IsPrime (f x) := (t.forall_mem_insert _ _).1 hp by_cases Ht : ∃ j ∈ t, f j ≤ f i