From 08804ac5cc5dca54e6979de8388f59c937b60e8a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Violeta=20Hern=C3=A1ndez?= <vi.hdz.p@gmail.com>
Date: Thu, 17 Oct 2024 03:53:08 +0000
Subject: [PATCH] =?UTF-8?q?chore(SetTheory/Ordinal/Arithmetic):=20`omega0?=
 =?UTF-8?q?=5FisLimit`=20=E2=86=92=20`isLimit=5Fomega0`=20(#17744)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

I missed this rename in #17673.
---
 Mathlib/SetTheory/Cardinal/Aleph.lean      |  6 +++---
 Mathlib/SetTheory/Cardinal/Arithmetic.lean |  2 +-
 Mathlib/SetTheory/Cardinal/Cofinality.lean | 12 ++++++------
 Mathlib/SetTheory/Ordinal/Arithmetic.lean  | 20 +++++++++++++-------
 Mathlib/SetTheory/Ordinal/Notation.lean    | 14 +++++++-------
 Mathlib/SetTheory/Ordinal/Principal.lean   | 10 +++++-----
 6 files changed, 35 insertions(+), 29 deletions(-)

diff --git a/Mathlib/SetTheory/Cardinal/Aleph.lean b/Mathlib/SetTheory/Cardinal/Aleph.lean
index 7a654d0363135..090dd44cb90c6 100644
--- a/Mathlib/SetTheory/Cardinal/Aleph.lean
+++ b/Mathlib/SetTheory/Cardinal/Aleph.lean
@@ -249,7 +249,7 @@ theorem aleph'_limit {o : Ordinal} (ho : o.IsLimit) : aleph' o = ⨆ a : Iio o,
 @[simp]
 theorem aleph'_omega0 : aleph' ω = ℵ₀ :=
   eq_of_forall_ge_iff fun c => by
-    simp only [aleph'_le_of_limit omega0_isLimit, lt_omega0, exists_imp, aleph0_le]
+    simp only [aleph'_le_of_limit isLimit_omega0, 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")]
@@ -333,12 +333,12 @@ instance nonempty_toType_aleph (o : Ordinal) : Nonempty (ℵ_ o).ord.toType := b
   exact fun h => (ord_injective h).not_gt (aleph_pos o)
 
 theorem ord_aleph_isLimit (o : Ordinal) : (ℵ_ o).ord.IsLimit :=
-  ord_isLimit <| aleph0_le_aleph _
+  isLimit_ord <| aleph0_le_aleph _
 
 instance (o : Ordinal) : NoMaxOrder (ℵ_ o).ord.toType :=
   toType_noMax_of_succ_lt (ord_aleph_isLimit o).2
 
-theorem exists_aleph {c : Cardinal} : ℵ₀ ≤ c ↔ ∃ o, c = aleph o :=
+theorem exists_aleph {c : Cardinal} : ℵ₀ ≤ c ↔ ∃ o, c = ℵ_ o :=
   ⟨fun h =>
     ⟨aleph'.symm c - ω, by
       rw [aleph_eq_aleph', Ordinal.add_sub_cancel_of_le, aleph'.apply_symm_apply]
diff --git a/Mathlib/SetTheory/Cardinal/Arithmetic.lean b/Mathlib/SetTheory/Cardinal/Arithmetic.lean
index 4bb8721a053d7..4dfd399fb40da 100644
--- a/Mathlib/SetTheory/Cardinal/Arithmetic.lean
+++ b/Mathlib/SetTheory/Cardinal/Arithmetic.lean
@@ -82,7 +82,7 @@ theorem mul_eq_self {c : Cardinal} (h : ℵ₀ ≤ c) : c * c = c := by
   · exact (mul_lt_aleph0 qo qo).trans_le ol
   · suffices (succ (typein LT.lt (g p))).card < ⟦α⟧ from (IH _ this qo).trans_lt this
     rw [← lt_ord]
-    apply (ord_isLimit ol).2
+    apply (isLimit_ord ol).2
     rw [mk'_def, e]
     apply typein_lt_type
 
diff --git a/Mathlib/SetTheory/Cardinal/Cofinality.lean b/Mathlib/SetTheory/Cardinal/Cofinality.lean
index 5f1d484af9be7..cbf48de84b877 100644
--- a/Mathlib/SetTheory/Cardinal/Cofinality.lean
+++ b/Mathlib/SetTheory/Cardinal/Cofinality.lean
@@ -681,7 +681,7 @@ theorem aleph_cof {o : Ordinal} (ho : o.IsLimit) : (aleph o).ord.cof = o.cof :=
 
 @[simp]
 theorem cof_omega0 : cof ω = ℵ₀ :=
-  (aleph0_le_cof.2 omega0_isLimit).antisymm' <| by
+  (aleph0_le_cof.2 isLimit_omega0).antisymm' <| by
     rw [← card_omega0]
     apply cof_le_card
 
@@ -862,7 +862,7 @@ theorem mk_bounded_subset {α : Type*} (h : ∀ x < #α, (2^x) < #α) {r : α 
   · refine @mk_le_of_injective α _ (fun x => Subtype.mk {x} ?_) ?_
     · apply bounded_singleton
       rw [← hr]
-      apply ord_isLimit ha
+      apply isLimit_ord ha
     · intro a b hab
       simpa [singleton_eq_singleton_iff] using hab
 
@@ -881,7 +881,7 @@ theorem mk_subset_mk_lt_cof {α : Type*} (h : ∀ x < #α, (2^x) < #α) :
     exact lt_cof_type hs
   · refine @mk_le_of_injective α _ (fun x => Subtype.mk {x} ?_) ?_
     · rw [mk_singleton]
-      exact one_lt_aleph0.trans_le (aleph0_le_cof.2 (ord_isLimit h'.aleph0_le))
+      exact one_lt_aleph0.trans_le (aleph0_le_cof.2 (isLimit_ord h'.aleph0_le))
     · intro a b hab
       simpa [singleton_eq_singleton_iff] using hab
 
@@ -917,7 +917,7 @@ theorem isRegular_succ {c : Cardinal.{u}} (h : ℵ₀ ≤ c) : IsRegular (succ c
       (by
         cases' Quotient.exists_rep (@succ Cardinal _ _ c) with α αe; simp only [mk'_def] at αe
         rcases ord_eq α with ⟨r, wo, re⟩
-        have := ord_isLimit (h.trans (le_succ _))
+        have := isLimit_ord (h.trans (le_succ _))
         rw [← αe, re] at this ⊢
         rcases cof_eq' r this with ⟨S, H, Se⟩
         rw [← Se]
@@ -1123,7 +1123,7 @@ theorem derivFamily_lt_ord_lift {ι} {f : ι → Ordinal → Ordinal} {c} (hc :
     rw [derivFamily_succ]
     exact
       nfpFamily_lt_ord_lift hω (by rwa [hc.cof_eq]) hf
-        ((ord_isLimit hc.1).2 _ (hb ((lt_succ b).trans hb')))
+        ((isLimit_ord hc.1).2 _ (hb ((lt_succ b).trans hb')))
   | H₃ b hb H =>
     intro hb'
     rw [derivFamily_limit f hb]
@@ -1170,7 +1170,7 @@ theorem univ_inaccessible : IsInaccessible univ.{u, v} :=
 theorem lt_power_cof {c : Cardinal.{u}} : ℵ₀ ≤ c → c < (c^cof c.ord) :=
   Quotient.inductionOn c fun α h => by
     rcases ord_eq α with ⟨r, wo, re⟩
-    have := ord_isLimit h
+    have := isLimit_ord h
     rw [mk'_def, re] at this ⊢
     rcases cof_eq' r this with ⟨S, H, Se⟩
     have := sum_lt_prod (fun a : S => #{ x // r x a }) (fun _ => #α) fun i => ?_
diff --git a/Mathlib/SetTheory/Ordinal/Arithmetic.lean b/Mathlib/SetTheory/Ordinal/Arithmetic.lean
index d8239b6b16acc..90d58666720d4 100644
--- a/Mathlib/SetTheory/Ordinal/Arithmetic.lean
+++ b/Mathlib/SetTheory/Ordinal/Arithmetic.lean
@@ -2263,13 +2263,16 @@ theorem one_lt_omega0 : 1 < ω := by simpa only [Nat.cast_one] using nat_lt_omeg
 @[deprecated (since := "2024-09-30")]
 alias one_lt_omega := one_lt_omega0
 
-theorem omega0_isLimit : IsLimit ω :=
+theorem isLimit_omega0 : 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-10-14")]
+alias omega0_isLimit := isLimit_omega0
+
 @[deprecated (since := "2024-09-30")]
-alias omega_isLimit := omega0_isLimit
+alias omega_isLimit := isLimit_omega0
 
 theorem omega0_le {o : Ordinal} : ω ≤ o ↔ ∀ n : ℕ, ↑n ≤ o :=
   ⟨fun h n => (nat_lt_omega0 _).le.trans h, fun H =>
@@ -2306,14 +2309,14 @@ theorem isLimit_iff_omega0_dvd {a : Ordinal} : IsLimit a ↔ a ≠ 0 ∧ ω ∣
   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 omega0_ne_zero, ← succ_le_iff, le_div omega0_ne_zero, mul_succ,
-      add_le_of_limit omega0_isLimit]
+      add_le_of_limit isLimit_omega0]
     intro b hb
     rcases lt_omega0.1 hb with ⟨n, rfl⟩
     exact
       (add_le_add_right (mul_div_le _ _) _).trans
         (lt_sub.1 <| nat_lt_limit (isLimit_sub l hx) _).le
   · rcases h with ⟨a0, b, rfl⟩
-    refine isLimit_mul_left omega0_isLimit (Ordinal.pos_iff_ne_zero.2 <| mt ?_ a0)
+    refine isLimit_mul_left isLimit_omega0 (Ordinal.pos_iff_ne_zero.2 <| mt ?_ a0)
     intro e
     simp only [e, mul_zero]
 
@@ -2394,7 +2397,7 @@ namespace Cardinal
 
 open Ordinal
 
-theorem ord_isLimit {c} (co : ℵ₀ ≤ c) : (ord c).IsLimit := by
+theorem isLimit_ord {c} (co : ℵ₀ ≤ c) : (ord c).IsLimit := by
   refine ⟨fun h => aleph0_ne_zero ?_, fun a => lt_imp_lt_of_le_imp_le fun h => ?_⟩
   · rw [← Ordinal.le_zero, ord_le] at h
     simpa only [card_zero, nonpos_iff_eq_zero] using co.trans h
@@ -2403,10 +2406,13 @@ 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 Ordinal.omega0_isLimit
+      exact Ordinal.isLimit_omega0
+
+@[deprecated (since := "2024-10-14")]
+alias ord_isLimit := isLimit_ord
 
 theorem noMaxOrder {c} (h : ℵ₀ ≤ c) : NoMaxOrder c.ord.toType :=
-  toType_noMax_of_succ_lt (ord_isLimit h).2
+  toType_noMax_of_succ_lt (isLimit_ord h).2
 
 end Cardinal
 
diff --git a/Mathlib/SetTheory/Ordinal/Notation.lean b/Mathlib/SetTheory/Ordinal/Notation.lean
index 9df8635093a8b..050c6b4f8f653 100644
--- a/Mathlib/SetTheory/Ordinal/Notation.lean
+++ b/Mathlib/SetTheory/Ordinal/Notation.lean
@@ -577,7 +577,7 @@ 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 (isLimit_opow_left omega0_isLimit this), mul_assoc,
+      rw [add_mul_limit ao (isLimit_opow_left isLimit_omega0 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)
 
@@ -790,7 +790,7 @@ theorem repr_opow_aux₁ {e a} [Ne : NF e] [Na : NF a] {a' : Ordinal} (e0 : repr
   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 _ omega0_pos).trans_le this).ne' omega0_isLimit).2
+  apply (opow_le_of_limit ((opow_pos _ omega0_pos).trans_le this).ne' isLimit_omega0).2
   intro b l
   have := (No.below_of_lt (lt_succ _)).repr_lt
   rw [repr] at this
@@ -801,8 +801,8 @@ theorem repr_opow_aux₁ {e a} [Ne : NF e] [Na : NF a] {a' : Ordinal} (e0 : repr
   · apply (mul_le_mul_left' (le_succ b) _).trans
     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 omega0_isLimit.2 _ l
-  · apply (principal_mul_omega0 (omega0_isLimit.2 _ h) l).le.trans
+    exact isLimit_omega0.2 _ l
+  · apply (principal_mul_omega0 (isLimit_omega0.2 _ h) l).le.trans
     simpa using mul_le_mul_right' (one_le_iff_ne_zero.2 e0) ω
 
 section
@@ -966,7 +966,7 @@ private theorem exists_lt_add {α} [hα : Nonempty α] {o : Ordinal} {f : α →
 
 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 omega0_isLimit).1 h
+  obtain ⟨i, hi, h'⟩ := (lt_mul_of_limit isLimit_omega0).1 h
   obtain ⟨i, rfl⟩ := lt_omega0.1 hi
   exact ⟨i, h'.trans_le (le_add_right _ _)⟩
 
@@ -1025,13 +1025,13 @@ theorem fundamentalSequence_has_prop (o) : FundamentalSequenceProp o (fundamenta
     · exact ⟨rfl, inferInstance⟩
     · have := opow_pos (repr a') omega0_pos
       refine
-        ⟨isLimit_mul this omega0_isLimit, fun i =>
+        ⟨isLimit_mul this isLimit_omega0, 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_omega0
     · have := opow_pos (repr a') omega0_pos
       refine
-        ⟨isLimit_add _ (isLimit_mul this omega0_isLimit), fun i => ⟨this, ?_, ?_⟩,
+        ⟨isLimit_add _ (isLimit_mul this isLimit_omega0), 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_omega0
diff --git a/Mathlib/SetTheory/Ordinal/Principal.lean b/Mathlib/SetTheory/Ordinal/Principal.lean
index d58c0eff2dd35..5e32abd578e7d 100644
--- a/Mathlib/SetTheory/Ordinal/Principal.lean
+++ b/Mathlib/SetTheory/Ordinal/Principal.lean
@@ -194,7 +194,7 @@ theorem add_omega0_opow {a b : Ordinal} (h : a < ω ^ b) : a + ω ^ b = ω ^ b :
   · 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 omega0_isLimit).1 h with ⟨x, xo, ax⟩
+    rcases (lt_mul_of_limit isLimit_omega0).1 h with ⟨x, xo, ax⟩
     apply (add_le_add_right ax.le _).trans
     rw [opow_succ, ← mul_add, add_omega0 xo]
   · rcases (lt_opow_of_limit omega0_ne_zero l).1 h with ⟨x, xb, ax⟩
@@ -228,7 +228,7 @@ theorem principal_add_iff_zero_or_omega0_opow {o : Ordinal} :
         fun ⟨b, e⟩ => e.symm ▸ fun a => add_omega0_opow⟩
     have := H _ h
     have := lt_opow_succ_log_self one_lt_omega0 o
-    rw [opow_succ, lt_mul_of_limit omega0_isLimit] at this
+    rw [opow_succ, lt_mul_of_limit isLimit_omega0] at this
     rcases this with ⟨a, ao, h'⟩
     rcases lt_omega0.1 ao with ⟨n, rfl⟩
     clear ao
@@ -347,7 +347,7 @@ theorem mul_lt_omega0_opow {a b c : Ordinal} (c0 : 0 < c) (ha : a < ω ^ c) (hb
   · exact (lt_irrefl _).elim c0
   · rw [opow_succ] at ha
     obtain ⟨n, hn, an⟩ :=
-      ((isNormal_mul_right <| opow_pos _ omega0_pos).limit_lt omega0_isLimit).1 ha
+      ((isNormal_mul_right <| opow_pos _ omega0_pos).limit_lt isLimit_omega0).1 ha
     apply (mul_le_mul_right' (le_of_lt an) _).trans_lt
     rw [opow_succ, mul_assoc, mul_lt_mul_iff_left (opow_pos _ omega0_pos)]
     exact principal_mul_omega0 hn hb
@@ -366,7 +366,7 @@ theorem mul_omega0_opow_opow {a b : Ordinal} (a0 : 0 < a) (h : a < ω ^ ω ^ b)
     exact mul_omega0 a0 h
   · apply le_antisymm
     · obtain ⟨x, xb, ax⟩ :=
-        (lt_opow_of_limit omega0_ne_zero (isLimit_opow_left omega0_isLimit b0)).1 h
+        (lt_opow_of_limit omega0_ne_zero (isLimit_opow_left isLimit_omega0 b0)).1 h
       apply (mul_le_mul_right' (le_of_lt ax) _).trans
       rw [← opow_add, add_omega0_opow xb]
     · conv_lhs => rw [← one_mul (ω ^ _)]
@@ -442,7 +442,7 @@ theorem principal_opow_omega0 : Principal (· ^ ·) ω := fun a b ha hb =>
 alias principal_opow_omega := principal_opow_omega0
 
 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 =>
+  ((opow_le_of_limit (one_le_iff_ne_zero.1 <| le_of_lt a1) isLimit_omega0).2 fun _ hb =>
       (principal_opow_omega0 h hb).le).antisymm
   (right_le_opow _ a1)