add

Author: vihdzp

Mathlib/SetTheory/Cardinal/Cofinality/Basic.lean

@@ -48,6 +48,7 @@ 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
+/-- Every well-order has a cofinal subset of cardinal `cof α`. -/
 theorem 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⟩
@@ -131,6 +132,9 @@ theorem cof_congr_of_strictMono {f : α → γ} (hf : StrictMono f) (hf' : IsCof
     cof α = cof γ := by
   simpa using lift_cof_congr_of_strictMono hf hf'
 
+theorem cof_eq_of_isCofinal {s : Set α} (hs : IsCofinal s) : cof s = cof α :=
+  cof_congr_of_strictMono (Subtype.strictMono_coe _) (by simpa)
+
 @[simp]
 theorem cof_lt_aleph0_iff : Order.cof α < ℵ₀ ↔ Order.cof α ≤ 1 := by
   refine ⟨fun h ↦ ?_, (lt_of_le_of_lt · one_lt_aleph0)⟩

Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean

@@ -151,7 +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 α] :
+variable (α) in
+/-- Every well-order has a cofinal subset of order type `(cof α).ord`. -/
+theorem ord_cof_eq [LinearOrder α] [WellFoundedLT α] :
     ∃ s : Set α, IsCofinal s ∧ typeLT s = (Order.cof α).ord := by
   obtain ⟨s, hs, hs'⟩ := Order.cof_eq α
   obtain ⟨r, hr, hr'⟩ := exists_ord_eq s
@@ -166,16 +168,21 @@ theorem ord_cof_eq (α : Type*) [LinearOrder α] [WellFoundedLT α] :
     · obtain ⟨x, z, hz, rfl⟩ := x
       exact (hz _ hxy').asymm hxy
 
+/-- Every cofinal set has a cofinal subset of order type `(cof α).ord`. -/
+theorem ord_cof_eq_of_isCofinal [LinearOrder α] [WellFoundedLT α] {s : Set α} (hs : IsCofinal s) :
+    ∃ t ⊆ s, IsCofinal t ∧ typeLT t = (Order.cof α).ord := by
+  obtain ⟨t, ht, ht'⟩ := ord_cof_eq s
+  rw [cof_eq_of_isCofinal hs] at ht'
+  refine ⟨t, ?_, hs.trans ht, ?_⟩
+  · simp
+  · rw [← ht']
+    exact ((Subtype.strictMono_coe _).strictMonoOn _).orderIso.ordinal_type_eq.symm
+
 @[simp]
 theorem _root_.Order.cof_ord_cof (α : Type*) [LinearOrder α] [WellFoundedLT α] :
     (Order.cof α).ord.cof = Order.cof α := by
   obtain ⟨s, hs, hs'⟩ := ord_cof_eq α
-  rw [← hs', cof_type]
-  apply le_antisymm
-  · rw [← card_ord (Order.cof α), ← hs', card_type]
-    exact cof_le_cardinalMk s
-  · rw [le_cof_iff]
-    exact fun t ht ↦ (cof_le (hs.trans ht)).trans_eq (mk_image_eq Subtype.val_injective)
+  rw [← hs', cof_type, cof_eq_of_isCofinal hs]
 
 @[simp]
 theorem cof_ord_cof (o : Ordinal) : o.cof.ord.cof = o.cof := by

Mathlib/SetTheory/Ordinal/Basic.lean

@@ -169,6 +169,10 @@ theorem _root_.RelIso.ordinal_type_eq {α β} {r : α → α → Prop} {s : β 
     [IsWellOrder β s] (h : r ≃r s) : type r = type s :=
   type_eq.2 ⟨h⟩
 
+theorem _root_.OrderIso.ordinal_type_eq {α β} [LinearOrder α] [LinearOrder β]
+    [WellFoundedLT α] [WellFoundedLT β] (h : α ≃o β) : typeLT α = typeLT β :=
+  h.toRelIsoLT.ordinal_type_eq
+
 theorem type_eq_zero_of_empty (r) [IsWellOrder α r] [IsEmpty α] : type r = 0 :=
   (RelIso.relIsoOfIsEmpty r _).ordinal_type_eq