chore: rename Ordinal.cof_cof → Ordinal.cof_ord_cof (#36975)

As suggested by Yaël in #36702.

Author: vihdzp

Mathlib/SetTheory/Cardinal/Cofinality.lean

@@ -378,9 +378,11 @@ theorem _root_.Order.cof_ord_cof (α : Type*) [LinearOrder α] [WellFoundedLT α
     exact fun t ht ↦ (cof_le (hs.trans ht)).trans_eq (mk_image_eq Subtype.val_injective)
 
 @[simp]
-theorem cof_cof (o : Ordinal) : o.cof.ord.cof = o.cof := by
+theorem cof_ord_cof (o : Ordinal) : o.cof.ord.cof = o.cof := by
   simpa using Order.cof_ord_cof o.ToType
 
+@[deprecated (since := "2026-03-21")] alias cof_cof := cof_ord_cof
+
 /-! ### Cofinality of suprema and least strict upper bounds -/
 
 -- TODO: use `⨆ i, succ (f i)` instead of `lsub`

Mathlib/SetTheory/Cardinal/Regular.lean

@@ -61,7 +61,7 @@ theorem IsRegular.ord_pos {c : Cardinal} (H : c.IsRegular) : 0 < c.ord := by
   exact H.pos
 
 theorem isRegular_cof {o : Ordinal} (h : IsSuccLimit o) : IsRegular o.cof := by
-  refine ⟨?_, (cof_cof o).ge⟩
+  refine ⟨?_, (cof_ord_cof o).ge⟩
   rwa [aleph0_le_cof_iff, one_lt_cof_iff]
 
 /-- If `c` is a regular cardinal, then `c.ord.ToType` has a least element. -/