From 6a6dab17b44811d916b898545593eae3f746851a Mon Sep 17 00:00:00 2001
From: YnirPaz <paznir83@gmail.com>
Date: Thu, 3 Oct 2024 08:34:00 +0000
Subject: [PATCH] refactor(SetTheory/Ordinal/Basic): deprecate Ordinal.omega in
 favor of Ordinal.omega0 (#17158)

See [zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.CF.89_.20.CE.B1.20function) for the discussion.
---
 Mathlib/SetTheory/Cardinal/Cofinality.lean |   9 +-
 Mathlib/SetTheory/Cardinal/Ordinal.lean    |  17 ++-
 Mathlib/SetTheory/Game/Nim.lean            |   4 +-
 Mathlib/SetTheory/Game/Short.lean          |   2 +-
 Mathlib/SetTheory/Ordinal/Arithmetic.lean  | 103 +++++++++-----
 Mathlib/SetTheory/Ordinal/Basic.lean       |  28 ++--
 Mathlib/SetTheory/Ordinal/Exponential.lean |   4 +-
 Mathlib/SetTheory/Ordinal/FixedPoint.lean  | 108 +++++++++------
 Mathlib/SetTheory/Ordinal/Notation.lean    | 132 ++++++++++--------
 Mathlib/SetTheory/Ordinal/Principal.lean   | 154 +++++++++++++--------
 scripts/no_lints_prime_decls.txt           |   4 +-
 11 files changed, 350 insertions(+), 215 deletions(-)

diff --git a/Mathlib/SetTheory/Cardinal/Cofinality.lean b/Mathlib/SetTheory/Cardinal/Cofinality.lean
index 035f8671aa50d4..53bfb76a4a06ee 100644
--- a/Mathlib/SetTheory/Cardinal/Cofinality.lean
+++ b/Mathlib/SetTheory/Cardinal/Cofinality.lean
@@ -680,11 +680,14 @@ theorem aleph_cof {o : Ordinal} (ho : o.IsLimit) : (aleph o).ord.cof = o.cof :=
   aleph_isNormal.cof_eq ho
 
 @[simp]
-theorem cof_omega : cof ω = ℵ₀ :=
-  (aleph0_le_cof.2 omega_isLimit).antisymm' <| by
-    rw [← card_omega]
+theorem cof_omega0 : cof ω = ℵ₀ :=
+  (aleph0_le_cof.2 omega0_isLimit).antisymm' <| by
+    rw [← card_omega0]
     apply cof_le_card
 
+@[deprecated (since := "2024-09-30")]
+alias cof_omega := cof_omega0
+
 theorem cof_eq' (r : α → α → Prop) [IsWellOrder α r] (h : IsLimit (type r)) :
     ∃ S : Set α, (∀ a, ∃ b ∈ S, r a b) ∧ #S = cof (type r) :=
   let ⟨S, H, e⟩ := cof_eq r
diff --git a/Mathlib/SetTheory/Cardinal/Ordinal.lean b/Mathlib/SetTheory/Cardinal/Ordinal.lean
index f605981cb3c6bc..fe8a2ac9038379 100644
--- a/Mathlib/SetTheory/Cardinal/Ordinal.lean
+++ b/Mathlib/SetTheory/Cardinal/Ordinal.lean
@@ -61,7 +61,7 @@ theorem ord_isLimit {c} (co : ℵ₀ ≤ c) : (ord c).IsLimit := by
     rw [← ord_le, ← le_succ_of_isLimit, ord_le]
     · exact co.trans h
     · rw [ord_aleph0]
-      exact omega_isLimit
+      exact omega0_isLimit
 
 theorem noMaxOrder {c} (h : ℵ₀ ≤ c) : NoMaxOrder c.ord.toType :=
   toType_noMax_of_succ_lt (ord_isLimit h).2
@@ -217,11 +217,14 @@ theorem aleph'_limit {o : Ordinal} (ho : o.IsLimit) : aleph' o = ⨆ a : Iio o,
   exact fun a ha => le_ciSup (bddAbove_of_small _) (⟨a, ha⟩ : Iio o)
 
 @[simp]
-theorem aleph'_omega : aleph' ω = ℵ₀ :=
+theorem aleph'_omega0 : aleph' ω = ℵ₀ :=
   eq_of_forall_ge_iff fun c => by
-    simp only [aleph'_le_of_limit omega_isLimit, lt_omega, exists_imp, aleph0_le]
+    simp only [aleph'_le_of_limit omega0_isLimit, lt_omega0, exists_imp, aleph0_le]
     exact forall_swap.trans (forall_congr' fun n => by simp only [forall_eq, aleph'_nat])
 
+@[deprecated (since := "2024-09-30")]
+alias aleph'_omega := aleph'_omega0
+
 set_option linter.deprecated false in
 /-- `aleph'` and `aleph_idx` form an equivalence between `Ordinal` and `Cardinal` -/
 @[deprecated aleph' (since := "2024-08-28")]
@@ -256,7 +259,7 @@ theorem aleph_succ (o : Ordinal) : aleph (succ o) = succ (aleph o) := by
   rw [aleph_eq_aleph', add_succ, aleph'_succ, aleph_eq_aleph']
 
 @[simp]
-theorem aleph_zero : aleph 0 = ℵ₀ := by rw [aleph_eq_aleph', add_zero, aleph'_omega]
+theorem aleph_zero : aleph 0 = ℵ₀ := by rw [aleph_eq_aleph', add_zero, aleph'_omega0]
 
 theorem aleph_limit {o : Ordinal} (ho : o.IsLimit) : aleph o = ⨆ a : Iio o, aleph a := by
   apply le_antisymm _ (ciSup_le' _)
@@ -264,13 +267,13 @@ theorem aleph_limit {o : Ordinal} (ho : o.IsLimit) : aleph o = ⨆ a : Iio o, al
     refine ciSup_mono' (bddAbove_of_small _) ?_
     rintro ⟨i, hi⟩
     cases' lt_or_le i ω with h h
-    · rcases lt_omega.1 h with ⟨n, rfl⟩
+    · rcases lt_omega0.1 h with ⟨n, rfl⟩
       use ⟨0, ho.pos⟩
       simpa using (nat_lt_aleph0 n).le
     · exact ⟨⟨_, (sub_lt_of_le h).2 hi⟩, aleph'_le.2 (le_add_sub _ _)⟩
   · exact fun i => aleph_le.2 (le_of_lt i.2)
 
-theorem aleph0_le_aleph' {o : Ordinal} : ℵ₀ ≤ aleph' o ↔ ω ≤ o := by rw [← aleph'_omega, aleph'_le]
+theorem aleph0_le_aleph' {o : Ordinal} : ℵ₀ ≤ aleph' o ↔ ω ≤ o := by rw [← aleph'_omega0, aleph'_le]
 
 theorem aleph0_le_aleph (o : Ordinal) : ℵ₀ ≤ aleph o := by
   rw [aleph_eq_aleph', aleph0_le_aleph']
@@ -1442,7 +1445,7 @@ scoped notation "ω_" o => ord <| aleph o
 -/
 scoped notation "ω₁" => ord <| aleph 1
 
-lemma omega_lt_omega1 : ω < ω₁ := ord_aleph0.symm.trans_lt (ord_lt_ord.mpr (aleph0_lt_aleph_one))
+lemma omega0_lt_omega1 : ω < ω₁ := ord_aleph0.symm.trans_lt (ord_lt_ord.mpr (aleph0_lt_aleph_one))
 
 section OrdinalIndices
 /-!
diff --git a/Mathlib/SetTheory/Game/Nim.lean b/Mathlib/SetTheory/Game/Nim.lean
index dea7c7401922ce..46bd9ae9c794ea 100644
--- a/Mathlib/SetTheory/Game/Nim.lean
+++ b/Mathlib/SetTheory/Game/Nim.lean
@@ -343,7 +343,7 @@ theorem grundyValue_nim_add_nim (n m : ℕ) : grundyValue (nim.{u} n + nim.{u} m
     all_goals
       intro j
       have hj := toLeftMovesNim_symm_lt j
-      obtain ⟨k, hk⟩ := lt_omega.1 (hj.trans (nat_lt_omega _))
+      obtain ⟨k, hk⟩ := lt_omega0.1 (hj.trans (nat_lt_omega0 _))
       rw [hk, Nat.cast_lt] at hj
       have := hj.ne
       have := hj -- The termination checker doesn't work without this.
@@ -354,7 +354,7 @@ theorem grundyValue_nim_add_nim (n m : ℕ) : grundyValue (nim.{u} n + nim.{u} m
   -- For any `k < n ^^^ m`, either `nim (k ^^^ m) + nim m` or `nim n + nim (k ^^^ n)` is a left
   -- option with Grundy value `k`.
   · intro k hk
-    obtain ⟨k, rfl⟩ := Ordinal.lt_omega.1 (hk.trans (Ordinal.nat_lt_omega _))
+    obtain ⟨k, rfl⟩ := Ordinal.lt_omega0.1 (hk.trans (Ordinal.nat_lt_omega0 _))
     rw [Set.mem_Iio, Nat.cast_lt] at hk
     obtain hk | hk := Nat.lt_xor_cases hk <;> rw [← natCast_lt] at hk
     · use toLeftMovesAdd (Sum.inl (toLeftMovesNim ⟨_, hk⟩))
diff --git a/Mathlib/SetTheory/Game/Short.lean b/Mathlib/SetTheory/Game/Short.lean
index 1d55f6247f4520..03c8ecbda2c5ba 100644
--- a/Mathlib/SetTheory/Game/Short.lean
+++ b/Mathlib/SetTheory/Game/Short.lean
@@ -136,7 +136,7 @@ def moveRightShort' {xl xr} (xL xR) [S : Short (mk xl xr xL xR)] (j : xr) : Shor
 
 attribute [local instance] moveRightShort'
 
-theorem short_birthday (x : PGame.{u}) : [Short x] → x.birthday < Ordinal.omega := by
+theorem short_birthday (x : PGame.{u}) : [Short x] → x.birthday < Ordinal.omega0 := by
   -- Porting note: Again `induction` is used instead of `pgame_wf_tac`
   induction x with
   | mk xl xr xL xR ihl ihr =>
diff --git a/Mathlib/SetTheory/Ordinal/Arithmetic.lean b/Mathlib/SetTheory/Ordinal/Arithmetic.lean
index c53d3f62b99c50..7c32c24c42d886 100644
--- a/Mathlib/SetTheory/Ordinal/Arithmetic.lean
+++ b/Mathlib/SetTheory/Ordinal/Arithmetic.lean
@@ -539,9 +539,9 @@ theorem sub_isLimit {a b} (l : IsLimit a) (h : b < a) : IsLimit (a - b) :=
     rw [lt_sub, add_succ]; exact l.2 _ (lt_sub.1 h)⟩
 
 -- @[simp] -- Porting note (#10618): simp can prove this
-theorem one_add_omega : 1 + ω = ω := by
+theorem one_add_omega0 : 1 + ω = ω := by
   refine le_antisymm ?_ (le_add_left _ _)
-  rw [omega, ← lift_one.{0}, ← lift_add, lift_le, ← type_unit, ← type_sum_lex]
+  rw [omega0, ← lift_one.{0}, ← lift_add, lift_le, ← type_unit, ← type_sum_lex]
   refine ⟨RelEmbedding.collapse (RelEmbedding.ofMonotone ?_ ?_)⟩
   · apply Sum.rec
     · exact fun _ => 0
@@ -550,9 +550,15 @@ theorem one_add_omega : 1 + ω = ω := by
     cases a <;> cases b <;> intro H <;> cases' H with _ _ H _ _ H <;>
       [exact H.elim; exact Nat.succ_pos _; exact Nat.succ_lt_succ H]
 
+@[deprecated (since := "2024-09-30")]
+alias one_add_omega := one_add_omega0
+
 @[simp]
-theorem one_add_of_omega_le {o} (h : ω ≤ o) : 1 + o = o := by
-  rw [← Ordinal.add_sub_cancel_of_le h, ← add_assoc, one_add_omega]
+theorem one_add_of_omega0_le {o} (h : ω ≤ o) : 1 + o = o := by
+  rw [← Ordinal.add_sub_cancel_of_le h, ← add_assoc, one_add_omega0]
+
+@[deprecated (since := "2024-09-30")]
+alias one_add_of_omega_le := one_add_of_omega0_le
 
 /-! ### Multiplication of ordinals -/
 
@@ -2252,7 +2258,7 @@ theorem lift_ofNat (n : ℕ) [n.AtLeastTwo] :
 
 end Ordinal
 
-/-! ### Properties of `omega` -/
+/-! ### Properties of ω -/
 
 
 namespace Cardinal
@@ -2269,7 +2275,7 @@ theorem ord_aleph0 : ord.{u} ℵ₀ = ω :=
 
 @[simp]
 theorem add_one_of_aleph0_le {c} (h : ℵ₀ ≤ c) : c + 1 = c := by
-  rw [add_comm, ← card_ord c, ← card_one, ← card_add, one_add_of_omega_le]
+  rw [add_comm, ← card_ord c, ← card_one, ← card_add, one_add_of_omega0_le]
   rwa [← ord_aleph0, ord_le_ord]
 
 end Cardinal
@@ -2281,34 +2287,56 @@ theorem lt_add_of_limit {a b c : Ordinal.{u}} (h : IsLimit c) :
   -- Porting note: `bex_def` is required.
   rw [← IsNormal.bsup_eq.{u, u} (add_isNormal b) h, lt_bsup, bex_def]
 
-theorem lt_omega {o : Ordinal} : o < ω ↔ ∃ n : ℕ, o = n := by
+theorem lt_omega0 {o : Ordinal} : o < ω ↔ ∃ n : ℕ, o = n := by
   simp_rw [← Cardinal.ord_aleph0, Cardinal.lt_ord, lt_aleph0, card_eq_nat]
 
-theorem nat_lt_omega (n : ℕ) : ↑n < ω :=
-  lt_omega.2 ⟨_, rfl⟩
+@[deprecated (since := "2024-09-30")]
+alias lt_omega := lt_omega0
+
+theorem nat_lt_omega0 (n : ℕ) : ↑n < ω :=
+  lt_omega0.2 ⟨_, rfl⟩
 
+@[deprecated (since := "2024-09-30")]
+alias nat_lt_omega := nat_lt_omega0
+
+theorem omega0_pos : 0 < ω :=
+  nat_lt_omega0 0
+
+@[deprecated (since := "2024-09-30")]
 theorem omega_pos : 0 < ω :=
-  nat_lt_omega 0
+  nat_lt_omega0 0
+
+theorem omega0_ne_zero : ω ≠ 0 :=
+  omega0_pos.ne'
 
-theorem omega_ne_zero : ω ≠ 0 :=
-  omega_pos.ne'
+@[deprecated (since := "2024-09-30")]
+alias omega_ne_zero := omega0_ne_zero
 
-theorem one_lt_omega : 1 < ω := by simpa only [Nat.cast_one] using nat_lt_omega 1
+theorem one_lt_omega0 : 1 < ω := by simpa only [Nat.cast_one] using nat_lt_omega0 1
 
-theorem omega_isLimit : IsLimit ω :=
-  ⟨omega_ne_zero, fun o h => by
-    let ⟨n, e⟩ := lt_omega.1 h
-    rw [e]; exact nat_lt_omega (n + 1)⟩
+@[deprecated (since := "2024-09-30")]
+alias one_lt_omega := one_lt_omega0
 
-theorem omega_le {o : Ordinal} : ω ≤ o ↔ ∀ n : ℕ, ↑n ≤ o :=
-  ⟨fun h n => (nat_lt_omega _).le.trans h, fun H =>
+theorem omega0_isLimit : IsLimit ω :=
+  ⟨omega0_ne_zero, fun o h => by
+    let ⟨n, e⟩ := lt_omega0.1 h
+    rw [e]; exact nat_lt_omega0 (n + 1)⟩
+
+@[deprecated (since := "2024-09-30")]
+alias omega_isLimit := omega0_isLimit
+
+theorem omega0_le {o : Ordinal} : ω ≤ o ↔ ∀ n : ℕ, ↑n ≤ o :=
+  ⟨fun h n => (nat_lt_omega0 _).le.trans h, fun H =>
     le_of_forall_lt fun a h => by
-      let ⟨n, e⟩ := lt_omega.1 h
+      let ⟨n, e⟩ := lt_omega0.1 h
       rw [e, ← succ_le_iff]; exact H (n + 1)⟩
 
+@[deprecated (since := "2024-09-30")]
+alias omega_le := omega0_le
+
 @[simp]
 theorem iSup_natCast : iSup Nat.cast = ω :=
-  (Ordinal.iSup_le fun n => (nat_lt_omega n).le).antisymm <| omega_le.2 <| Ordinal.le_iSup _
+  (Ordinal.iSup_le fun n => (nat_lt_omega0 n).le).antisymm <| omega0_le.2 <| Ordinal.le_iSup _
 
 set_option linter.deprecated false in
 @[deprecated iSup_natCast (since := "2024-04-17")]
@@ -2322,24 +2350,30 @@ theorem nat_lt_limit {o} (h : IsLimit o) : ∀ n : ℕ, ↑n < o
   | 0 => lt_of_le_of_ne (Ordinal.zero_le o) h.1.symm
   | n + 1 => h.2 _ (nat_lt_limit h n)
 
-theorem omega_le_of_isLimit {o} (h : IsLimit o) : ω ≤ o :=
-  omega_le.2 fun n => le_of_lt <| nat_lt_limit h n
+theorem omega0_le_of_isLimit {o} (h : IsLimit o) : ω ≤ o :=
+  omega0_le.2 fun n => le_of_lt <| nat_lt_limit h n
 
-theorem isLimit_iff_omega_dvd {a : Ordinal} : IsLimit a ↔ a ≠ 0 ∧ ω ∣ a := by
+@[deprecated (since := "2024-09-30")]
+alias omega_le_of_isLimit := omega0_le_of_isLimit
+
+theorem isLimit_iff_omega0_dvd {a : Ordinal} : IsLimit a ↔ a ≠ 0 ∧ ω ∣ a := by
   refine ⟨fun l => ⟨l.1, ⟨a / ω, le_antisymm ?_ (mul_div_le _ _)⟩⟩, fun h => ?_⟩
   · refine (limit_le l).2 fun x hx => le_of_lt ?_
-    rw [← div_lt omega_ne_zero, ← succ_le_iff, le_div omega_ne_zero, mul_succ,
-      add_le_of_limit omega_isLimit]
+    rw [← div_lt omega0_ne_zero, ← succ_le_iff, le_div omega0_ne_zero, mul_succ,
+      add_le_of_limit omega0_isLimit]
     intro b hb
-    rcases lt_omega.1 hb with ⟨n, rfl⟩
+    rcases lt_omega0.1 hb with ⟨n, rfl⟩
     exact
       (add_le_add_right (mul_div_le _ _) _).trans
         (lt_sub.1 <| nat_lt_limit (sub_isLimit l hx) _).le
   · rcases h with ⟨a0, b, rfl⟩
-    refine mul_isLimit_left omega_isLimit (Ordinal.pos_iff_ne_zero.2 <| mt ?_ a0)
+    refine mul_isLimit_left omega0_isLimit (Ordinal.pos_iff_ne_zero.2 <| mt ?_ a0)
     intro e
     simp only [e, mul_zero]
 
+@[deprecated (since := "2024-09-30")]
+alias isLimit_iff_omega_dvd := isLimit_iff_omega0_dvd
+
 theorem add_mul_limit_aux {a b c : Ordinal} (ba : b + a = a) (l : IsLimit c)
     (IH : ∀ c' < c, (a + b) * succ c' = a * succ c' + b) : (a + b) * c = a * c :=
   le_antisymm
@@ -2378,24 +2412,27 @@ theorem add_le_of_forall_add_lt {a b c : Ordinal} (hb : 0 < b) (h : ∀ d < b, a
   by_contra! hb
   exact (h _ hb).ne H
 
-theorem IsNormal.apply_omega {f : Ordinal.{u} → Ordinal.{v}} (hf : IsNormal f) :
+theorem IsNormal.apply_omega0 {f : Ordinal.{u} → Ordinal.{v}} (hf : IsNormal f) :
     ⨆ n : ℕ, f n = f ω := by rw [← iSup_natCast, hf.map_iSup]
 
+@[deprecated (since := "2024-09-30")]
+alias IsNormal.apply_omega := IsNormal.apply_omega0
+
 @[simp]
 theorem iSup_add_nat (o : Ordinal) : ⨆ n : ℕ, o + n = o + ω :=
-  (add_isNormal o).apply_omega
+  (add_isNormal o).apply_omega0
 
 set_option linter.deprecated false in
 @[deprecated iSup_add_nat (since := "2024-08-27")]
 theorem sup_add_nat (o : Ordinal) : (sup fun n : ℕ => o + n) = o + ω :=
-  (add_isNormal o).apply_omega
+  (add_isNormal o).apply_omega0
 
 @[simp]
 theorem iSup_mul_nat (o : Ordinal) : ⨆ n : ℕ, o * n = o * ω := by
   rcases eq_zero_or_pos o with (rfl | ho)
   · rw [zero_mul]
     exact iSup_eq_zero_iff.2 fun n => zero_mul (n : Ordinal)
-  · exact (mul_isNormal ho).apply_omega
+  · exact (mul_isNormal ho).apply_omega0
 
 set_option linter.deprecated false in
 @[deprecated iSup_add_nat (since := "2024-08-27")]
@@ -2403,7 +2440,7 @@ theorem sup_mul_nat (o : Ordinal) : (sup fun n : ℕ => o * n) = o * ω := by
   rcases eq_zero_or_pos o with (rfl | ho)
   · rw [zero_mul]
     exact sup_eq_zero_iff.2 fun n => zero_mul (n : Ordinal)
-  · exact (mul_isNormal ho).apply_omega
+  · exact (mul_isNormal ho).apply_omega0
 
 end Ordinal
 
diff --git a/Mathlib/SetTheory/Ordinal/Basic.lean b/Mathlib/SetTheory/Ordinal/Basic.lean
index d9a0cb4a39c91d..895d453ab84d99 100644
--- a/Mathlib/SetTheory/Ordinal/Basic.lean
+++ b/Mathlib/SetTheory/Ordinal/Basic.lean
@@ -31,9 +31,10 @@ initial segment (or, equivalently, in any way). This total order is well founded
   `Ordinal.liftInitialSeg`.
   For a version registering that it is a principal segment embedding if `u < v`, see
   `Ordinal.liftPrincipalSeg`.
-* `Ordinal.omega` or `ω` is the order type of `ℕ`. This definition is universe polymorphic:
-  `Ordinal.omega.{u} : Ordinal.{u}` (contrast with `ℕ : Type`, which lives in a specific
-  universe). In some cases the universe level has to be given explicitly.
+* `Ordinal.omega0` or `ω` is the order type of `ℕ`. It is called this to match `Cardinal.aleph0`
+  and so that the omega function can be named `Ordinal.omega`. This definition is universe
+  polymorphic: `Ordinal.omega0.{u} : Ordinal.{u}` (contrast with `ℕ : Type`, which lives in
+  a specific universe). In some cases the universe level has to be given explicitly.
 
 * `o₁ + o₂` is the order on the disjoint union of `o₁` and `o₂` obtained by declaring that
   every element of `o₁` is smaller than every element of `o₂`.
@@ -701,29 +702,38 @@ set_option linter.deprecated false in
 theorem lift.initialSeg_coe : (lift.initialSeg.{u, v} : Ordinal → Ordinal) = lift.{v, u} :=
   rfl
 
-/-! ### The first infinite ordinal `omega` -/
+/-! ### The first infinite ordinal ω -/
 
 
 /-- `ω` is the first infinite ordinal, defined as the order type of `ℕ`. -/
-def omega : Ordinal.{u} :=
+def omega0 : Ordinal.{u} :=
   lift <| @type ℕ (· < ·) _
 
+@[deprecated Ordinal.omega0 (since := "2024-09-26")]
+alias omega := omega0
+
 @[inherit_doc]
-scoped notation "ω" => Ordinal.omega
+scoped notation "ω" => Ordinal.omega0
 
-/-- Note that the presence of this lemma makes `simp [omega]` form a loop. -/
+/-- Note that the presence of this lemma makes `simp [omega0]` form a loop. -/
 @[simp]
 theorem type_nat_lt : @type ℕ (· < ·) _ = ω :=
   (lift_id _).symm
 
 @[simp]
-theorem card_omega : card ω = ℵ₀ :=
+theorem card_omega0 : card ω = ℵ₀ :=
   rfl
 
+@[deprecated (since := "2024-09-30")]
+alias card_omega := card_omega0
+
 @[simp]
-theorem lift_omega : lift ω = ω :=
+theorem lift_omega0 : lift ω = ω :=
   lift_lift _
 
+@[deprecated (since := "2024-09-30")]
+alias lift_omega := lift_omega0
+
 /-!
 ### Definition and first properties of addition on ordinals
 
diff --git a/Mathlib/SetTheory/Ordinal/Exponential.lean b/Mathlib/SetTheory/Ordinal/Exponential.lean
index d134e192623ac6..f5d3ed03ea35fe 100644
--- a/Mathlib/SetTheory/Ordinal/Exponential.lean
+++ b/Mathlib/SetTheory/Ordinal/Exponential.lean
@@ -403,7 +403,7 @@ theorem natCast_opow (m : ℕ) : ∀ n : ℕ, ↑(m ^ n : ℕ) = (m : Ordinal) ^
 theorem iSup_pow {o : Ordinal} (ho : 0 < o) : ⨆ n : ℕ, o ^ n = o ^ ω := by
   simp_rw [← opow_natCast]
   rcases (one_le_iff_pos.2 ho).lt_or_eq with ho₁ | rfl
-  · exact (opow_isNormal ho₁).apply_omega
+  · exact (opow_isNormal ho₁).apply_omega0
   · rw [one_opow]
     refine le_antisymm (Ordinal.iSup_le fun n => by rw [one_opow]) ?_
     convert Ordinal.le_iSup _ 0
@@ -414,7 +414,7 @@ set_option linter.deprecated false in
 theorem sup_opow_nat {o : Ordinal} (ho : 0 < o) : (sup fun n : ℕ => o ^ n) = o ^ ω := by
   simp_rw [← opow_natCast]
   rcases (one_le_iff_pos.2 ho).lt_or_eq with ho₁ | rfl
-  · exact (opow_isNormal ho₁).apply_omega
+  · exact (opow_isNormal ho₁).apply_omega0
   · rw [one_opow]
     refine le_antisymm (sup_le fun n => by rw [one_opow]) ?_
     convert le_sup (fun n : ℕ => 1 ^ (n : Ordinal)) 0
diff --git a/Mathlib/SetTheory/Ordinal/FixedPoint.lean b/Mathlib/SetTheory/Ordinal/FixedPoint.lean
index 235483b8420b98..4fe7f81c092182 100644
--- a/Mathlib/SetTheory/Ordinal/FixedPoint.lean
+++ b/Mathlib/SetTheory/Ordinal/FixedPoint.lean
@@ -21,8 +21,8 @@ Moreover, we prove some lemmas about the fixed points of specific normal functio
 * `nfpFamily`, `nfpBFamily`, `nfp`: the next fixed point of a (family of) normal function(s).
 * `fp_family_unbounded`, `fp_bfamily_unbounded`, `fp_unbounded`: the (common) fixed points of a
   (family of) normal function(s) are unbounded in the ordinals.
-* `deriv_add_eq_mul_omega_add`: a characterization of the derivative of addition.
-* `deriv_mul_eq_opow_omega_mul`: a characterization of the derivative of multiplication.
+* `deriv_add_eq_mul_omega0_add`: a characterization of the derivative of addition.
+* `deriv_mul_eq_opow_omega0_mul`: a characterization of the derivative of multiplication.
 -/
 
 
@@ -521,20 +521,23 @@ end
 /-! ### Fixed points of addition -/
 
 @[simp]
-theorem nfp_add_zero (a) : nfp (a + ·) 0 = a * omega := by
+theorem nfp_add_zero (a) : nfp (a + ·) 0 = a * ω := by
   simp_rw [← iSup_iterate_eq_nfp, ← iSup_mul_nat]
   congr; funext n
   induction' n with n hn
   · rw [Nat.cast_zero, mul_zero, iterate_zero_apply]
   · rw [iterate_succ_apply', Nat.add_comm, Nat.cast_add, Nat.cast_one, mul_one_add, hn]
 
-theorem nfp_add_eq_mul_omega {a b} (hba : b ≤ a * omega) : nfp (a + ·) b = a * omega := by
+theorem nfp_add_eq_mul_omega0 {a b} (hba : b ≤ a * ω) : nfp (a + ·) b = a * ω := by
   apply le_antisymm (nfp_le_fp (add_isNormal a).monotone hba _)
   · rw [← nfp_add_zero]
     exact nfp_monotone (add_isNormal a).monotone (Ordinal.zero_le b)
-  · dsimp; rw [← mul_one_add, one_add_omega]
+  · dsimp; rw [← mul_one_add, one_add_omega0]
 
-theorem add_eq_right_iff_mul_omega_le {a b : Ordinal} : a + b = b ↔ a * omega ≤ b := by
+@[deprecated (since := "2024-09-30")]
+alias nfp_add_eq_mul_omega := nfp_add_eq_mul_omega0
+
+theorem add_eq_right_iff_mul_omega0_le {a b : Ordinal} : a + b = b ↔ a * ω ≤ b := by
   refine ⟨fun h => ?_, fun h => ?_⟩
   · rw [← nfp_add_zero a, ← deriv_zero_right]
     cases' (add_isNormal a).fp_iff_deriv.1 h with c hc
@@ -542,25 +545,34 @@ theorem add_eq_right_iff_mul_omega_le {a b : Ordinal} : a + b = b ↔ a * omega
     exact (deriv_isNormal _).monotone (Ordinal.zero_le _)
   · have := Ordinal.add_sub_cancel_of_le h
     nth_rw 1 [← this]
-    rwa [← add_assoc, ← mul_one_add, one_add_omega]
+    rwa [← add_assoc, ← mul_one_add, one_add_omega0]
+
+@[deprecated (since := "2024-09-30")]
+alias add_eq_right_iff_mul_omega_le := add_eq_right_iff_mul_omega0_le
 
-theorem add_le_right_iff_mul_omega_le {a b : Ordinal} : a + b ≤ b ↔ a * omega ≤ b := by
-  rw [← add_eq_right_iff_mul_omega_le]
+theorem add_le_right_iff_mul_omega0_le {a b : Ordinal} : a + b ≤ b ↔ a * ω ≤ b := by
+  rw [← add_eq_right_iff_mul_omega0_le]
   exact (add_isNormal a).le_iff_eq
 
-theorem deriv_add_eq_mul_omega_add (a b : Ordinal.{u}) : deriv (a + ·) b = a * omega + b := by
+@[deprecated (since := "2024-09-30")]
+alias add_le_right_iff_mul_omega_le := add_le_right_iff_mul_omega0_le
+
+theorem deriv_add_eq_mul_omega0_add (a b : Ordinal.{u}) : deriv (a + ·) b = a * ω + b := by
   revert b
   rw [← funext_iff, IsNormal.eq_iff_zero_and_succ (deriv_isNormal _) (add_isNormal _)]
   refine ⟨?_, fun a h => ?_⟩
   · rw [deriv_zero_right, add_zero]
     exact nfp_add_zero a
   · rw [deriv_succ, h, add_succ]
-    exact nfp_eq_self (add_eq_right_iff_mul_omega_le.2 ((le_add_right _ _).trans (le_succ _)))
+    exact nfp_eq_self (add_eq_right_iff_mul_omega0_le.2 ((le_add_right _ _).trans (le_succ _)))
+
+@[deprecated (since := "2024-09-30")]
+alias deriv_add_eq_mul_omega_add := deriv_add_eq_mul_omega0_add
 
 /-! ### Fixed points of multiplication -/
 
 @[simp]
-theorem nfp_mul_one {a : Ordinal} (ha : 0 < a) : nfp (a * ·) 1 = (a^omega) := by
+theorem nfp_mul_one {a : Ordinal} (ha : 0 < a) : nfp (a * ·) 1 = (a ^ ω) := by
   rw [← iSup_iterate_eq_nfp, ← iSup_pow ha]
   congr
   funext n
@@ -575,22 +587,25 @@ theorem nfp_mul_zero (a : Ordinal) : nfp (a * ·) 0 = 0 := by
   induction' n with n hn; · rfl
   dsimp only; rwa [iterate_succ_apply, mul_zero]
 
-theorem nfp_mul_eq_opow_omega {a b : Ordinal} (hb : 0 < b) (hba : b ≤ (a^omega)) :
-    nfp (a * ·) b = (a^omega.{u}) := by
+theorem nfp_mul_eq_opow_omega0 {a b : Ordinal} (hb : 0 < b) (hba : b ≤ (a ^ ω)) :
+    nfp (a * ·) b = (a ^ (ω : Ordinal.{u})) := by
   rcases eq_zero_or_pos a with ha | ha
-  · rw [ha, zero_opow omega_ne_zero] at hba ⊢
+  · rw [ha, zero_opow omega0_ne_zero] at hba ⊢
     simp_rw [Ordinal.le_zero.1 hba, zero_mul]
     exact nfp_zero_left 0
   apply le_antisymm
   · apply nfp_le_fp (mul_isNormal ha).monotone hba
-    rw [← opow_one_add, one_add_omega]
+    rw [← opow_one_add, one_add_omega0]
   rw [← nfp_mul_one ha]
   exact nfp_monotone (mul_isNormal ha).monotone (one_le_iff_pos.2 hb)
 
-theorem eq_zero_or_opow_omega_le_of_mul_eq_right {a b : Ordinal} (hab : a * b = b) :
-    b = 0 ∨ (a^omega.{u}) ≤ b := by
+@[deprecated (since := "2024-09-30")]
+alias nfp_mul_eq_opow_omega := nfp_mul_eq_opow_omega0
+
+theorem eq_zero_or_opow_omega0_le_of_mul_eq_right {a b : Ordinal} (hab : a * b = b) :
+    b = 0 ∨ (a ^ (ω : Ordinal.{u})) ≤ b := by
   rcases eq_zero_or_pos a with ha | ha
-  · rw [ha, zero_opow omega_ne_zero]
+  · rw [ha, zero_opow omega0_ne_zero]
     exact Or.inr (Ordinal.zero_le b)
   rw [or_iff_not_imp_left]
   intro hb
@@ -598,51 +613,66 @@ theorem eq_zero_or_opow_omega_le_of_mul_eq_right {a b : Ordinal} (hab : a * b =
   rw [← Ne, ← one_le_iff_ne_zero] at hb
   exact nfp_le_fp (mul_isNormal ha).monotone hb (le_of_eq hab)
 
-theorem mul_eq_right_iff_opow_omega_dvd {a b : Ordinal} : a * b = b ↔ (a^omega) ∣ b := by
+@[deprecated (since := "2024-09-30")]
+alias eq_zero_or_opow_omega_le_of_mul_eq_right := eq_zero_or_opow_omega0_le_of_mul_eq_right
+
+theorem mul_eq_right_iff_opow_omega0_dvd {a b : Ordinal} : a * b = b ↔ (a ^ ω) ∣ b := by
   rcases eq_zero_or_pos a with ha | ha
-  · rw [ha, zero_mul, zero_opow omega_ne_zero, zero_dvd_iff]
+  · rw [ha, zero_mul, zero_opow omega0_ne_zero, zero_dvd_iff]
     exact eq_comm
   refine ⟨fun hab => ?_, fun h => ?_⟩
   · rw [dvd_iff_mod_eq_zero]
-    rw [← div_add_mod b (a^omega), mul_add, ← mul_assoc, ← opow_one_add, one_add_omega,
+    rw [← div_add_mod b (a ^ ω), mul_add, ← mul_assoc, ← opow_one_add, one_add_omega0,
       add_left_cancel] at hab
-    cases' eq_zero_or_opow_omega_le_of_mul_eq_right hab with hab hab
+    cases' eq_zero_or_opow_omega0_le_of_mul_eq_right hab with hab hab
     · exact hab
-    refine (not_lt_of_le hab (mod_lt b (opow_ne_zero omega ?_))).elim
+    refine (not_lt_of_le hab (mod_lt b (opow_ne_zero ω ?_))).elim
     rwa [← Ordinal.pos_iff_ne_zero]
   cases' h with c hc
-  rw [hc, ← mul_assoc, ← opow_one_add, one_add_omega]
+  rw [hc, ← mul_assoc, ← opow_one_add, one_add_omega0]
+
+@[deprecated (since := "2024-09-30")]
+alias mul_eq_right_iff_opow_omega_dvd := mul_eq_right_iff_opow_omega0_dvd
 
-theorem mul_le_right_iff_opow_omega_dvd {a b : Ordinal} (ha : 0 < a) :
-    a * b ≤ b ↔ (a^omega) ∣ b := by
-  rw [← mul_eq_right_iff_opow_omega_dvd]
+theorem mul_le_right_iff_opow_omega0_dvd {a b : Ordinal} (ha : 0 < a) :
+    a * b ≤ b ↔ (a ^ ω) ∣ b := by
+  rw [← mul_eq_right_iff_opow_omega0_dvd]
   exact (mul_isNormal ha).le_iff_eq
 
-theorem nfp_mul_opow_omega_add {a c : Ordinal} (b) (ha : 0 < a) (hc : 0 < c) (hca : c ≤ (a^omega)) :
-    nfp (a * ·) ((a^omega) * b + c) = (a^omega.{u}) * succ b := by
+@[deprecated (since := "2024-09-30")]
+alias mul_le_right_iff_opow_omega_dvd := mul_le_right_iff_opow_omega0_dvd
+
+theorem nfp_mul_opow_omega0_add {a c : Ordinal} (b) (ha : 0 < a) (hc : 0 < c)
+    (hca : c ≤ a ^ ω) : nfp (a * ·) (a ^ ω * b + c) = (a ^ (ω : Ordinal.{u})) * succ b := by
   apply le_antisymm
   · apply nfp_le_fp (mul_isNormal ha).monotone
     · rw [mul_succ]
       apply add_le_add_left hca
-    · dsimp only; rw [← mul_assoc, ← opow_one_add, one_add_omega]
-  · cases' mul_eq_right_iff_opow_omega_dvd.1 ((mul_isNormal ha).nfp_fp ((a^omega) * b + c)) with
+    · dsimp only; rw [← mul_assoc, ← opow_one_add, one_add_omega0]
+  · cases' mul_eq_right_iff_opow_omega0_dvd.1 ((mul_isNormal ha).nfp_fp ((a ^ ω) * b + c)) with
       d hd
     rw [hd]
     apply mul_le_mul_left'
-    have := le_nfp (Mul.mul a) ((a^omega) * b + c)
+    have := le_nfp (a * ·) (a ^ ω * b + c)
     erw [hd] at this
-    have := (add_lt_add_left hc ((a^omega) * b)).trans_le this
-    rw [add_zero, mul_lt_mul_iff_left (opow_pos omega ha)] at this
+    have := (add_lt_add_left hc (a ^ ω * b)).trans_le this
+    rw [add_zero, mul_lt_mul_iff_left (opow_pos ω ha)] at this
     rwa [succ_le_iff]
 
-theorem deriv_mul_eq_opow_omega_mul {a : Ordinal.{u}} (ha : 0 < a) (b) :
-    deriv (a * ·) b = (a^omega) * b := by
+@[deprecated (since := "2024-09-30")]
+alias nfp_mul_opow_omega_add := nfp_mul_opow_omega0_add
+
+theorem deriv_mul_eq_opow_omega0_mul {a : Ordinal.{u}} (ha : 0 < a) (b) :
+    deriv (a * ·) b = (a ^ ω) * b := by
   revert b
   rw [← funext_iff,
-    IsNormal.eq_iff_zero_and_succ (deriv_isNormal _) (mul_isNormal (opow_pos omega ha))]
+    IsNormal.eq_iff_zero_and_succ (deriv_isNormal _) (mul_isNormal (opow_pos ω ha))]
   refine ⟨?_, fun c h => ?_⟩
   · dsimp only; rw [deriv_zero_right, nfp_mul_zero, mul_zero]
   · rw [deriv_succ, h]
-    exact nfp_mul_opow_omega_add c ha zero_lt_one (one_le_iff_pos.2 (opow_pos _ ha))
+    exact nfp_mul_opow_omega0_add c ha zero_lt_one (one_le_iff_pos.2 (opow_pos _ ha))
+
+@[deprecated (since := "2024-09-30")]
+alias deriv_mul_eq_opow_omega_mul := deriv_mul_eq_opow_omega0_mul
 
 end Ordinal
diff --git a/Mathlib/SetTheory/Ordinal/Notation.lean b/Mathlib/SetTheory/Ordinal/Notation.lean
index d32c08e3c86d19..fd54a141e21311 100644
--- a/Mathlib/SetTheory/Ordinal/Notation.lean
+++ b/Mathlib/SetTheory/Ordinal/Notation.lean
@@ -139,12 +139,15 @@ theorem repr_ofNat (n : ℕ) : repr (ofNat n) = n := by cases n <;> simp
 -- @[simp] -- Porting note (#10618): simp can prove this
 theorem repr_one : repr (ofNat 1) = (1 : ℕ) := repr_ofNat 1
 
-theorem omega_le_oadd (e n a) : ω ^ repr e ≤ repr (oadd e n a) := by
+theorem omega0_le_oadd (e n a) : ω ^ repr e ≤ repr (oadd e n a) := by
   refine le_trans ?_ (le_add_right _ _)
-  simpa using (Ordinal.mul_le_mul_iff_left <| opow_pos (repr e) omega_pos).2 (natCast_le.2 n.2)
+  simpa using (Ordinal.mul_le_mul_iff_left <| opow_pos (repr e) omega0_pos).2 (natCast_le.2 n.2)
+
+@[deprecated (since := "2024-09-30")]
+alias omega_le_oadd := omega0_le_oadd
 
 theorem oadd_pos (e n a) : 0 < oadd e n a :=
-  @lt_of_lt_of_le _ _ _ (ω ^ repr e) _ (opow_pos (repr e) omega_pos) (omega_le_oadd e n a)
+  @lt_of_lt_of_le _ _ _ (ω ^ repr e) _ (opow_pos (repr e) omega0_pos) (omega0_le_oadd e n a)
 
 /-- Compare ordinal notations -/
 def cmp : ONote → ONote → Ordering
@@ -231,14 +234,14 @@ theorem NF.zero_of_zero {e n a} (h : NF (ONote.oadd e n a)) (e0 : e = 0) : a = 0
 
 theorem NFBelow.repr_lt {o b} (h : NFBelow o b) : repr o < ω ^ b := by
   induction h with
-  | zero => exact opow_pos _ omega_pos
+  | zero => exact opow_pos _ omega0_pos
   | oadd' _ _ h₃ _ IH =>
     rw [repr]
     apply ((add_lt_add_iff_left _).2 IH).trans_le
     rw [← mul_succ]
-    apply (mul_le_mul_left' (succ_le_of_lt (nat_lt_omega _)) _).trans
+    apply (mul_le_mul_left' (succ_le_of_lt (nat_lt_omega0 _)) _).trans
     rw [← opow_succ]
-    exact opow_le_opow_right omega_pos (succ_le_of_lt h₃)
+    exact opow_le_opow_right omega0_pos (succ_le_of_lt h₃)
 
 theorem NFBelow.mono {o b₁ b₂} (bb : b₁ ≤ b₂) (h : NFBelow o b₁) : NFBelow o b₂ := by
   induction h with
@@ -253,7 +256,7 @@ theorem NF.below_of_lt' : ∀ {o b}, repr o < ω ^ b → NF o → NFBelow o b
   | 0, _, _, _ => NFBelow.zero
   | ONote.oadd _ _ _, _, H, h =>
     h.below_of_lt <|
-      (opow_lt_opow_iff_right one_lt_omega).1 <| lt_of_le_of_lt (omega_le_oadd _ _ _) H
+      (opow_lt_opow_iff_right one_lt_omega0).1 <| lt_of_le_of_lt (omega0_le_oadd _ _ _) H
 
 theorem nfBelow_ofNat : ∀ n, NFBelow (ofNat n) 1
   | 0 => NFBelow.zero
@@ -267,13 +270,13 @@ instance nf_one : NF 1 := by rw [← ofNat_one]; infer_instance
 theorem oadd_lt_oadd_1 {e₁ n₁ o₁ e₂ n₂ o₂} (h₁ : NF (oadd e₁ n₁ o₁)) (h : e₁ < e₂) :
     oadd e₁ n₁ o₁ < oadd e₂ n₂ o₂ :=
   @lt_of_lt_of_le _ _ (repr (oadd e₁ n₁ o₁)) _ _
-    (NF.below_of_lt h h₁).repr_lt (omega_le_oadd e₂ n₂ o₂)
+    (NF.below_of_lt h h₁).repr_lt (omega0_le_oadd e₂ n₂ o₂)
 
 theorem oadd_lt_oadd_2 {e o₁ o₂ : ONote} {n₁ n₂ : ℕ+} (h₁ : NF (oadd e n₁ o₁)) (h : (n₁ : ℕ) < n₂) :
     oadd e n₁ o₁ < oadd e n₂ o₂ := by
   simp only [lt_def, repr]
   refine lt_of_lt_of_le ((add_lt_add_iff_left _).2 h₁.snd'.repr_lt) (le_trans ?_ (le_add_right _ _))
-  rwa [← mul_succ,Ordinal.mul_le_mul_iff_left (opow_pos _ omega_pos), succ_le_iff, natCast_lt]
+  rwa [← mul_succ,Ordinal.mul_le_mul_iff_left (opow_pos _ omega0_pos), succ_le_iff, natCast_lt]
 
 theorem oadd_lt_oadd_3 {e n a₁ a₂} (h : a₁ < a₂) : oadd e n a₁ < oadd e n a₂ := by
   rw [lt_def]; unfold repr
@@ -325,7 +328,7 @@ theorem repr_inj {a b} [NF a] [NF b] : repr a = repr b ↔ a = b :=
     | Ordering.eq, h => h,
     congr_arg _⟩
 
-theorem NF.of_dvd_omega_opow {b e n a} (h : NF (ONote.oadd e n a))
+theorem NF.of_dvd_omega0_opow {b e n a} (h : NF (ONote.oadd e n a))
     (d : ω ^ b ∣ repr (ONote.oadd e n a)) :
     b ≤ repr e ∧ ω ^ b ∣ repr a := by
   have := mt repr_inj.1 (fun h => by injection h : ONote.oadd e n a ≠ 0)
@@ -333,9 +336,15 @@ theorem NF.of_dvd_omega_opow {b e n a} (h : NF (ONote.oadd e n a))
   simp only [repr] at d
   exact ⟨L, (dvd_add_iff <| (opow_dvd_opow _ L).mul_right _).1 d⟩
 
-theorem NF.of_dvd_omega {e n a} (h : NF (ONote.oadd e n a)) :
+@[deprecated (since := "2024-09-30")]
+alias NF.of_dvd_omega_opow := NF.of_dvd_omega0_opow
+
+theorem NF.of_dvd_omega0 {e n a} (h : NF (ONote.oadd e n a)) :
     ω ∣ repr (ONote.oadd e n a) → repr e ≠ 0 ∧ ω ∣ repr a := by
-  (rw [← opow_one ω, ← one_le_iff_ne_zero]; exact h.of_dvd_omega_opow)
+  (rw [← opow_one ω, ← one_le_iff_ne_zero]; exact h.of_dvd_omega0_opow)
+
+@[deprecated (since := "2024-09-30")]
+alias NF.of_dvd_omega := NF.of_dvd_omega0
 
 /-- `TopBelow b o` asserts that the largest exponent in `o`, if
   it exists, is less than `b`. This is an auxiliary definition
@@ -443,7 +452,7 @@ theorem repr_add : ∀ (o₁ o₂) [NF o₁] [NF o₂], repr (o₁ + o₂) = rep
         unfold repr at this
         cases he' : e' <;> simp only [he', zero_def, opow_zero, repr, gt_iff_lt] at this ⊢ <;>
         exact lt_of_le_of_lt (le_add_right _ _) this
-      · simpa using (Ordinal.mul_le_mul_iff_left <| opow_pos (repr e') omega_pos).2
+      · simpa using (Ordinal.mul_le_mul_iff_left <| opow_pos (repr e') omega0_pos).2
           (natCast_le.2 n'.pos)
     · rw [ee, ← add_assoc, ← mul_add]
 
@@ -503,7 +512,7 @@ theorem repr_sub : ∀ (o₁ o₂) [NF o₁] [NF o₂], repr (o₁ - o₂) = rep
         simpa using mul_le_mul_left' (natCast_le.2 <| Nat.succ_pos _) _
     · exact
         (Ordinal.sub_eq_of_add_eq <|
-            add_absorp (h₂.below_of_lt ee).repr_lt <| omega_le_oadd _ _ _).symm
+            add_absorp (h₂.below_of_lt ee).repr_lt <| omega0_le_oadd _ _ _).symm
 
 /-- Multiplication of ordinal notations (correct only for normal input) -/
 def mul : ONote → ONote → ONote
@@ -557,7 +566,7 @@ theorem repr_mul : ∀ (o₁ o₂) [NF o₁] [NF o₂], repr (o₁ * o₂) = rep
       simp [(· * ·)]
     have ao : repr a₁ + ω ^ repr e₁ * (n₁ : ℕ) = ω ^ repr e₁ * (n₁ : ℕ) := by
       apply add_absorp h₁.snd'.repr_lt
-      simpa using (Ordinal.mul_le_mul_iff_left <| opow_pos _ omega_pos).2 (natCast_le.2 n₁.2)
+      simpa using (Ordinal.mul_le_mul_iff_left <| opow_pos _ omega0_pos).2 (natCast_le.2 n₁.2)
     by_cases e0 : e₂ = 0
     · cases' Nat.exists_eq_succ_of_ne_zero n₂.ne_zero with x xe
       simp only [e0, repr, PNat.mul_coe, natCast_mul, opow_zero, one_mul]
@@ -570,8 +579,8 @@ theorem repr_mul : ∀ (o₁ o₂) [NF o₁] [NF o₂], repr (o₁ * o₂) = rep
       rw [← mul_assoc]
       congr 2
       have := mt repr_inj.1 e0
-      rw [add_mul_limit ao (opow_isLimit_left omega_isLimit this), mul_assoc,
-        mul_omega_dvd (natCast_pos.2 n₁.pos) (nat_lt_omega _)]
+      rw [add_mul_limit ao (opow_isLimit_left omega0_isLimit this), mul_assoc,
+        mul_omega0_dvd (natCast_pos.2 n₁.pos) (nat_lt_omega0 _)]
       simpa using opow_dvd_opow ω (one_le_iff_ne_zero.2 this)
 
 /-- Calculate division and remainder of `o` mod ω.
@@ -680,7 +689,7 @@ theorem nf_repr_split' : ∀ {o o' m} [NF o], split' o = (o', m) → NF o' ∧ r
       · simp at this ⊢
         refine
           IH₁.below_of_lt'
-            ((Ordinal.mul_lt_mul_iff_left omega_pos).1 <| lt_of_le_of_lt (le_add_right _ m') ?_)
+            ((Ordinal.mul_lt_mul_iff_left omega0_pos).1 <| lt_of_le_of_lt (le_add_right _ m') ?_)
         rw [← this, ← IH₂]
         exact h.snd'.repr_lt
       · rw [this]
@@ -723,9 +732,9 @@ theorem split_dvd {o o' m} [NF o] (h : split o = (o', m)) : ω ∣ repr o' := by
 theorem split_add_lt {o e n a m} [NF o] (h : split o = (oadd e n a, m)) :
     repr a + m < ω ^ repr e := by
   cases' nf_repr_split h with h₁ h₂
-  cases' h₁.of_dvd_omega (split_dvd h) with e0 d
-  apply principal_add_omega_opow _ h₁.snd'.repr_lt (lt_of_lt_of_le (nat_lt_omega _) _)
-  simpa using opow_le_opow_right omega_pos (one_le_iff_ne_zero.2 e0)
+  cases' h₁.of_dvd_omega0 (split_dvd h) with e0 d
+  apply principal_add_omega0_opow _ h₁.snd'.repr_lt (lt_of_lt_of_le (nat_lt_omega0 _) _)
+  simpa using opow_le_opow_right omega0_pos (one_le_iff_ne_zero.2 e0)
 
 @[simp]
 theorem mulNat_eq_mul (n o) : mulNat o n = o * ofNat n := by cases o <;> cases n <;> rfl
@@ -781,22 +790,22 @@ theorem repr_opow_aux₁ {e a} [Ne : NF e] [Na : NF a] {a' : Ordinal} (e0 : repr
       (ω ^ repr e) ^ (ω : Ordinal.{0}) := by
   subst aa
   have No := Ne.oadd n (Na.below_of_lt' h)
-  have := omega_le_oadd e n a
+  have := omega0_le_oadd e n a
   rw [repr] at this
   refine le_antisymm ?_ (opow_le_opow_left _ this)
-  apply (opow_le_of_limit ((opow_pos _ omega_pos).trans_le this).ne' omega_isLimit).2
+  apply (opow_le_of_limit ((opow_pos _ omega0_pos).trans_le this).ne' omega0_isLimit).2
   intro b l
   have := (No.below_of_lt (lt_succ _)).repr_lt
   rw [repr] at this
   apply (opow_le_opow_left b <| this.le).trans
   rw [← opow_mul, ← opow_mul]
-  apply opow_le_opow_right omega_pos
+  apply opow_le_opow_right omega0_pos
   rcases le_or_lt ω (repr e) with h | h
   · apply (mul_le_mul_left' (le_succ b) _).trans
-    rw [← add_one_eq_succ, add_mul_succ _ (one_add_of_omega_le h), add_one_eq_succ, succ_le_iff,
+    rw [← add_one_eq_succ, add_mul_succ _ (one_add_of_omega0_le h), add_one_eq_succ, succ_le_iff,
       Ordinal.mul_lt_mul_iff_left (Ordinal.pos_iff_ne_zero.2 e0)]
-    exact omega_isLimit.2 _ l
-  · apply (principal_mul_omega (omega_isLimit.2 _ h) l).le.trans
+    exact omega0_isLimit.2 _ l
+  · apply (principal_mul_omega0 (omega0_isLimit.2 _ h) l).le.trans
     simpa using mul_le_mul_right' (one_le_iff_ne_zero.2 e0) ω
 
 section
@@ -827,30 +836,30 @@ theorem repr_opow_aux₂ {a0 a'} [N0 : NF a0] [Na' : NF a'] (m : ℕ) (d : ω 
     · simp only [R', ONote.repr_scale, ONote.repr, ONote.mulNat_eq_mul, ONote.opowAux,
         ONote.repr_ofNat, ONote.repr_mul, ONote.repr_add, Ordinal.opow_mul, ONote.zero_add]
   have α0 : 0 < α' := by simpa [lt_def, repr] using oadd_pos a0 n a'
-  have ω00 : 0 < ω0 ^ (k : Ordinal) := opow_pos _ (opow_pos _ omega_pos)
+  have ω00 : 0 < ω0 ^ (k : Ordinal) := opow_pos _ (opow_pos _ omega0_pos)
   have Rl : R < ω ^ (repr a0 * succ ↑k) := by
     by_cases k0 : k = 0
     · simp only [k0, Nat.cast_zero, succ_zero, mul_one, R]
-      refine lt_of_lt_of_le ?_ (opow_le_opow_right omega_pos (one_le_iff_ne_zero.2 e0))
-      cases' m with m <;> simp [opowAux, omega_pos]
+      refine lt_of_lt_of_le ?_ (opow_le_opow_right omega0_pos (one_le_iff_ne_zero.2 e0))
+      cases' m with m <;> simp [opowAux, omega0_pos]
       rw [← add_one_eq_succ, ← Nat.cast_succ]
-      apply nat_lt_omega
+      apply nat_lt_omega0
     · rw [opow_mul]
       exact IH.1 k0
   refine ⟨fun _ => ?_, ?_⟩
   · rw [RR, ← opow_mul _ _ (succ k.succ)]
     have e0 := Ordinal.pos_iff_ne_zero.2 e0
     have rr0 : 0 < repr a0 + repr a0 := lt_of_lt_of_le e0 (le_add_left _ _)
-    apply principal_add_omega_opow
+    apply principal_add_omega0_opow
     · simp only [Nat.succ_eq_add_one, Nat.cast_add, Nat.cast_one, add_one_eq_succ,
         opow_mul, opow_succ, mul_assoc]
       rw [Ordinal.mul_lt_mul_iff_left ω00, ← Ordinal.opow_add]
       have : _ < ω ^ (repr a0 + repr a0) := (No.below_of_lt ?_).repr_lt
-      · exact mul_lt_omega_opow rr0 this (nat_lt_omega _)
+      · exact mul_lt_omega0_opow rr0 this (nat_lt_omega0 _)
       · simpa using (add_lt_add_iff_left (repr a0)).2 e0
     · exact
         lt_of_lt_of_le Rl
-          (opow_le_opow_right omega_pos <|
+          (opow_le_opow_right omega0_pos <|
             mul_le_mul_left' (succ_le_succ_iff.2 (natCast_le.2 (le_of_lt k.lt_succ_self))) _)
   calc
     (ω0 ^ (k.succ : Ordinal)) * α' + R'
@@ -862,10 +871,10 @@ theorem repr_opow_aux₂ {a0 a'} [N0 : NF a0] [Na' : NF a'] (m : ℕ) (d : ω 
   · have αd : ω ∣ α' :=
       dvd_add (dvd_mul_of_dvd_left (by simpa using opow_dvd_opow ω (one_le_iff_ne_zero.2 e0)) _) d
     rw [mul_add (ω0 ^ (k : Ordinal)), add_assoc, ← mul_assoc, ← opow_succ,
-      add_mul_limit _ (isLimit_iff_omega_dvd.2 ⟨ne_of_gt α0, αd⟩), mul_assoc,
-      @mul_omega_dvd n (natCast_pos.2 n.pos) (nat_lt_omega _) _ αd]
+      add_mul_limit _ (isLimit_iff_omega0_dvd.2 ⟨ne_of_gt α0, αd⟩), mul_assoc,
+      @mul_omega0_dvd n (natCast_pos.2 n.pos) (nat_lt_omega0 _) _ αd]
     apply @add_absorp _ (repr a0 * succ ↑k)
-    · refine principal_add_omega_opow _ ?_ Rl
+    · refine principal_add_omega0_opow _ ?_ Rl
       rw [opow_mul, opow_succ, Ordinal.mul_lt_mul_iff_left ω00]
       exact No.snd'.repr_lt
     · have := mul_le_mul_left' (one_le_iff_pos.2 <| natCast_pos.2 n.pos) (ω0 ^ succ (k : Ordinal))
@@ -878,7 +887,7 @@ theorem repr_opow_aux₂ {a0 a'} [N0 : NF a0] [Na' : NF a'] (m : ℕ) (d : ω 
       apply add_absorp Rl
       rw [opow_mul, opow_succ]
       apply mul_le_mul_left'
-      simpa [repr] using omega_le_oadd a0 n a'
+      simpa [repr] using omega0_le_oadd a0 n a'
 
 end
 
@@ -897,18 +906,18 @@ theorem repr_opow (o₁ o₂) [NF o₁] [NF o₂] : repr (o₁ ^ o₂) = repr o
       simp only [opow_def, opowAux2, opow, e₁, h, r₁, e₂, r₂, repr,
           opow_zero, Nat.succPNat_coe, Nat.cast_succ, Nat.cast_zero, _root_.zero_add, mul_one,
           add_zero, one_opow, npow_eq_pow]
-      rw [opow_add, opow_mul, opow_omega, add_one_eq_succ]
+      rw [opow_add, opow_mul, opow_omega0, add_one_eq_succ]
       · congr
         conv_lhs =>
           dsimp [(· ^ ·)]
           simp [Pow.pow, opow, Ordinal.succ_ne_zero]
         rw [opow_natCast]
       · simpa [Nat.one_le_iff_ne_zero]
-      · rw [← Nat.cast_succ, lt_omega]
+      · rw [← Nat.cast_succ, lt_omega0]
         exact ⟨_, rfl⟩
   · haveI := N₁.fst
     haveI := N₁.snd
-    cases' N₁.of_dvd_omega (split_dvd e₁) with a00 ad
+    cases' N₁.of_dvd_omega0 (split_dvd e₁) with a00 ad
     have al := split_add_lt e₁
     have aa : repr (a' + ofNat m) = repr a' + m := by
       simp only [eq_self_iff_true, ONote.repr_ofNat, ONote.repr_add]
@@ -955,13 +964,13 @@ private theorem exists_lt_add {α} [hα : Nonempty α] {o : Ordinal} {f : α →
     refine (H h).imp fun i H => ?_
     rwa [← Ordinal.add_sub_cancel_of_le h', add_lt_add_iff_left]
 
-private theorem exists_lt_mul_omega' {o : Ordinal} ⦃a⦄ (h : a < o * ω) :
+private theorem exists_lt_mul_omega0' {o : Ordinal} ⦃a⦄ (h : a < o * ω) :
     ∃ i : ℕ, a < o * ↑i + o := by
-  obtain ⟨i, hi, h'⟩ := (lt_mul_of_limit omega_isLimit).1 h
-  obtain ⟨i, rfl⟩ := lt_omega.1 hi
+  obtain ⟨i, hi, h'⟩ := (lt_mul_of_limit omega0_isLimit).1 h
+  obtain ⟨i, rfl⟩ := lt_omega0.1 hi
   exact ⟨i, h'.trans_le (le_add_right _ _)⟩
 
-private theorem exists_lt_omega_opow' {α} {o b : Ordinal} (hb : 1 < b) (ho : o.IsLimit)
+private theorem exists_lt_omega0_opow' {α} {o b : Ordinal} (hb : 1 < b) (ho : o.IsLimit)
     {f : α → Ordinal} (H : ∀ ⦃a⦄, a < o → ∃ i, a < f i) ⦃a⦄ (h : a < b ^ o) :
         ∃ i, a < b ^ f i := by
   obtain ⟨d, hd, h'⟩ := (lt_opow_of_limit (zero_lt_one.trans hb).ne' ho).1 h
@@ -1014,39 +1023,40 @@ theorem fundamentalSequence_has_prop (o) : FundamentalSequenceProp o (fundamenta
             have := PNat.natPred_add_one m; rw [e'] at this; exact PNat.coe_inj.1 this.symm]) <;>
       (try rw [show m = (m' + 1).succPNat by
               rw [← e', ← PNat.coe_inj, Nat.succPNat_coe, ← Nat.add_one, PNat.natPred_add_one]]) <;>
-      simp only [repr, iha, ihb, opow_lt_opow_iff_right one_lt_omega, add_lt_add_iff_left, add_zero,
-        eq_self_iff_true, lt_add_iff_pos_right, lt_def, mul_one, Nat.cast_zero, Nat.cast_succ,
-        Nat.succPNat_coe, opow_succ, opow_zero, mul_add_one, PNat.one_coe, succ_zero,
+      simp only [repr, iha, ihb, opow_lt_opow_iff_right one_lt_omega0, add_lt_add_iff_left,
+        add_zero, eq_self_iff_true, lt_add_iff_pos_right, lt_def, mul_one, Nat.cast_zero,
+        Nat.cast_succ, Nat.succPNat_coe, opow_succ, opow_zero, mul_add_one, PNat.one_coe, succ_zero,
         _root_.zero_add, zero_def]
     · decide
     · exact ⟨rfl, inferInstance⟩
-    · have := opow_pos (repr a') omega_pos
+    · have := opow_pos (repr a') omega0_pos
       refine
-        ⟨mul_isLimit this omega_isLimit, fun i =>
-          ⟨this, ?_, fun H => @NF.oadd_zero _ _ (iha.2 H.fst)⟩, exists_lt_mul_omega'⟩
+        ⟨mul_isLimit this omega0_isLimit, fun i =>
+          ⟨this, ?_, fun H => @NF.oadd_zero _ _ (iha.2 H.fst)⟩, exists_lt_mul_omega0'⟩
       rw [← mul_succ, ← natCast_succ, Ordinal.mul_lt_mul_iff_left this]
-      apply nat_lt_omega
-    · have := opow_pos (repr a') omega_pos
+      apply nat_lt_omega0
+    · have := opow_pos (repr a') omega0_pos
       refine
-        ⟨add_isLimit _ (mul_isLimit this omega_isLimit), fun i => ⟨this, ?_, ?_⟩,
-          exists_lt_add exists_lt_mul_omega'⟩
+        ⟨add_isLimit _ (mul_isLimit this omega0_isLimit), fun i => ⟨this, ?_, ?_⟩,
+          exists_lt_add exists_lt_mul_omega0'⟩
       · rw [← mul_succ, ← natCast_succ, Ordinal.mul_lt_mul_iff_left this]
-        apply nat_lt_omega
+        apply nat_lt_omega0
       · refine fun H => H.fst.oadd _ (NF.below_of_lt' ?_ (@NF.oadd_zero _ _ (iha.2 H.fst)))
         rw [repr, ← zero_def, repr, add_zero, iha.1, opow_succ, Ordinal.mul_lt_mul_iff_left this]
-        apply nat_lt_omega
+        apply nat_lt_omega0
     · rcases iha with ⟨h1, h2, h3⟩
-      refine ⟨opow_isLimit one_lt_omega h1, fun i => ?_, exists_lt_omega_opow' one_lt_omega h1 h3⟩
+      refine ⟨opow_isLimit one_lt_omega0 h1, fun i => ?_,
+        exists_lt_omega0_opow' one_lt_omega0 h1 h3⟩
       obtain ⟨h4, h5, h6⟩ := h2 i
       exact ⟨h4, h5, fun H => @NF.oadd_zero _ _ (h6 H.fst)⟩
     · rcases iha with ⟨h1, h2, h3⟩
       refine
-        ⟨add_isLimit _ (opow_isLimit one_lt_omega h1), fun i => ?_,
-          exists_lt_add (exists_lt_omega_opow' one_lt_omega h1 h3)⟩
+        ⟨add_isLimit _ (opow_isLimit one_lt_omega0 h1), fun i => ?_,
+          exists_lt_add (exists_lt_omega0_opow' one_lt_omega0 h1 h3)⟩
       obtain ⟨h4, h5, h6⟩ := h2 i
       refine ⟨h4, h5, fun H => H.fst.oadd _ (NF.below_of_lt' ?_ (@NF.oadd_zero _ _ (h6 H.fst)))⟩
       rwa [repr, ← zero_def, repr, add_zero, PNat.one_coe, Nat.cast_one, mul_one,
-        opow_lt_opow_iff_right one_lt_omega]
+        opow_lt_opow_iff_right one_lt_omega0]
   · refine ⟨by
       rw [repr, ihb.1, add_succ, repr], fun H => H.fst.oadd _ (NF.below_of_lt' ?_ (ihb.2 H.snd))⟩
     have := H.snd'.repr_lt
diff --git a/Mathlib/SetTheory/Ordinal/Principal.lean b/Mathlib/SetTheory/Ordinal/Principal.lean
index f149eea4b37a46..2835fd286b3f39 100644
--- a/Mathlib/SetTheory/Ordinal/Principal.lean
+++ b/Mathlib/SetTheory/Ordinal/Principal.lean
@@ -14,9 +14,9 @@ We define principal or indecomposable ordinals, and we prove the standard proper
 * `Principal`: A principal or indecomposable ordinal under some binary operation. We include 0 and
   any other typically excluded edge cases for simplicity.
 * `unbounded_principal`: Principal ordinals are unbounded.
-* `principal_add_iff_zero_or_omega_opow`: The main characterization theorem for additive principal
+* `principal_add_iff_zero_or_omega0_opow`: The main characterization theorem for additive principal
   ordinals.
-* `principal_mul_iff_le_two_or_omega_opow_opow`: The main characterization theorem for
+* `principal_mul_iff_le_two_or_omega0_opow_opow`: The main characterization theorem for
   multiplicative principal ordinals.
 
 ## TODO
@@ -163,39 +163,51 @@ theorem principal_add_iff_add_lt_ne_self {a} :
     rcases exists_lt_add_of_not_principal_add ha with ⟨b, hb, c, hc, rfl⟩
     exact (H b hb c hc).irrefl⟩
 
-theorem add_omega {a : Ordinal} (h : a < ω) : a + ω = ω := by
-  rcases lt_omega.1 h with ⟨n, rfl⟩
+theorem add_omega0 {a : Ordinal} (h : a < ω) : a + ω = ω := by
+  rcases lt_omega0.1 h with ⟨n, rfl⟩
   clear h; induction' n with n IH
   · rw [Nat.cast_zero, zero_add]
-  · rwa [Nat.cast_succ, add_assoc, one_add_of_omega_le (le_refl _)]
+  · rwa [Nat.cast_succ, add_assoc, one_add_of_omega0_le (le_refl _)]
 
-theorem principal_add_omega : Principal (· + ·) ω :=
-  principal_add_iff_add_left_eq_self.2 fun _ => add_omega
+@[deprecated (since := "2024-09-30")]
+alias add_omega := add_omega0
 
-theorem add_omega_opow {a b : Ordinal} (h : a < ω ^ b) : a + ω ^ b = ω ^ b := by
+theorem principal_add_omega0 : Principal (· + ·) ω :=
+  principal_add_iff_add_left_eq_self.2 fun _ => add_omega0
+
+@[deprecated (since := "2024-09-30")]
+alias principal_add_omega := principal_add_omega0
+
+theorem add_omega0_opow {a b : Ordinal} (h : a < ω ^ b) : a + ω ^ b = ω ^ b := by
   refine le_antisymm ?_ (le_add_left _ a)
   induction' b using limitRecOn with b _ b l IH
   · rw [opow_zero, ← succ_zero, lt_succ_iff, Ordinal.le_zero] at h
     rw [h, zero_add]
   · rw [opow_succ] at h
-    rcases (lt_mul_of_limit omega_isLimit).1 h with ⟨x, xo, ax⟩
+    rcases (lt_mul_of_limit omega0_isLimit).1 h with ⟨x, xo, ax⟩
     apply (add_le_add_right ax.le _).trans
-    rw [opow_succ, ← mul_add, add_omega xo]
-  · rcases (lt_opow_of_limit omega_ne_zero l).1 h with ⟨x, xb, ax⟩
-    apply (((add_isNormal a).trans <| opow_isNormal one_lt_omega).limit_le l).2
+    rw [opow_succ, ← mul_add, add_omega0 xo]
+  · rcases (lt_opow_of_limit omega0_ne_zero l).1 h with ⟨x, xb, ax⟩
+    apply (((add_isNormal a).trans <| opow_isNormal one_lt_omega0).limit_le l).2
     intro y yb
     calc a + ω ^ y ≤ a + ω ^ max x y :=
-      add_le_add_left (opow_le_opow_right omega_pos (le_max_right x y)) _
+      add_le_add_left (opow_le_opow_right omega0_pos (le_max_right x y)) _
     _ ≤ ω ^ max x y :=
-      IH _ (max_lt xb yb) <| ax.trans_le <| opow_le_opow_right omega_pos <| le_max_left x y
+      IH _ (max_lt xb yb) <| ax.trans_le <| opow_le_opow_right omega0_pos <| le_max_left x y
     _ ≤ ω ^ b :=
-      opow_le_opow_right omega_pos <| (max_lt xb yb).le
+      opow_le_opow_right omega0_pos <| (max_lt xb yb).le
+
+@[deprecated (since := "2024-09-30")]
+alias add_omega_opow := add_omega0_opow
+
+theorem principal_add_omega0_opow (o : Ordinal) : Principal (· + ·) (ω ^ o) :=
+  principal_add_iff_add_left_eq_self.2 fun _ => add_omega0_opow
 
-theorem principal_add_omega_opow (o : Ordinal) : Principal (· + ·) (ω ^ o) :=
-  principal_add_iff_add_left_eq_self.2 fun _ => add_omega_opow
+@[deprecated (since := "2024-09-30")]
+alias principal_add_omega_opow := principal_add_omega0_opow
 
 /-- The main characterization theorem for additive principal ordinals. -/
-theorem principal_add_iff_zero_or_omega_opow {o : Ordinal} :
+theorem principal_add_iff_zero_or_omega0_opow {o : Ordinal} :
     Principal (· + ·) o ↔ o = 0 ∨ o ∈ Set.range (ω ^ · : Ordinal → Ordinal) := by
   rcases eq_or_ne o 0 with (rfl | ho)
   · simp only [principal_zero, Or.inl]
@@ -203,12 +215,12 @@ theorem principal_add_iff_zero_or_omega_opow {o : Ordinal} :
     simp only [ho, false_or]
     refine
       ⟨fun H => ⟨_, ((lt_or_eq_of_le (opow_log_le_self _ ho)).resolve_left fun h => ?_)⟩,
-        fun ⟨b, e⟩ => e.symm ▸ fun a => add_omega_opow⟩
+        fun ⟨b, e⟩ => e.symm ▸ fun a => add_omega0_opow⟩
     have := H _ h
-    have := lt_opow_succ_log_self one_lt_omega o
-    rw [opow_succ, lt_mul_of_limit omega_isLimit] at this
+    have := lt_opow_succ_log_self one_lt_omega0 o
+    rw [opow_succ, lt_mul_of_limit omega0_isLimit] at this
     rcases this with ⟨a, ao, h'⟩
-    rcases lt_omega.1 ao with ⟨n, rfl⟩
+    rcases lt_omega0.1 ao with ⟨n, rfl⟩
     clear ao
     revert h'
     apply not_lt_of_le
@@ -218,18 +230,21 @@ theorem principal_add_iff_zero_or_omega_opow {o : Ordinal} :
     · simp [Nat.cast_zero, mul_zero, zero_add]
     · simp only [Nat.cast_succ, mul_add_one, add_assoc, this, IH]
 
+@[deprecated (since := "2024-09-30")]
+alias principal_add_iff_zero_or_omega_opow := principal_add_iff_zero_or_omega0_opow
+
 theorem opow_principal_add_of_principal_add {a} (ha : Principal (· + ·) a) (b : Ordinal) :
     Principal (· + ·) (a ^ b) := by
-  rcases principal_add_iff_zero_or_omega_opow.1 ha with (rfl | ⟨c, rfl⟩)
+  rcases principal_add_iff_zero_or_omega0_opow.1 ha with (rfl | ⟨c, rfl⟩)
   · rcases eq_or_ne b 0 with (rfl | hb)
     · rw [opow_zero]
       exact principal_add_one
     · rwa [zero_opow hb]
   · rw [← opow_mul]
-    exact principal_add_omega_opow _
+    exact principal_add_omega0_opow _
 
 theorem add_absorp {a b c : Ordinal} (h₁ : a < ω ^ b) (h₂ : ω ^ b ≤ c) : a + c = c := by
-  rw [← Ordinal.add_sub_cancel_of_le h₂, ← add_assoc, add_omega_opow h₁]
+  rw [← Ordinal.add_sub_cancel_of_le h₂, ← add_assoc, add_omega0_opow h₁]
 
 theorem mul_principal_add_is_principal_add (a : Ordinal.{u}) {b : Ordinal.{u}} (hb₁ : b ≠ 1)
     (hb : Principal (· + ·) b) : Principal (· + ·) (a * b) := by
@@ -302,44 +317,59 @@ theorem principal_mul_iff_mul_left_eq {o : Ordinal} :
     rw [← h a ha hao]
     exact (mul_isNormal ha).strictMono hbo
 
-theorem principal_mul_omega : Principal (· * ·) ω := fun a b ha hb =>
-  match a, b, lt_omega.1 ha, lt_omega.1 hb with
+theorem principal_mul_omega0 : Principal (· * ·) ω := fun a b ha hb =>
+  match a, b, lt_omega0.1 ha, lt_omega0.1 hb with
   | _, _, ⟨m, rfl⟩, ⟨n, rfl⟩ => by
     dsimp only; rw [← natCast_mul]
-    apply nat_lt_omega
+    apply nat_lt_omega0
+
+@[deprecated (since := "2024-09-30")]
+alias principal_mul_omega := principal_mul_omega0
+
+theorem mul_omega0 {a : Ordinal} (a0 : 0 < a) (ha : a < ω) : a * ω = ω :=
+  principal_mul_iff_mul_left_eq.1 principal_mul_omega0 a a0 ha
 
-theorem mul_omega {a : Ordinal} (a0 : 0 < a) (ha : a < ω) : a * ω = ω :=
-  principal_mul_iff_mul_left_eq.1 principal_mul_omega a a0 ha
+@[deprecated (since := "2024-09-30")]
+alias mul_omega := mul_omega0
 
-theorem mul_lt_omega_opow {a b c : Ordinal} (c0 : 0 < c) (ha : a < ω ^ c) (hb : b < ω) :
+theorem mul_lt_omega0_opow {a b c : Ordinal} (c0 : 0 < c) (ha : a < ω ^ c) (hb : b < ω) :
     a * b < ω ^ c := by
   rcases zero_or_succ_or_limit c with (rfl | ⟨c, rfl⟩ | l)
   · exact (lt_irrefl _).elim c0
   · rw [opow_succ] at ha
-    rcases ((mul_isNormal <| opow_pos _ omega_pos).limit_lt omega_isLimit).1 ha with ⟨n, hn, an⟩
+    rcases ((mul_isNormal <| opow_pos _ omega0_pos).limit_lt omega0_isLimit).1 ha with ⟨n, hn, an⟩
     apply (mul_le_mul_right' (le_of_lt an) _).trans_lt
-    rw [opow_succ, mul_assoc, mul_lt_mul_iff_left (opow_pos _ omega_pos)]
-    exact principal_mul_omega hn hb
-  · rcases ((opow_isNormal one_lt_omega).limit_lt l).1 ha with ⟨x, hx, ax⟩
+    rw [opow_succ, mul_assoc, mul_lt_mul_iff_left (opow_pos _ omega0_pos)]
+    exact principal_mul_omega0 hn hb
+  · rcases ((opow_isNormal one_lt_omega0).limit_lt l).1 ha with ⟨x, hx, ax⟩
     refine (mul_le_mul' (le_of_lt ax) (le_of_lt hb)).trans_lt ?_
-    rw [← opow_succ, opow_lt_opow_iff_right one_lt_omega]
+    rw [← opow_succ, opow_lt_opow_iff_right one_lt_omega0]
     exact l.2 _ hx
 
-theorem mul_omega_opow_opow {a b : Ordinal} (a0 : 0 < a) (h : a < ω ^ ω ^ b) :
+@[deprecated (since := "2024-09-30")]
+alias mul_lt_omega_opow := mul_lt_omega0_opow
+
+theorem mul_omega0_opow_opow {a b : Ordinal} (a0 : 0 < a) (h : a < ω ^ ω ^ b) :
     a * ω ^ ω ^ b = ω ^ ω ^ b := by
   obtain rfl | b0 := eq_or_ne b 0
   · rw [opow_zero, opow_one] at h ⊢
-    exact mul_omega a0 h
+    exact mul_omega0 a0 h
   · apply le_antisymm
     · obtain ⟨x, xb, ax⟩ :=
-        (lt_opow_of_limit omega_ne_zero (opow_isLimit_left omega_isLimit b0)).1 h
+        (lt_opow_of_limit omega0_ne_zero (opow_isLimit_left omega0_isLimit b0)).1 h
       apply (mul_le_mul_right' (le_of_lt ax) _).trans
-      rw [← opow_add, add_omega_opow xb]
+      rw [← opow_add, add_omega0_opow xb]
     · conv_lhs => rw [← one_mul (ω ^ _)]
       exact mul_le_mul_right' (one_le_iff_pos.2 a0) _
 
-theorem principal_mul_omega_opow_opow (o : Ordinal) : Principal (· * ·) (ω ^ ω ^ o) :=
-  principal_mul_iff_mul_left_eq.2 fun _ => mul_omega_opow_opow
+@[deprecated (since := "2024-09-30")]
+alias mul_omega_opow_opow := mul_omega0_opow_opow
+
+theorem principal_mul_omega0_opow_opow (o : Ordinal) : Principal (· * ·) (ω ^ ω ^ o) :=
+  principal_mul_iff_mul_left_eq.2 fun _ => mul_omega0_opow_opow
+
+@[deprecated (since := "2024-09-30")]
+alias principal_mul_omega_opow_opow := principal_mul_omega0_opow_opow
 
 theorem principal_add_of_principal_mul_opow {o b : Ordinal} (hb : 1 < b)
     (ho : Principal (· * ·) (b ^ o)) : Principal (· + ·) o := by
@@ -349,24 +379,30 @@ theorem principal_add_of_principal_mul_opow {o b : Ordinal} (hb : 1 < b)
   rwa [← opow_add, opow_lt_opow_iff_right hb] at this
 
 /-- The main characterization theorem for multiplicative principal ordinals. -/
-theorem principal_mul_iff_le_two_or_omega_opow_opow {o : Ordinal} :
+theorem principal_mul_iff_le_two_or_omega0_opow_opow {o : Ordinal} :
     Principal (· * ·) o ↔ o ≤ 2 ∨ o ∈ Set.range (ω ^ ω ^ · : Ordinal → Ordinal) := by
   refine ⟨fun ho => ?_, ?_⟩
   · rcases le_or_lt o 2 with ho₂ | ho₂
     · exact Or.inl ho₂
-    · rcases principal_add_iff_zero_or_omega_opow.1 (principal_add_of_principal_mul ho ho₂.ne') with
-      (rfl | ⟨a, rfl⟩)
+    · rcases principal_add_iff_zero_or_omega0_opow.1 (principal_add_of_principal_mul ho ho₂.ne')
+        with (rfl | ⟨a, rfl⟩)
       · exact (Ordinal.not_lt_zero 2 ho₂).elim
-      · rcases principal_add_iff_zero_or_omega_opow.1
-          (principal_add_of_principal_mul_opow one_lt_omega ho) with (rfl | ⟨b, rfl⟩)
+      · rcases principal_add_iff_zero_or_omega0_opow.1
+          (principal_add_of_principal_mul_opow one_lt_omega0 ho) with (rfl | ⟨b, rfl⟩)
         · simp
         · exact Or.inr ⟨b, rfl⟩
   · rintro (ho₂ | ⟨a, rfl⟩)
     · exact principal_mul_of_le_two ho₂
-    · exact principal_mul_omega_opow_opow a
+    · exact principal_mul_omega0_opow_opow a
+
+@[deprecated (since := "2024-09-30")]
+alias principal_mul_iff_le_two_or_omega_opow_opow := principal_mul_iff_le_two_or_omega0_opow_opow
 
-theorem mul_omega_dvd {a : Ordinal} (a0 : 0 < a) (ha : a < ω) : ∀ {b}, ω ∣ b → a * b = b
-  | _, ⟨b, rfl⟩ => by rw [← mul_assoc, mul_omega a0 ha]
+theorem mul_omega0_dvd {a : Ordinal} (a0 : 0 < a) (ha : a < ω) : ∀ {b}, ω ∣ b → a * b = b
+  | _, ⟨b, rfl⟩ => by rw [← mul_assoc, mul_omega0 a0 ha]
+
+@[deprecated (since := "2024-09-30")]
+alias mul_omega_dvd := mul_omega0_dvd
 
 theorem mul_eq_opow_log_succ {a b : Ordinal.{u}} (ha : a ≠ 0) (hb : Principal (· * ·) b)
     (hb₂ : 2 < b) : a * b = b ^ succ (log b a) := by
@@ -387,15 +423,21 @@ theorem mul_eq_opow_log_succ {a b : Ordinal.{u}} (ha : a ≠ 0) (hb : Principal
 /-! #### Exponential principal ordinals -/
 
 
-theorem principal_opow_omega : Principal (· ^ ·) ω := fun a b ha hb =>
-  match a, b, lt_omega.1 ha, lt_omega.1 hb with
+theorem principal_opow_omega0 : Principal (· ^ ·) ω := fun a b ha hb =>
+  match a, b, lt_omega0.1 ha, lt_omega0.1 hb with
   | _, _, ⟨m, rfl⟩, ⟨n, rfl⟩ => by
     simp_rw [← natCast_opow]
-    apply nat_lt_omega
+    apply nat_lt_omega0
+
+@[deprecated (since := "2024-09-30")]
+alias principal_opow_omega := principal_opow_omega0
 
-theorem opow_omega {a : Ordinal} (a1 : 1 < a) (h : a < ω) : a ^ ω = ω :=
-  ((opow_le_of_limit (one_le_iff_ne_zero.1 <| le_of_lt a1) omega_isLimit).2 fun _ hb =>
-      (principal_opow_omega h hb).le).antisymm
+theorem opow_omega0 {a : Ordinal} (a1 : 1 < a) (h : a < ω) : a ^ ω = ω :=
+  ((opow_le_of_limit (one_le_iff_ne_zero.1 <| le_of_lt a1) omega0_isLimit).2 fun _ hb =>
+      (principal_opow_omega0 h hb).le).antisymm
   (right_le_opow _ a1)
 
+@[deprecated (since := "2024-09-30")]
+alias opow_omega := opow_omega0
+
 end Ordinal
diff --git a/scripts/no_lints_prime_decls.txt b/scripts/no_lints_prime_decls.txt
index d66cd78fe7c09b..61a8f1beba4017 100644
--- a/scripts/no_lints_prime_decls.txt
+++ b/scripts/no_lints_prime_decls.txt
@@ -3514,8 +3514,8 @@ one_ne_zero'
 OnePoint.continuousAt_infty'
 OnePoint.isOpen_iff_of_mem'
 OnePoint.tendsto_nhds_infty'
-ONote.exists_lt_mul_omega'
-ONote.exists_lt_omega_opow'
+ONote.exists_lt_mul_omega0'
+ONote.exists_lt_omega0_opow'
 ONote.fastGrowing_zero'
 ONote.NF.below_of_lt'
 ONote.nf_repr_split'