chore: rename Order.cof_eq → Order.exists_cof_eq (leanprover-community#39851)

Author: vihdzp

Mathlib/SetTheory/Cardinal/Cofinality/Basic.lean

@@ -48,17 +48,19 @@ theorem le_cof_iff {c : Cardinal} : c ≤ cof α ↔ ∀ s : Set α, IsCofinal s
 @[deprecated (since := "2026-02-18")] alias le_cof := le_cof_iff
 
 variable (α) in
-theorem cof_eq : ∃ s : Set α, IsCofinal s ∧ #s = cof α := by
+theorem exists_cof_eq : ∃ s : Set α, IsCofinal s ∧ #s = cof α := by
   obtain ⟨s, hs⟩ := ciInf_mem fun s : {s : Set α // IsCofinal s} ↦ #s
   exact ⟨s.1, s.2, hs⟩
 
+@[deprecated (since := "2026-05-25")] alias cof_eq := exists_cof_eq
+
 variable (α) in
 theorem cof_le_cardinalMk : cof α ≤ #α :=
   cof_le .univ |>.trans_eq mk_univ
 
 theorem cof_eq_zero_iff : cof α = 0 ↔ IsEmpty α := by
   refine ⟨fun _ ↦ ?_, fun _ ↦ by simp [cof]⟩
-  obtain ⟨s, hs, hs'⟩ := cof_eq α
+  obtain ⟨s, hs, hs'⟩ := exists_cof_eq α
   simp_all [mk_eq_zero_iff, isCofinal_empty_iff]
 
 @[simp]
@@ -74,7 +76,7 @@ theorem cof_ne_zero [h : Nonempty α] : cof α ≠ 0 :=
 
 theorem cof_eq_one_iff : cof α = 1 ↔ ∃ x : α, IsTop x := by
   refine ⟨fun h ↦ ?_, fun ⟨t, ht⟩ ↦ ?_⟩
-  · obtain ⟨s, hs, hs'⟩ := cof_eq α
+  · obtain ⟨s, hs, hs'⟩ := exists_cof_eq α
     rw [h, mk_set_eq_one_iff] at hs'
     obtain ⟨t, rfl⟩ := hs'
     use t
@@ -132,9 +134,9 @@ theorem cof_congr_of_strictMono {f : α → γ} (hf : StrictMono f) (hf' : IsCof
   simpa using lift_cof_congr_of_strictMono hf hf'
 
 @[simp]
-theorem cof_lt_aleph0_iff : Order.cof α < ℵ₀ ↔ Order.cof α ≤ 1 := by
+theorem cof_lt_aleph0_iff : cof α < ℵ₀ ↔ cof α ≤ 1 := by
   refine ⟨fun h ↦ ?_, (lt_of_le_of_lt · one_lt_aleph0)⟩
-  obtain ⟨s, hs, hs'⟩ := Order.cof_eq α
+  obtain ⟨s, hs, hs'⟩ := exists_cof_eq α
   have hf : s.Finite := by
     rw [Set.Finite, ← mk_lt_aleph0_iff]
     exact hs'.trans_lt h
@@ -143,7 +145,7 @@ theorem cof_lt_aleph0_iff : Order.cof α < ℵ₀ ↔ Order.cof α ≤ 1 := by
   simpa
 
 @[simp]
-theorem aleph0_le_cof_iff : ℵ₀ ≤ Order.cof α ↔ 1 < Order.cof α := by
+theorem aleph0_le_cof_iff : ℵ₀ ≤ cof α ↔ 1 < cof α := by
   simp [← not_lt]
 
 theorem aleph0_le_cof [Nonempty α] [NoMaxOrder α] : ℵ₀ ≤ cof α := by

Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean

@@ -151,9 +151,9 @@ theorem cof_omega0 : cof ω = ℵ₀ :=
 
 @[deprecated (since := "2026-02-18")] alias cof_eq_one_iff_is_succ := cof_eq_one_iff
 
-theorem ord_cof_eq (α : Type*) [LinearOrder α] [WellFoundedLT α] :
+theorem exists_ord_cof_eq (α : Type*) [LinearOrder α] [WellFoundedLT α] :
     ∃ s : Set α, IsCofinal s ∧ typeLT s = (Order.cof α).ord := by
-  obtain ⟨s, hs, hs'⟩ := Order.cof_eq α
+  obtain ⟨s, hs, hs'⟩ := exists_cof_eq α
   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' ?_⟩
@@ -166,10 +166,12 @@ theorem ord_cof_eq (α : Type*) [LinearOrder α] [WellFoundedLT α] :
     · obtain ⟨x, z, hz, rfl⟩ := x
       exact (hz _ hxy').asymm hxy
 
+@[deprecated (since := "2026-05-25")] alias ord_cof_eq := exists_ord_cof_eq
+
 @[simp]
 theorem _root_.Order.cof_ord_cof (α : Type*) [LinearOrder α] [WellFoundedLT α] :
     (Order.cof α).ord.cof = Order.cof α := by
-  obtain ⟨s, hs, hs'⟩ := ord_cof_eq α
+  obtain ⟨s, hs, hs'⟩ := exists_ord_cof_eq α
   rw [← hs', cof_type]
   apply le_antisymm
   · rw [← card_ord (Order.cof α), ← hs', card_type]
@@ -547,7 +549,7 @@ theorem cof_eq' (r : α → α → Prop) [H : IsWellOrder α r] (h : IsSuccLimit
   let := linearOrderOfSTO r
   have : WellFoundedLT α := H.toIsWellFounded
   have : NoMaxOrder α := isSuccPrelimit_type_lt_iff.1 h.isSuccPrelimit
-  obtain ⟨s, hs, hs'⟩ := Order.cof_eq α
+  obtain ⟨s, hs, hs'⟩ := exists_cof_eq α
   refine ⟨s, ?_, hs'⟩
   rwa [← not_bddAbove_iff_isCofinal, not_bddAbove_iff] at hs
 
@@ -631,7 +633,7 @@ theorem lt_power_cof_ord {c : Cardinal} (hc : ℵ₀ ≤ c) : c < c ^ c.ord.cof
   have : NoMaxOrder α := by
     rw [← isSuccPrelimit_type_lt_iff, ← hα]
     exact (isSuccLimit_ord hc).isSuccPrelimit
-  obtain ⟨s, hs, hs'⟩ := ord_cof_eq α
+  obtain ⟨s, hs, hs'⟩ := exists_ord_cof_eq α
   rw [hα, cof_type, ← card_ord (Order.cof _), ← hs', card_type, ← prod_const']
   refine (mk_iUnion_le_sum_mk.trans' ?_).trans_lt (sum_lt_prod _ _ fun i ↦ mk_Iio_lt i.1 hα)
   rw [← mk_univ, ← isCofinal_iff_iUnion_Iio_eq_univ.1 hs, iUnion_coe_set]

Mathlib/SetTheory/Ordinal/FundamentalSequence.lean

@@ -111,7 +111,7 @@ end IsFundamentalSeq
 /-- Every ordinal has a fundamental sequence. -/
 theorem exists_isFundamentalSeq (ha : o.cof.ord = a) : ∃ f : Iio a → Iio o, IsFundamentalSeq f := by
   subst ha
-  obtain ⟨s, hs, hs'⟩ := ord_cof_eq o.ToType
+  obtain ⟨s, hs, hs'⟩ := exists_ord_cof_eq o.ToType
   rw [cof_toType] at hs'
   let g := (OrderIso.setCongr _ _ (congrArg _ hs'.symm)).trans <|
     .ofRelIsoLT (enum (α := s) (· < ·))