refactor: rename Cardinal.ord_eq → Cardinal.exists_ord_eq (#37330)

As suggested in #36928.

Author: vihdzp

Counterexamples/Phillips.lean

@@ -460,7 +460,7 @@ We need the continuum hypothesis to construct it.
 
 theorem sierpinski_pathological_family (Hcont : #ℝ = ℵ₁) :
     ∃ f : ℝ → Set ℝ, (∀ x, (univ \ f x).Countable) ∧ ∀ y, {x : ℝ | y ∈ f x}.Countable := by
-  rcases Cardinal.ord_eq ℝ with ⟨r, hr, H⟩
+  rcases Cardinal.exists_ord_eq ℝ with ⟨r, hr, H⟩
   refine ⟨fun x => {y | r x y}, fun x => ?_, fun y => ?_⟩
   · have : univ \ {y | r x y} = {y | r y x} ∪ {x} := by
       ext y

Mathlib/SetTheory/Cardinal/Arithmetic.lean

@@ -46,7 +46,7 @@ theorem mul_eq_self {c : Cardinal} (h : ℵ₀ ≤ c) : c * c = c := by
   -- the only nontrivial part is `c * c ≤ c`. We prove it inductively.
   refine Acc.recOn (Cardinal.lt_wf.apply c) (fun c _ => Cardinal.inductionOn c fun α IH ol => ?_) h
   -- consider the minimal well-order `r` on `α` (a type with cardinality `c`).
-  rcases ord_eq α with ⟨r, wo, e⟩
+  rcases exists_ord_eq α with ⟨r, wo, e⟩
   classical
   letI := linearOrderOfSTO r
   -- Define an order `s` on `α × α` by writing `(a, b) < (c, d)` if `max a b < max c d`, or

Mathlib/SetTheory/Cardinal/Cofinality.lean

@@ -337,7 +337,7 @@ theorem cof_omega0 : cof ω = ℵ₀ :=
 theorem ord_cof_eq (α : Type*) [LinearOrder α] [WellFoundedLT α] :
     ∃ s : Set α, IsCofinal s ∧ typeLT s = (Order.cof α).ord := by
   obtain ⟨s, hs, hs'⟩ := Order.cof_eq α
-  obtain ⟨r, hr, hr'⟩ := ord_eq s
+  obtain ⟨r, hr, hr'⟩ := exists_ord_eq s
   have ht := hs.trans (isCofinal_setOf_imp_lt r)
   refine ⟨_, ht, (ord_le.2 (cof_le ht)).antisymm' ?_⟩
   rw [← hs', hr', type_le_iff']
@@ -636,7 +636,7 @@ theorem nfp_lt_ord {f : Ordinal → Ordinal} {c} (hc : ℵ₀ < cof c) (hf : ∀
 theorem exists_blsub_cof (o : Ordinal) :
     ∃ f : ∀ a < (cof o).ord, Ordinal, blsub.{u, u} _ f = o := by
   rcases exists_lsub_cof o with ⟨ι, f, hf, hι⟩
-  rcases Cardinal.ord_eq ι with ⟨r, hr, hι'⟩
+  rcases Cardinal.exists_ord_eq ι with ⟨r, hr, hι'⟩
   rw [← @blsub_eq_lsub' ι r hr] at hf
   rw [← hι, hι']
   exact ⟨_, hf⟩
@@ -645,7 +645,7 @@ theorem le_cof_iff_blsub {b : Ordinal} {a : Cardinal} :
     a ≤ cof b ↔ ∀ {o} (f : ∀ a < o, Ordinal), blsub.{u, u} o f = b → a ≤ o.card :=
   le_cof_iff_lsub.trans
     ⟨fun H o f hf => by simpa using H _ hf, fun H ι f hf => by
-      rcases Cardinal.ord_eq ι with ⟨r, hr, hι'⟩
+      rcases Cardinal.exists_ord_eq ι with ⟨r, hr, hι'⟩
       rw [← @blsub_eq_lsub' ι r hr] at hf
       simpa using H _ hf⟩
 
@@ -762,7 +762,7 @@ theorem mk_subset_mk_lt_cof {α : Type*} (h : ∀ x < #α, 2 ^ x < #α) :
   rcases eq_or_ne #α 0 with (ha | ha)
   · simp [ha]
   have h' : IsStrongLimit #α := ⟨ha, @h⟩
-  rcases ord_eq α with ⟨r, wo, hr⟩
+  rcases exists_ord_eq α with ⟨r, wo, hr⟩
   classical
   letI := linearOrderOfSTO r
   apply le_antisymm
@@ -790,7 +790,7 @@ alias unbounded_of_unbounded_iUnion := isCofinal_of_isCofinal_iUnion
 
 theorem lt_power_cof {c : Cardinal.{u}} : ℵ₀ ≤ c → c < c ^ c.ord.cof :=
   Cardinal.inductionOn c fun α h => by
-    rcases ord_eq α with ⟨r, wo, re⟩
+    rcases exists_ord_eq α with ⟨r, wo, re⟩
     have := isSuccLimit_ord h
     rw [re] at this ⊢
     rcases cof_eq' r this with ⟨S, H, Se⟩

Mathlib/SetTheory/Cardinal/Regular.lean

@@ -82,7 +82,7 @@ theorem isRegular_succ {c : Cardinal.{u}} (h : ℵ₀ ≤ c) : IsRegular (succ c
       (by
         have αe := Cardinal.mk_out (succ c)
         set α := (succ c).out
-        rcases ord_eq α with ⟨r, wo, re⟩
+        rcases exists_ord_eq α with ⟨r, wo, re⟩
         have := isSuccLimit_ord (h.trans (le_succ _))
         rw [← αe, re] at this ⊢
         rcases cof_eq' r this with ⟨S, H, Se⟩

Mathlib/SetTheory/Ordinal/Basic.lean

@@ -1101,14 +1101,16 @@ theorem ord_eq_iInf (α : Type u) : ord #α = ⨅ r : { r // IsWellOrder α r },
 @[deprecated (since := "2026-03-15")] alias ord_eq_Inf := ord_eq_iInf
 
 /-- There exists a well-order on `α` whose order type is exactly `ord #α`. -/
-theorem ord_eq (α) : ∃ (r : α → α → Prop) (_ : IsWellOrder α r), ord #α = type r :=
+theorem exists_ord_eq (α) : ∃ (r : α → α → Prop) (_ : IsWellOrder α r), ord #α = type r :=
   let ⟨r, wo⟩ := ciInf_mem fun r : { r // IsWellOrder α r } => @type α r.1 r.2
   ⟨r.1, r.2, wo.symm⟩
 
+@[deprecated (since := "2026-03-29")] alias ord_eq := exists_ord_eq
+
 open Classical in
 /-- There exists a well-order on `α` whose order type is exactly `ord #α`. -/
 theorem exists_ord_eq_type_lt (α) : ∃ (_ : LinearOrder α) (_: WellFoundedLT α), ord #α = typeLT α :=
-  let ⟨r, _, hr⟩ := ord_eq α
+  let ⟨r, _, hr⟩ := exists_ord_eq α
   let := linearOrderOfSTO r
   ⟨this, inferInstance, hr⟩
 
@@ -1117,7 +1119,7 @@ theorem ord_le_type (r : α → α → Prop) [h : IsWellOrder α r] : ord #α 
 
 theorem ord_le {c o} : ord c ≤ o ↔ c ≤ o.card := by
   refine c.inductionOn fun α ↦ o.inductionOn fun β s _ ↦ ?_
-  let ⟨r, _, e⟩ := ord_eq α
+  let ⟨r, _, e⟩ := exists_ord_eq α
   constructor <;> intro h
   · rw [e] at h
     exact card_le_card h
@@ -1133,7 +1135,7 @@ theorem lt_ord {c o} : o < ord c ↔ o.card < c :=
 
 @[simp]
 theorem card_ord (c) : (ord c).card = c :=
-  c.inductionOn fun α ↦ let ⟨r, _, e⟩ := ord_eq α; e ▸ card_type r
+  c.inductionOn fun α ↦ let ⟨r, _, e⟩ := exists_ord_eq α; e ▸ card_type r
 
 theorem card_surjective : Function.Surjective card :=
   fun c ↦ ⟨_, card_ord c⟩