chore: use x + 1 instead of succ x in Ordinal.limitRecOn (leanprover-community#39648)

The idea is to phase out the use of `Order.succ` on ordinals. See also [Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/why.20is.20Order.2Esucc_eq_add_one.20simp.3F/near/596561918).

Author: vihdzp

Mathlib/SetTheory/Cardinal/Ordinal.lean

@@ -124,10 +124,9 @@ theorem card_sSup_le {c : Cardinal} {s : Set Ordinal.{u}}
 
 theorem card_opow_le_of_omega0_le_left {a : Ordinal} (ha : ω ≤ a) (b : Ordinal) :
     (a ^ b).card ≤ max a.card b.card := by
-  refine limitRecOn b ?_ ?_ ?_
-  · simpa using one_lt_omega0.le.trans ha
-  · intro b IH
-    simp_rw [Order.succ_eq_add_one]
+  induction b using limitRecOn with
+  | zero => simpa using one_lt_omega0.le.trans ha
+  | add_one b IH =>
     rw [opow_add_one, card_mul, card_add_one, Cardinal.mul_eq_max_of_aleph0_le_right, max_comm]
     · grw [IH]
       rw [← max_assoc, max_self]
@@ -136,7 +135,7 @@ theorem card_opow_le_of_omega0_le_left {a : Ordinal} (ha : ω ≤ a) (b : Ordina
       rintro ⟨rfl, -⟩
       cases omega0_pos.not_ge ha
     · rwa [aleph0_le_card]
-  · intro b hb IH
+  | limit b hb IH =>
     rw [(isNormal_opow (one_lt_omega0.trans_le ha)).apply_of_isSuccLimit hb]
     exact card_iSup_Iio_le (le_max_right ..) fun i ↦
       (IH i i.2).trans (max_le_max_left _ (card_le_card i.2.le))

Mathlib/SetTheory/Cardinal/Regular.lean

@@ -266,9 +266,9 @@ theorem derivFamily_lt_ord_lift {ι : Type u} {f : ι → Ordinal → Ordinal} {
   | zero =>
     rw [derivFamily_zero]
     exact nfpFamily_lt_ord_lift hω (by rwa [hc.cof_ord]) hf
-  | succ b hb =>
+  | add_one b hb =>
     intro hb'
-    rw [derivFamily_succ]
+    rw [derivFamily_add_one]
     exact
       nfpFamily_lt_ord_lift hω (by rwa [hc.cof_ord]) hf
         ((isSuccLimit_ord hc.1).succ_lt (hb ((lt_succ b).trans hb')))

Mathlib/SetTheory/Ordinal/Arithmetic.lean

@@ -156,18 +156,23 @@ Note that this is just a special (though sometimes convenient) case of the more
 well-founded recursion `WellFoundedLT.fix`. -/
 @[elab_as_elim]
 def limitRecOn {motive : Ordinal → Sort*} (o : Ordinal)
-    (zero : motive 0) (succ : ∀ o, motive o → motive (succ o))
+    (zero : motive 0) (add_one : ∀ o, motive o → motive (o + 1))
     (limit : ∀ o, IsSuccLimit o → (∀ o' < o, motive o') → motive o) : motive o :=
-  SuccOrder.limitRecOn o (fun _a ha ↦ ha.eq_bot ▸ zero) (fun a _ ↦ succ a) limit
+  SuccOrder.limitRecOn o (fun _a ha ↦ ha.eq_bot ▸ zero) (fun a _ ↦ add_one a) limit
 
 @[simp]
 theorem limitRecOn_zero {motive} (H₁ H₂ H₃) : @limitRecOn motive 0 H₁ H₂ H₃ = H₁ :=
   SuccOrder.limitRecOn_isMin _ _ _ isMin_bot
 
 @[simp]
+theorem limitRecOn_add_one {motive} (o H₁ H₂ H₃) :
+    @limitRecOn motive (o + 1) H₁ H₂ H₃ = H₂ o (@limitRecOn motive o H₁ H₂ H₃) :=
+  SuccOrder.limitRecOn_succ ..
+
+@[deprecated limitRecOn_add_one (since := "2026-05-21")]
 theorem limitRecOn_succ {motive} (o H₁ H₂ H₃) :
     @limitRecOn motive (succ o) H₁ H₂ H₃ = H₂ o (@limitRecOn motive o H₁ H₂ H₃) :=
-  SuccOrder.limitRecOn_succ ..
+  limitRecOn_add_one ..
 
 @[simp]
 theorem limitRecOn_limit {motive} (o H₁ H₂ H₃ h) :
@@ -184,7 +189,7 @@ def boundedLimitRecOn {l : Ordinal} (lLim : IsSuccLimit l) {motive : Iio l → S
   obtain ⟨o, ho⟩ := o
   induction o using limitRecOn with
   | zero => exact zero
-  | succ o IH =>
+  | add_one o IH =>
     have ho' : o < l := (lt_succ o).trans ho
     exact succ ⟨o, ho'⟩ (IH ho')
   | limit o ho' IH => exact limit _ ho' fun a ha ↦ IH a.1 ha (ha.trans (c := l) ho)
@@ -678,13 +683,16 @@ private theorem add_mul_limit_aux {a b c : Ordinal} (ba : b + a = a) (l : IsSucc
       grw [le_succ c', IH _ h, le_self_add (a := b), ba, ← mul_succ, succ_le_of_lt <| l.succ_lt h])
     (by grw [← le_self_add])
 
-theorem add_mul_succ {a b : Ordinal} (c) (ba : b + a = a) : (a + b) * succ c = a * succ c + b := by
+theorem add_mul_add_one {a b : Ordinal} (c) (ba : b + a = a) :
+    (a + b) * (c + 1) = a * (c + 1) + b := by
   induction c using limitRecOn with
   | zero => simp
-  | succ c IH =>
-    rw [mul_succ, IH, ← add_assoc, add_assoc _ b, ba, ← mul_succ]
-  | limit c l IH =>
-    rw [mul_succ, add_mul_limit_aux ba l IH, mul_succ, add_assoc]
+  | add_one c IH => rw [mul_add_one, IH, ← add_assoc, add_assoc _ b, ba, ← mul_add_one]
+  | limit c l IH => rw [mul_add_one, add_mul_limit_aux ba l IH, mul_add_one, add_assoc]
+
+-- TODO: deprecate
+theorem add_mul_succ {a b : Ordinal} (c) (ba : b + a = a) : (a + b) * succ c = a * succ c + b :=
+  add_mul_add_one c ba
 
 theorem add_mul_of_isSuccLimit {a b c : Ordinal} (ba : b + a = a) (l : IsSuccLimit c) :
     (a + b) * c = a * c :=

Mathlib/SetTheory/Ordinal/Exponential.lean

@@ -60,7 +60,7 @@ theorem opow_add_one (a b : Ordinal) : a ^ (b + 1) = a ^ b * a := by
   obtain rfl | h := eq_or_ne a 0
   · rw [zero_opow (add_pos_of_right zero_lt_one b).ne', mul_zero]
   · rw [opow_of_ne_zero h, opow_of_ne_zero h]
-    exact limitRecOn_succ ..
+    exact limitRecOn_add_one ..
 
 -- TODO: deprecate
 theorem opow_succ (a b : Ordinal) : a ^ succ b = a ^ b * a :=
@@ -86,23 +86,19 @@ theorem opow_one (a : Ordinal) : a ^ (1 : Ordinal) = a := by
 @[simp]
 theorem one_opow (a : Ordinal) : (1 : Ordinal) ^ a = 1 := by
   induction a using limitRecOn with
-  | zero => simp only [opow_zero]
-  | succ _ ih =>
-    simp only [opow_succ, ih, mul_one]
+  | zero => simp
+  | add_one _ IH => simp [IH, mul_one]
   | limit b l IH =>
     refine eq_of_forall_ge_iff fun c => ?_
     rw [opow_le_of_isSuccLimit one_ne_zero l]
     exact ⟨fun H => by simpa only [opow_zero] using H 0 l.bot_lt, fun H b' h => by rwa [IH _ h]⟩
 
 theorem opow_pos {a : Ordinal} (b : Ordinal) (a0 : 0 < a) : 0 < a ^ b := by
-  have h0 : 0 < a ^ (0 : Ordinal) := by simp only [opow_zero, zero_lt_one]
+  have h0 : 0 < a ^ (0 : Ordinal) := by simp
   induction b using limitRecOn with
   | zero => exact h0
-  | succ b IH =>
-    rw [opow_succ]
-    exact mul_pos IH a0
-  | limit b l _ =>
-    exact (lt_opow_of_isSuccLimit (pos_iff_ne_zero.1 a0) l).2 ⟨0, l.bot_lt, h0⟩
+  | add_one b IH => simpa using mul_pos IH a0
+  | limit b l _ => exact (lt_opow_of_isSuccLimit (pos_iff_ne_zero.1 a0) l).2 ⟨0, l.pos, h0⟩
 
 theorem opow_ne_zero {a : Ordinal} (b : Ordinal) (a0 : a ≠ 0) : a ^ b ≠ 0 :=
   pos_iff_ne_zero.1 <| opow_pos b <| pos_iff_ne_zero.2 a0
@@ -184,7 +180,7 @@ theorem opow_le_opow_left {a b : Ordinal} (c : Ordinal) (ab : a ≤ b) : a ^ c 
   · by_cases c = 0 <;> simp_all
   · induction c using limitRecOn with
     | zero => simp
-    | succ c IH => simpa using mul_le_mul' IH ab
+    | add_one c IH => simpa using mul_le_mul' IH ab
     | limit c l IH =>
       exact (opow_le_of_isSuccLimit ha l).2 fun b' h ↦
         (IH _ h).trans (opow_le_opow_right ((pos_iff_ne_zero.2 ha).trans_le ab) h.le)
@@ -223,7 +219,7 @@ theorem opow_add (a b c : Ordinal) : a ^ (b + c) = a ^ b * a ^ c := by
   obtain rfl | ha' := (one_le_iff_ne_zero.2 ha.ne').eq_or_lt; · simp
   induction c using limitRecOn with
   | zero => simp
-  | succ c IH => rw [succ_eq_add_one, ← add_assoc, opow_add_one, IH, opow_add_one, mul_assoc]
+  | add_one c IH => rw [← add_assoc, opow_add_one, IH, opow_add_one, mul_assoc]
   | limit c l IH =>
     refine eq_of_forall_ge_iff fun d ↦
       (((isNormal_opow ha').comp (isNormal_add_right b)).le_iff_forall_le l).trans ?_
@@ -251,7 +247,7 @@ theorem opow_mul (a b c : Ordinal) : a ^ (b * c) = (a ^ b) ^ c := by
   obtain rfl | ha' := (one_le_iff_ne_zero.2 ha).eq_or_lt; · simp
   induction c using limitRecOn with
   | zero => simp
-  | succ c IH => rw [mul_succ, opow_add, IH, opow_succ]
+  | add_one c IH => rw [mul_add_one, opow_add, IH, opow_add_one]
   | limit c l IH =>
     refine eq_of_forall_ge_iff fun d ↦
       (((isNormal_opow ha').comp (isNormal_mul_right hb)).le_iff_forall_le l).trans ?_

Mathlib/SetTheory/Ordinal/FixedPoint.lean

@@ -141,7 +141,7 @@ theorem derivFamily_zero (f : ι → Ordinal → Ordinal) :
 @[simp]
 theorem derivFamily_add_one (f : ι → Ordinal → Ordinal) (o) :
     derivFamily f (o + 1) = nfpFamily f (derivFamily f o + 1) :=
-  limitRecOn_succ ..
+  limitRecOn_add_one ..
 
 -- TODO: deprecate
 theorem derivFamily_succ (f : ι → Ordinal → Ordinal) (o) :
@@ -171,8 +171,8 @@ theorem derivFamily_fp [Small.{u} ι] {i} (H : IsNormal (f i)) (o : Ordinal) :
   | zero =>
     rw [derivFamily_zero]
     exact nfpFamily_fp H 0
-  | succ =>
-    rw [derivFamily_succ]
+  | add_one =>
+    rw [derivFamily_add_one]
     exact nfpFamily_fp H _
   | limit o l IH =>
     have := l.nonempty_Iio.to_subtype
@@ -194,12 +194,12 @@ theorem le_iff_derivFamily [Small.{u} ι] (H : ∀ i, IsNormal (f i)) {a} :
       refine ⟨0, le_antisymm ?_ h₁⟩
       rw [derivFamily_zero]
       exact nfpFamily_le_fp (fun i => (H i).monotone) zero_le ha
-    | succ o IH =>
+    | add_one o IH =>
       intro h₁
       rcases le_or_gt a (derivFamily f o) with h | h
       · exact IH h
-      refine ⟨succ o, le_antisymm ?_ h₁⟩
-      rw [derivFamily_succ]
+      refine ⟨o + 1, le_antisymm ?_ h₁⟩
+      rw [derivFamily_add_one]
       exact nfpFamily_le_fp (fun i => (H i).monotone) (succ_le_of_lt h) ha
     | limit o l IH =>
       intro h₁

Mathlib/SetTheory/ZFC/VonNeumann.lean

@@ -140,10 +140,8 @@ lemma _root_.Ordinal.card_le_card_vonNeumann (o : Ordinal) : o.card ≤ card (V_
 open Cardinal in
 theorem card_vonNeumann (o : Ordinal.{u}) : card (V_ o) = preBeth o := by
   induction o using Ordinal.limitRecOn with
-  | zero =>
-    rw [vonNeumann_zero, card_empty, preBeth_zero]
-  | succ o ih =>
-    rw [vonNeumann_succ, card_powerset, ih, preBeth_succ]
+  | zero => simp
+  | add_one o ih => simp [ih]
   | limit o ho ih =>
     simp_rw [preBeth_limit ho.isSuccPrelimit, ← fun i : Set.Iio o => ih i i.2,
       vonNeumann_of_isSuccPrelimit ho.isSuccPrelimit]