refactor: standardize spelling of ℵ₁ as aleph_one (leanprover-community#33198)

See [Zulip](https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Cardinal.2Econtinuum/near/564917455).

Author: vihdzp

Mathlib/MeasureTheory/MeasurableSpace/Card.lean

@@ -105,7 +105,7 @@ theorem generateMeasurableRec_induction {s : Set (Set α)} {i : Ordinal} {t : Se
     obtain ⟨j, hj, hj'⟩ := mem_iUnion₂.1 (f n).2
     use IH j hj _ hj', j, hj.trans_le hk
 
-theorem generateMeasurableRec_omega1 (s : Set (Set α)) :
+theorem generateMeasurableRec_omega_one (s : Set (Set α)) :
     generateMeasurableRec s (ω₁ : Ordinal.{v}) =
       ⋃ i < (ω₁ : Ordinal.{v}), generateMeasurableRec s i := by
   apply (iUnion₂_subset fun i h => generateMeasurableRec_mono s h.le).antisymm'
@@ -126,6 +126,9 @@ theorem generateMeasurableRec_omega1 (s : Set (Set α)) :
     rw [mk_nat, lift_aleph0, isRegular_aleph_one.cof_omega_eq]
     exact aleph0_lt_aleph_one
 
+@[deprecated (since := "2025-12-22")]
+alias generateMeasurableRec_omega1 := generateMeasurableRec_omega_one
+
 theorem generateMeasurableRec_subset (s : Set (Set α)) (i : Ordinal) :
     generateMeasurableRec s i ⊆ { t | GenerateMeasurable s t } := by
   apply WellFoundedLT.induction i
@@ -141,28 +144,31 @@ theorem generateMeasurable_eq_rec (s : Set (Set α)) :
   | basic u hu => exact self_subset_generateMeasurableRec s _ hu
   | empty => exact empty_mem_generateMeasurableRec s _
   | compl u _ IH =>
-    rw [generateMeasurableRec_omega1, mem_iUnion₂] at IH
+    rw [generateMeasurableRec_omega_one, mem_iUnion₂] at IH
     obtain ⟨i, hi, hi'⟩ := IH
     exact generateMeasurableRec_mono _ ((isSuccLimit_omega 1).succ_lt hi).le
       (compl_mem_generateMeasurableRec (Order.lt_succ i) hi')
   | iUnion f _ IH =>
-    simp_rw [generateMeasurableRec_omega1, mem_iUnion₂, exists_prop] at IH
+    simp_rw [generateMeasurableRec_omega_one, mem_iUnion₂, exists_prop] at IH
     exact iUnion_mem_generateMeasurableRec IH
 
 /-- `generateMeasurableRec` is constant for ordinals `≥ ω₁`. -/
-theorem generateMeasurableRec_of_omega1_le (s : Set (Set α)) {i : Ordinal.{v}} (hi : ω₁ ≤ i) :
+theorem generateMeasurableRec_of_omega_one_le (s : Set (Set α)) {i : Ordinal.{v}} (hi : ω₁ ≤ i) :
     generateMeasurableRec s i = generateMeasurableRec s (ω₁ : Ordinal.{v}) := by
   apply (generateMeasurableRec_mono s hi).antisymm'
   rw [← generateMeasurable_eq_rec]
   exact generateMeasurableRec_subset s i
 
+@[deprecated (since := "2025-12-22")]
+alias generateMeasurableRec_of_omega1_le := generateMeasurableRec_of_omega_one_le
+
 /-- At each step of the inductive construction, the cardinality bound `≤ #s ^ ℵ₀` holds. -/
 theorem cardinal_generateMeasurableRec_le (s : Set (Set α)) (i : Ordinal.{v}) :
     #(generateMeasurableRec s i) ≤ max #s 2 ^ ℵ₀ := by
   suffices ∀ i ≤ ω₁, #(generateMeasurableRec s i) ≤ max #s 2 ^ ℵ₀ by
     obtain hi | hi := le_or_gt i ω₁
     · exact this i hi
-    · rw [generateMeasurableRec_of_omega1_le s hi.le]
+    · rw [generateMeasurableRec_of_omega_one_le s hi.le]
       exact this _ le_rfl
   intro i
   apply WellFoundedLT.induction i

Mathlib/SetTheory/Cardinal/Aleph.lean

@@ -196,11 +196,12 @@ For a version including finite ordinals, see `Ordinal.preOmega`. -/
 def omega : Ordinal ↪o Ordinal :=
   (OrderEmbedding.addLeft ω).trans preOmega
 
-@[inherit_doc]
-scoped notation "ω_ " => omega
+@[inherit_doc] scoped notation "ω_ " => omega
+recommended_spelling "omega" for "ω_" in [omega, «termω_»]
 
 /-- `ω₁` is the first uncountable ordinal. -/
 scoped notation "ω₁" => ω_ 1
+recommended_spelling "omega_one" for "ω₁" in [«termω₁»]
 
 theorem omega_eq_preOmega (o : Ordinal) : ω_ o = preOmega (ω + o) :=
   rfl
@@ -238,10 +239,13 @@ theorem omega0_le_omega (o : Ordinal) : ω ≤ ω_ o := by
 theorem omega_pos (o : Ordinal) : 0 < ω_ o :=
   omega0_pos.trans_le (omega0_le_omega o)
 
-theorem omega0_lt_omega1 : ω < ω₁ := by
+theorem omega0_lt_omega_one : ω < ω₁ := by
   rw [← omega_zero, omega_lt_omega]
   exact zero_lt_one
 
+@[deprecated (since := "2025-12-22")]
+alias omega0_lt_omega1 := omega0_lt_omega_one
+
 theorem isNormal_omega : IsNormal omega :=
   isNormal_preOmega.trans (isNormal_add_right _)
 
@@ -362,11 +366,12 @@ For a version including finite cardinals, see `Cardinal.preAleph`. -/
 def aleph : Ordinal ↪o Cardinal :=
   (OrderEmbedding.addLeft ω).trans preAleph.toOrderEmbedding
 
-@[inherit_doc]
-scoped notation "ℵ_ " => aleph
+@[inherit_doc] scoped notation "ℵ_ " => aleph
+recommended_spelling "aleph" for "ℵ_" in [aleph, «termℵ_»]
 
 /-- `ℵ₁` is the first uncountable cardinal. -/
 scoped notation "ℵ₁" => ℵ_ 1
+recommended_spelling "aleph_one" for "ℵ₁" in [«termℵ₁»]
 
 theorem aleph_eq_preAleph (o : Ordinal) : ℵ_ o = preAleph (ω + o) :=
   rfl
@@ -458,29 +463,47 @@ theorem countable_iff_lt_aleph_one {α : Type*} (s : Set α) : s.Countable ↔ #
   rw [← succ_aleph0, lt_succ_iff, le_aleph0_iff_set_countable]
 
 @[simp]
-theorem aleph1_le_lift {c : Cardinal.{u}} : ℵ₁ ≤ lift.{v} c ↔ ℵ₁ ≤ c := by
+theorem aleph_one_le_lift {c : Cardinal.{u}} : ℵ₁ ≤ lift.{v} c ↔ ℵ₁ ≤ c := by
   simpa using lift_le (a := ℵ₁)
 
+@[deprecated (since := "2025-12-22")]
+alias aleph1_le_lift := aleph_one_le_lift
+
 @[simp]
-theorem lift_le_aleph1 {c : Cardinal.{u}} : lift.{v} c ≤ ℵ₁ ↔ c ≤ ℵ₁ := by
+theorem lift_le_aleph_one {c : Cardinal.{u}} : lift.{v} c ≤ ℵ₁ ↔ c ≤ ℵ₁ := by
   simpa using lift_le (b := ℵ₁)
 
+@[deprecated (since := "2025-12-22")]
+alias lift_le_aleph1 := lift_le_aleph_one
+
 @[simp]
-theorem aleph1_lt_lift {c : Cardinal.{u}} : ℵ₁ < lift.{v} c ↔ ℵ₁ < c := by
+theorem aleph_one_lt_lift {c : Cardinal.{u}} : ℵ₁ < lift.{v} c ↔ ℵ₁ < c := by
   simpa using lift_lt (a := ℵ₁)
 
+@[deprecated (since := "2025-12-22")]
+alias aleph1_lt_lift := aleph_one_lt_lift
+
 @[simp]
-theorem lift_lt_aleph1 {c : Cardinal.{u}} : lift.{v} c < ℵ₁ ↔ c < ℵ₁ := by
+theorem lift_lt_aleph_one {c : Cardinal.{u}} : lift.{v} c < ℵ₁ ↔ c < ℵ₁ := by
   simpa using lift_lt (b := ℵ₁)
 
+@[deprecated (since := "2025-12-22")]
+alias lift_lt_aleph1 := lift_lt_aleph_one
+
 @[simp]
-theorem aleph1_eq_lift {c : Cardinal.{u}} : ℵ₁ = lift.{v} c ↔ ℵ₁ = c := by
+theorem aleph_one_eq_lift {c : Cardinal.{u}} : ℵ₁ = lift.{v} c ↔ ℵ₁ = c := by
   simpa using lift_inj (a := ℵ₁)
 
+@[deprecated (since := "2025-12-22")]
+alias aleph1_eq_lift := aleph_one_eq_lift
+
 @[simp]
-theorem lift_eq_aleph1 {c : Cardinal.{u}} : lift.{v} c = ℵ₁ ↔ c = ℵ₁ := by
+theorem lift_eq_aleph_one {c : Cardinal.{u}} : lift.{v} c = ℵ₁ ↔ c = ℵ₁ := by
   simpa using lift_inj (b := ℵ₁)
 
+@[deprecated (since := "2025-12-22")]
+alias lift_eq_aleph1 := lift_eq_aleph_one
+
 theorem lt_omega_iff_card_lt {x o : Ordinal} : x < ω_ o ↔ x.card < ℵ_ o := by
   rw [← (isInitial_omega o).card_lt_card, card_omega]
 
@@ -612,8 +635,8 @@ For a version which starts at zero, see `Cardinal.preBeth`. -/
 def beth (o : Ordinal.{u}) : Cardinal.{u} :=
   preBeth (ω + o)
 
-@[inherit_doc]
-scoped notation "ℶ_ " => beth
+@[inherit_doc] scoped notation "ℶ_ " => beth
+recommended_spelling "beth" for "ℶ_" in [«termℶ_»]
 
 theorem beth_eq_preBeth (o : Ordinal) : beth o = preBeth (ω + o) :=
   rfl

Mathlib/SetTheory/Cardinal/Defs.lean

@@ -474,8 +474,8 @@ theorem lift_prod {ι : Type u} (c : ι → Cardinal.{v}) :
 def aleph0 : Cardinal.{u} :=
   lift #ℕ
 
-@[inherit_doc]
-scoped notation "ℵ₀" => Cardinal.aleph0
+@[inherit_doc] scoped notation "ℵ₀" => Cardinal.aleph0
+recommended_spelling "aleph0" for "ℵ₀" in [aleph0, «termℵ₀»]
 
 theorem mk_nat : #ℕ = ℵ₀ :=
   (lift_id _).symm

Mathlib/SetTheory/Cardinal/Regular.lean

@@ -302,13 +302,16 @@ open Cardinal
 open scoped Ordinal
 
 -- TODO: generalize universes, and use ω₁.
-lemma iSup_sequence_lt_omega1 {α : Type u} [Countable α]
+lemma iSup_sequence_lt_omega_one {α : Type u} [Countable α]
     (o : α → Ordinal.{max u v}) (ho : ∀ n, o n < (aleph 1).ord) :
     iSup o < (aleph 1).ord := by
   apply iSup_lt_ord_lift _ ho
   rw [Cardinal.isRegular_aleph_one.cof_eq]
   exact lt_of_le_of_lt mk_le_aleph0 aleph0_lt_aleph_one
 
+@[deprecated (since := "2025-12-22")]
+alias iSup_sequence_lt_omega1 := iSup_sequence_lt_omega_one
+
 end Ordinal
 
 end Omega1

Mathlib/SetTheory/Ordinal/Basic.lean

@@ -760,13 +760,12 @@ theorem lt_lift_iff {a : Ordinal.{u}} {b : Ordinal.{max u v}} :
 
 /-! ### The first infinite ordinal ω -/
 
-
 /-- `ω` is the first infinite ordinal, defined as the order type of `ℕ`. -/
 def omega0 : Ordinal.{u} :=
   lift (typeLT ℕ)
 
-@[inherit_doc]
-scoped notation "ω" => Ordinal.omega0
+@[inherit_doc] scoped notation "ω" => Ordinal.omega0
+recommended_spelling "omega0" for "ω" in [omega0, «termω»]
 
 /-- Note that the presence of this lemma makes `simp [omega0]` form a loop. -/
 @[simp]