refactor(SetTheory/Ordinal/Basic): deprecate Ordinal.omega in favor o…

…f 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

@@ -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

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,21 +259,21 @@ 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' _)
   · rw [aleph_eq_aleph', aleph'_limit (ho.add _)]
     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
 /-!

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⟩))

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 =>

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,32 +2412,35 @@ 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")]
 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
 

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
 

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