diff --git a/Mathlib/Algebra/Polynomial/EraseLead.lean b/Mathlib/Algebra/Polynomial/EraseLead.lean
index 478142e8f396a6..19ab695f231a40 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.pred_card_le_card_erase).ne.symm
+    (zero_lt_one.trans_le <|
+      (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 530007ec7ec027..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 <| pred_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 37c2b8e97c20de..c50bcb5b33b886 100644
--- a/Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean
+++ b/Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean
@@ -417,7 +417,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 d1c2c1e36ea902..8e30cf38d8a1d5 100644
--- a/Mathlib/Data/Finset/Card.lean
+++ b/Mathlib/Data/Finset/Card.lean
@@ -153,7 +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 pred_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-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 :=
@@ -738,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]⟩
@@ -746,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 d37121600efa7e..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) pred_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 1ca79eb8302a1a..6e681ed862fcda 100644
--- a/Mathlib/Data/Set/Card.lean
+++ b/Mathlib/Data/Set/Card.lean
@@ -1243,7 +1243,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 9c2f9763b2828c..73f75027dc9299 100644
--- a/Mathlib/GroupTheory/Perm/Support.lean
+++ b/Mathlib/GroupTheory/Perm/Support.lean
@@ -590,7 +590,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 f6ffa68863dd37..57b02e9fb14b83 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