chore: deprecate three lemmas about Order.succ on ordinals (#39859)

We want to write `x + 1` instead of `succ x`. These were three easy pickings.

Author: vihdzp

Mathlib/SetTheory/Cardinal/Aleph.lean

@@ -586,7 +586,7 @@ theorem preBeth_add_one (o : Ordinal) : preBeth (o + 1) = 2 ^ preBeth o := by
   rw [preBeth, ← succ_eq_add_one, Iio_succ]
   exact ciSup_Iic o fun x y h ↦ power_le_power_left two_ne_zero (preBeth_mono h)
 
--- TODO: deprecate
+@[deprecated preBeth_add_one (since := "2026-05-26")]
 theorem preBeth_succ (o : Ordinal) : preBeth (succ o) = 2 ^ preBeth o :=
   preBeth_add_one o
 
@@ -596,7 +596,7 @@ theorem preBeth_limit {o : Ordinal} (ho : IsSuccPrelimit o) :
   apply (ciSup_mono bddAbove_of_small fun _ ↦ (cantor _).le).antisymm'
   rw [ciSup_le_iff' bddAbove_of_small]
   intro a
-  rw [← preBeth_succ]
+  rw [← preBeth_add_one]
   exact le_ciSup bddAbove_of_small (⟨_, ho.succ_lt a.2⟩ : Iio o)
 
 theorem isNormal_preBeth : Order.IsNormal preBeth := by

Mathlib/SetTheory/Ordinal/Arithmetic.lean

@@ -261,7 +261,7 @@ def pred (o : Ordinal) : Ordinal :=
 theorem pred_add_one (o) : pred (o + 1) = o :=
   isSuccPrelimitRecOn_succ ..
 
--- TODO: deprecate
+@[deprecated pred_add_one (since := "2026-05-25")]
 theorem pred_succ (o) : pred (succ o) = o :=
   pred_add_one o
 

Mathlib/SetTheory/ZFC/VonNeumann.lean

@@ -120,7 +120,7 @@ theorem vonNeumann_zero : V_ 0 = ∅ :=
 theorem vonNeumann_add_one (o : Ordinal) : V_ (o + 1) = powerset (V_ o) :=
   ext fun z ↦ by rw [mem_vonNeumann, mem_powerset, subset_vonNeumann, lt_add_one_iff]
 
--- TODO: deprecate
+@[deprecated vonNeumann_add_one (since := "2026-05-25")]
 theorem vonNeumann_succ (o : Ordinal) : V_ (succ o) = powerset (V_ o) :=
   vonNeumann_add_one o
 
@@ -155,7 +155,7 @@ theorem card_vonNeumann (o : Ordinal.{u}) : card (V_ o) = preBeth o := by
       by_contra! h
       refine (⨆ i : Set.Iio o, (V_ ↑i).card).card_ord.not_lt <|
         (Ordinal.card_le_card_vonNeumann _).trans_lt <| (cantor _).trans_le ?_
-      rw [← card_powerset, ← vonNeumann_succ]
+      rw [← card_powerset, ← vonNeumann_add_one]
       refine le_ciSup bddAbove_of_small (⟨_, ho.succ_lt ?_⟩ : Set.Iio o)
       exact (ord_card_le _).trans_lt' (ord_strictMono h)