From 540ebc6df9395914656dcfc0462523919fdc1d83 Mon Sep 17 00:00:00 2001
From: vihdzp <vi.hdz.p@gmail.com>
Date: Fri, 22 May 2026 11:24:15 -0600
Subject: [PATCH 01/12] cofwithin

---
 Mathlib/SetTheory/Cardinal/Basic.lean         |  8 ++
 .../SetTheory/Cardinal/Cofinality/Basic.lean  | 99 +++++++++++++++++--
 .../Cardinal/Cofinality/Ordinal.lean          | 15 +--
 3 files changed, 105 insertions(+), 17 deletions(-)

diff --git a/Mathlib/SetTheory/Cardinal/Basic.lean b/Mathlib/SetTheory/Cardinal/Basic.lean
index b45d98e570313b..d65e9f9ba1d508 100644
--- a/Mathlib/SetTheory/Cardinal/Basic.lean
+++ b/Mathlib/SetTheory/Cardinal/Basic.lean
@@ -942,6 +942,14 @@ theorem mk_preimage_of_subset_range (f : α → β) (s : Set β) (h : s ⊆ rang
   rw [← lift_id #(↑(f ⁻¹' s)), ← lift_id #(↑s)]
   exact mk_preimage_of_subset_range_lift f s h
 
+open Set.Notation in
+theorem mk_preimage_val_le_right (s t : Set α) : #(s ↓∩ t) ≤ #t :=
+  mk_preimage_of_injective _ _ Subtype.val_injective
+
+open Set.Notation in
+theorem mk_preimage_val_le_left (s t : Set α) : #(s ↓∩ t) ≤ #s :=
+  mk_set_le _
+
 theorem mk_subset_ge_of_subset_image_lift {α : Type u} {β : Type v} (f : α → β) {s : Set α}
     {t : Set β} (h : t ⊆ f '' s) : lift.{u} #t ≤ lift.{v} #({ x ∈ s | f x ∈ t } : Set α) := by
   rw [image_eq_range] at h
diff --git a/Mathlib/SetTheory/Cardinal/Cofinality/Basic.lean b/Mathlib/SetTheory/Cardinal/Cofinality/Basic.lean
index ff288badfea0f4..62b239350df651 100644
--- a/Mathlib/SetTheory/Cardinal/Cofinality/Basic.lean
+++ b/Mathlib/SetTheory/Cardinal/Cofinality/Basic.lean
@@ -8,6 +8,8 @@ module
 public import Mathlib.Order.Cofinal
 public import Mathlib.SetTheory.Cardinal.Basic
 
+import Mathlib.Order.LatticeIntervals
+
 /-!
 # Cofinality of an order
 
@@ -17,7 +19,7 @@ cardinality of a cofinal subset.
 
 public noncomputable section
 
-open Function Cardinal Set Order
+open Function Cardinal Set Set.Notation Order
 
 universe u v w
 
@@ -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'⟩ := 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
@@ -162,21 +164,21 @@ section Congr
 variable [Preorder α] [Preorder β] [Preorder γ]
 
 theorem GaloisConnection.cof_le_lift {f : β → α} {g : α → β} (h : GaloisConnection f g) :
-    Cardinal.lift.{u} (Order.cof β) ≤ Cardinal.lift.{v} (Order.cof α) := by
+    Cardinal.lift.{u} (cof β) ≤ Cardinal.lift.{v} (cof α) := by
   rw [le_lift_cof_iff]
   exact fun s hs ↦ (lift_le.2 <| cof_le (h.map_isCofinal hs)).trans mk_image_le_lift
 
 theorem GaloisConnection.cof_le {f : γ → α} {g : α → γ} (h : GaloisConnection f g) :
-    Order.cof γ ≤ Order.cof α := by
+    cof γ ≤ cof α := by
   simpa using h.cof_le_lift
 
 theorem OrderIso.lift_cof_congr (f : α ≃o β) :
-    Cardinal.lift.{v} (Order.cof α) = Cardinal.lift.{u} (Order.cof β) :=
+    Cardinal.lift.{v} (cof α) = Cardinal.lift.{u} (cof β) :=
   f.to_galoisConnection.cof_le_lift.antisymm (f.symm.to_galoisConnection.cof_le_lift)
 
 @[deprecated (since := "2026-03-20")] alias OrderIso.lift_cof_eq := OrderIso.lift_cof_congr
 
-theorem OrderIso.cof_congr (f : α ≃o γ) : Order.cof α = Order.cof γ := by
+theorem OrderIso.cof_congr (f : α ≃o γ) : cof α = cof γ := by
   simpa using f.lift_cof_congr
 
 @[deprecated (since := "2026-03-20")] alias OrderIso.cof_eq := OrderIso.cof_congr
@@ -189,7 +191,7 @@ end Congr
 /-- If the union of `s` is cofinal and `s` is smaller than the cofinality, then `s` has a cofinal
 member. -/
 theorem isCofinal_of_isCofinal_sUnion {α : Type*} [LinearOrder α] {s : Set (Set α)}
-    (h₁ : IsCofinal (⋃₀ s)) (h₂ : #s < Order.cof α) : ∃ x ∈ s, IsCofinal x := by
+    (h₁ : IsCofinal (⋃₀ s)) (h₂ : #s < cof α) : ∃ x ∈ s, IsCofinal x := by
   contrapose! h₂
   simp_rw [not_isCofinal_iff] at h₂
   choose f hf using h₂
@@ -200,7 +202,84 @@ theorem isCofinal_of_isCofinal_sUnion {α : Type*} [LinearOrder α] {s : Set (Se
 /-- If the union of the `ι`-indexed family `s` is cofinal and `ι` is smaller than the cofinality,
 then `s` has a cofinal member. -/
 theorem isCofinal_of_isCofinal_iUnion {α : Type*} {ι} [LinearOrder α] {s : ι → Set α}
-    (h₁ : IsCofinal (⋃ i, s i)) (h₂ : #ι < Order.cof α) : ∃ i, IsCofinal (s i) := by
+    (h₁ : IsCofinal (⋃ i, s i)) (h₂ : #ι < cof α) : ∃ i, IsCofinal (s i) := by
   rw [← sUnion_range] at h₁
   obtain ⟨_, ⟨i, rfl⟩, h⟩ := isCofinal_of_isCofinal_sUnion h₁ (mk_range_le.trans_lt h₂)
   exact ⟨i, h⟩
+
+/-! ### Cofinality within order -/
+
+namespace Order
+variable {x : α}
+
+section Preorder
+variable [Preorder α]
+
+/-- The cofinality of an element `x` within a preorder is defined as `cof (Iio x)`. -/
+@[expose]
+def cofWithin (x : α) : Cardinal :=
+  cof (Iio x)
+
+@[simp]
+theorem cof_Iio (x : α) : cof (Iio x) = cofWithin x :=
+  rfl
+
+theorem cofWithin_le {s : Set α} (hs : IsCofinalFor (Iio x) s) (hsx : s ⊆ Iio x) :
+    cofWithin x ≤ #s := by
+  trans #(Iio x ↓∩ s)
+  · refine cof_le fun ⟨y, hy⟩ ↦ ?_
+    obtain ⟨z, hz, hyz⟩ := hs hy
+    refine ⟨⟨z, hsx hz⟩, ?_, ?_⟩ <;> simpa
+  · exact mk_preimage_val_le_right ..
+
+@[simp]
+theorem cofWithin_eq_zero_iff : cofWithin x = 0 ↔ IsMin x := by
+  rw [cofWithin, cof_eq_zero_iff, isEmpty_coe_sort, Iio_eq_empty_iff]
+
+@[simp]
+theorem cofWithin_bot [OrderBot α] : cofWithin (⊥ : α) = 0 :=
+  cofWithin_eq_zero_iff.2 isMin_bot
+
+end Preorder
+
+section LinearOrder
+variable [LinearOrder α]
+
+@[simp]
+theorem cofWithin_lt_aleph0_iff : cofWithin x < ℵ₀ ↔ cofWithin x ≤ 1 :=
+  cof_lt_aleph0_iff
+
+@[simp]
+theorem aleph0_le_cofWithin_iff : ℵ₀ ≤ cofWithin x ↔ 1 < cofWithin x :=
+  aleph0_le_cof_iff
+
+theorem cofWithin_eq_one_iff : cofWithin x = 1 ↔ ¬ IsSuccPrelimit x := by
+  rw [cofWithin, cof_eq_one_iff]
+  unfold IsTop IsSuccPrelimit CovBy
+  simp [← not_lt, imp_not_comm]
+
+theorem cofWithin_ne_one_iff : cofWithin x ≠ 1 ↔ IsSuccPrelimit x := by
+  rw [ne_eq, cofWithin_eq_one_iff, not_not]
+
+theorem cofWithin_le_one_iff : cofWithin x ≤ 1 ↔ ¬ IsSuccLimit x := by
+  rw [Cardinal.le_one_iff, cofWithin_eq_zero_iff, cofWithin_eq_one_iff,
+    IsSuccLimit, not_and_or, not_not]
+
+theorem one_lt_cofWithin_iff : 1 < cofWithin x ↔ IsSuccLimit x := by
+  rw [← not_le, cofWithin_le_one_iff, not_not]
+
+alias ⟨_, IsSuccPrelimit.cofWithin_ne_one⟩ := cofWithin_ne_one_iff
+alias ⟨_, IsSuccLimit.one_lt_cofWithin⟩ := one_lt_cofWithin_iff
+
+theorem IsSuccLimit.cofWithin_ne_one (hx : IsSuccLimit x) : cofWithin x ≠ 1 :=
+  hx.one_lt_cofWithin.ne'
+
+theorem cofWithin_succ_of_not_isMax (hx : ¬ IsMax x) [SuccOrder α] : cofWithin (succ x) = 1 :=
+  cofWithin_eq_one_iff.2 (mt IsSuccPrelimit.isMax hx)
+
+@[simp]
+theorem cofWithin_succ (x : α) [SuccOrder α] [NoMaxOrder α] : cofWithin (succ x) = 1 :=
+  cofWithin_succ_of_not_isMax (not_isMax x)
+
+end LinearOrder
+end Order
diff --git a/Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean b/Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean
index a3fbe3edf236a9..371104048db39e 100644
--- a/Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean
+++ b/Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean
@@ -43,6 +43,7 @@ theorem Order.cof_int : cof ℤ = ℵ₀ := by simp
 namespace Ordinal
 
 /-- The cofinality on an ordinal is the `Order.cof` of any isomorphic linear order.
+This is the same as `Order.cofWithin`, but without the universe bump.
 
 In particular, `cof 0 = 0` and `cof (succ o) = 1`. -/
 def cof (o : Ordinal.{u}) : Cardinal.{u} :=
@@ -73,13 +74,13 @@ theorem lift_cof (o : Ordinal.{u}) : Cardinal.lift.{v} (cof o) = cof (Ordinal.li
   rw [cof_type, ← type_lt_ulift, cof_type, ← Cardinal.lift_id'.{u, v} (Order.cof (ULift _)),
     ← Cardinal.lift_umax, ← ULift.orderIso.lift_cof_congr]
 
-theorem _root_.Order.cof_Iio [LinearOrder α] [WellFoundedLT α] (x : α) :
-    Order.cof (Iio x) = cof (typein (α := α) (· < ·) x) :=
-  (cof_type _).symm
+theorem cof_typein [LinearOrder α] [WellFoundedLT α] (x : α) :
+    cof (typein (α := α) (· < ·) x) = cofWithin x :=
+  (cof_type _)
 
 @[simp]
-theorem cof_Iio (o : Ordinal.{u}) : Order.cof (Iio o) = cof (lift.{u + 1} o) := by
-  rw [Order.cof_Iio, typein_ordinal]
+theorem _root_.Order.cofWithin_ordinal (o : Ordinal.{u}) : cofWithin o = cof (lift.{u + 1} o) := by
+  rw [← cof_typein, typein_ordinal]
 
 theorem cof_le_card (o : Ordinal) : cof o ≤ card o := by
   simpa using cof_le_cardinalMk o.ToType
@@ -263,7 +264,7 @@ theorem sSup_add_one_lt_of_lt_cof {s : Set Ordinal.{u}} {a : Ordinal.{u}}
   · simp [hs]
   · rintro rfl
     rw [← lift_cof, ← Cardinal.lift_lt.{_, u + 2}, Cardinal.lift_lift,
-      lift_cof_iSup_add_one fun _ ↦ by simp, cof_Iio, ← lift_cof, cof_type,
+      lift_cof_iSup_add_one fun _ ↦ by simp, cof_Iio, cofWithin_ordinal, ← lift_cof, cof_type,
       Cardinal.lift_lift, Cardinal.lift_lt] at ha
     exact ha.not_ge (cof_le_cardinalMk _)
 
@@ -563,7 +564,7 @@ theorem _root_.Order.cof_ordinal : Order.cof Ordinal.{u} = Cardinal.univ.{u, u +
   have := (OrderIso.ofRelIsoLT liftPrincipalSeg.subrelIso.{u, u + 1}).lift_cof_congr
   rw [Cardinal.lift_id'.{_, u + 2}] at this
   change Order.cof (Iio univ) = _ at this
-  rwa [cof_Iio, ← lift_cof, Cardinal.lift_inj, cof_univ, eq_comm] at this
+  rwa [cof_Iio, cofWithin_ordinal, ← lift_cof, Cardinal.lift_inj, cof_univ, eq_comm] at this
 
 @[simp]
 theorem _root_.Order.cof_cardinal : Order.cof Cardinal.{u} = Cardinal.univ.{u, u + 1} := by

From ab77d094b1bb6f7e6f55d9fb64814b5480a22627 Mon Sep 17 00:00:00 2001
From: vihdzp <vi.hdz.p@gmail.com>
Date: Fri, 22 May 2026 11:25:32 -0600
Subject: [PATCH 02/12] unused

---
 Mathlib/SetTheory/Cardinal/Cofinality/Basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/SetTheory/Cardinal/Cofinality/Basic.lean b/Mathlib/SetTheory/Cardinal/Cofinality/Basic.lean
index 62b239350df651..042786bce901d2 100644
--- a/Mathlib/SetTheory/Cardinal/Cofinality/Basic.lean
+++ b/Mathlib/SetTheory/Cardinal/Cofinality/Basic.lean
@@ -19,7 +19,7 @@ cardinality of a cofinal subset.
 
 public noncomputable section
 
-open Function Cardinal Set Set.Notation Order
+open Cardinal Set Notation Order
 
 universe u v w
 

From a587fcf773c133774bdd12fa8fcabbcd836e501a Mon Sep 17 00:00:00 2001
From: vihdzp <vi.hdz.p@gmail.com>
Date: Fri, 22 May 2026 11:28:41 -0600
Subject: [PATCH 03/12] golf

---
 Mathlib/SetTheory/Cardinal/Cofinality/Basic.lean | 10 ++++------
 1 file changed, 4 insertions(+), 6 deletions(-)

diff --git a/Mathlib/SetTheory/Cardinal/Cofinality/Basic.lean b/Mathlib/SetTheory/Cardinal/Cofinality/Basic.lean
index 042786bce901d2..e578c3d9fb8b2f 100644
--- a/Mathlib/SetTheory/Cardinal/Cofinality/Basic.lean
+++ b/Mathlib/SetTheory/Cardinal/Cofinality/Basic.lean
@@ -19,7 +19,7 @@ cardinality of a cofinal subset.
 
 public noncomputable section
 
-open Cardinal Set Notation Order
+open Cardinal Set Order
 
 universe u v w
 
@@ -226,11 +226,9 @@ theorem cof_Iio (x : α) : cof (Iio x) = cofWithin x :=
 
 theorem cofWithin_le {s : Set α} (hs : IsCofinalFor (Iio x) s) (hsx : s ⊆ Iio x) :
     cofWithin x ≤ #s := by
-  trans #(Iio x ↓∩ s)
-  · refine cof_le fun ⟨y, hy⟩ ↦ ?_
-    obtain ⟨z, hz, hyz⟩ := hs hy
-    refine ⟨⟨z, hsx hz⟩, ?_, ?_⟩ <;> simpa
-  · exact mk_preimage_val_le_right ..
+  refine (cof_le fun ⟨y, hy⟩ ↦ ?_).trans <| mk_preimage_val_le_right ..
+  obtain ⟨z, hz, hyz⟩ := hs hy
+  exact ⟨⟨z, hsx hz⟩, hz, hyz⟩
 
 @[simp]
 theorem cofWithin_eq_zero_iff : cofWithin x = 0 ↔ IsMin x := by

From 899c6c171c8734c2c9f9b9921b748a4b810f5d9a Mon Sep 17 00:00:00 2001
From: vihdzp <vi.hdz.p@gmail.com>
Date: Fri, 22 May 2026 11:29:26 -0600
Subject: [PATCH 04/12] ove

---
 Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean b/Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean
index 371104048db39e..fae3e01970d963 100644
--- a/Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean
+++ b/Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean
@@ -62,6 +62,10 @@ theorem cof_type (α : Type*) [LinearOrder α] [WellFoundedLT α] :
 theorem cof_toType (o : Ordinal) : Order.cof o.ToType = o.cof := by
   conv_rhs => rw [← type_toType o, cof_type]
 
+theorem cof_typein [LinearOrder α] [WellFoundedLT α] (x : α) :
+    cof (typein (α := α) (· < ·) x) = cofWithin x :=
+  cof_type _
+
 @[deprecated (since := "2026-02-18")] alias cof_eq_cof_toType := cof_toType
 @[deprecated (since := "2026-02-18")] alias le_cof_type := le_cof_iff
 @[deprecated (since := "2026-02-18")] alias cof_type_le := cof_le
@@ -74,10 +78,6 @@ theorem lift_cof (o : Ordinal.{u}) : Cardinal.lift.{v} (cof o) = cof (Ordinal.li
   rw [cof_type, ← type_lt_ulift, cof_type, ← Cardinal.lift_id'.{u, v} (Order.cof (ULift _)),
     ← Cardinal.lift_umax, ← ULift.orderIso.lift_cof_congr]
 
-theorem cof_typein [LinearOrder α] [WellFoundedLT α] (x : α) :
-    cof (typein (α := α) (· < ·) x) = cofWithin x :=
-  (cof_type _)
-
 @[simp]
 theorem _root_.Order.cofWithin_ordinal (o : Ordinal.{u}) : cofWithin o = cof (lift.{u + 1} o) := by
   rw [← cof_typein, typein_ordinal]

From a89766e252d47ce31daf0f68400fd833be6a0b91 Mon Sep 17 00:00:00 2001
From: vihdzp <vi.hdz.p@gmail.com>
Date: Fri, 22 May 2026 11:31:39 -0600
Subject: [PATCH 05/12] reorder

---
 Mathlib/SetTheory/Cardinal/Basic.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/Mathlib/SetTheory/Cardinal/Basic.lean b/Mathlib/SetTheory/Cardinal/Basic.lean
index d65e9f9ba1d508..cc816094c43c95 100644
--- a/Mathlib/SetTheory/Cardinal/Basic.lean
+++ b/Mathlib/SetTheory/Cardinal/Basic.lean
@@ -942,14 +942,14 @@ theorem mk_preimage_of_subset_range (f : α → β) (s : Set β) (h : s ⊆ rang
   rw [← lift_id #(↑(f ⁻¹' s)), ← lift_id #(↑s)]
   exact mk_preimage_of_subset_range_lift f s h
 
-open Set.Notation in
-theorem mk_preimage_val_le_right (s t : Set α) : #(s ↓∩ t) ≤ #t :=
-  mk_preimage_of_injective _ _ Subtype.val_injective
-
 open Set.Notation in
 theorem mk_preimage_val_le_left (s t : Set α) : #(s ↓∩ t) ≤ #s :=
   mk_set_le _
 
+open Set.Notation in
+theorem mk_preimage_val_le_right (s t : Set α) : #(s ↓∩ t) ≤ #t :=
+  mk_preimage_of_injective _ _ Subtype.val_injective
+
 theorem mk_subset_ge_of_subset_image_lift {α : Type u} {β : Type v} (f : α → β) {s : Set α}
     {t : Set β} (h : t ⊆ f '' s) : lift.{u} #t ≤ lift.{v} #({ x ∈ s | f x ∈ t } : Set α) := by
   rw [image_eq_range] at h

From c91314f03a31e007638a8c976d621abd91c891bb Mon Sep 17 00:00:00 2001
From: vihdzp <vi.hdz.p@gmail.com>
Date: Fri, 22 May 2026 11:33:06 -0600
Subject: [PATCH 06/12] unused

---
 Mathlib/SetTheory/Cardinal/Cofinality/Basic.lean | 2 --
 1 file changed, 2 deletions(-)

diff --git a/Mathlib/SetTheory/Cardinal/Cofinality/Basic.lean b/Mathlib/SetTheory/Cardinal/Cofinality/Basic.lean
index e578c3d9fb8b2f..9da14d961a43da 100644
--- a/Mathlib/SetTheory/Cardinal/Cofinality/Basic.lean
+++ b/Mathlib/SetTheory/Cardinal/Cofinality/Basic.lean
@@ -8,8 +8,6 @@ module
 public import Mathlib.Order.Cofinal
 public import Mathlib.SetTheory.Cardinal.Basic
 
-import Mathlib.Order.LatticeIntervals
-
 /-!
 # Cofinality of an order
 

From 20b5ef741fa39300302c053d0dba8eb74fce1caf Mon Sep 17 00:00:00 2001
From: vihdzp <vi.hdz.p@gmail.com>
Date: Fri, 22 May 2026 11:38:59 -0600
Subject: [PATCH 07/12] tweak

---
 Mathlib/SetTheory/Cardinal/Cofinality/Basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/SetTheory/Cardinal/Cofinality/Basic.lean b/Mathlib/SetTheory/Cardinal/Cofinality/Basic.lean
index 9da14d961a43da..512dcc044a8caa 100644
--- a/Mathlib/SetTheory/Cardinal/Cofinality/Basic.lean
+++ b/Mathlib/SetTheory/Cardinal/Cofinality/Basic.lean
@@ -239,7 +239,7 @@ theorem cofWithin_bot [OrderBot α] : cofWithin (⊥ : α) = 0 :=
 end Preorder
 
 section LinearOrder
-variable [LinearOrder α]
+variable [LinearOrder α] [LinearOrder β]
 
 @[simp]
 theorem cofWithin_lt_aleph0_iff : cofWithin x < ℵ₀ ↔ cofWithin x ≤ 1 :=

From 2d0f7c4c4718f2695b62151633c50517697946ff Mon Sep 17 00:00:00 2001
From: vihdzp <vi.hdz.p@gmail.com>
Date: Fri, 22 May 2026 11:47:25 -0600
Subject: [PATCH 08/12] simp

---
 Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean b/Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean
index fae3e01970d963..bfb7bd8b82b1cd 100644
--- a/Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean
+++ b/Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean
@@ -62,6 +62,7 @@ theorem cof_type (α : Type*) [LinearOrder α] [WellFoundedLT α] :
 theorem cof_toType (o : Ordinal) : Order.cof o.ToType = o.cof := by
   conv_rhs => rw [← type_toType o, cof_type]
 
+@[simp]
 theorem cof_typein [LinearOrder α] [WellFoundedLT α] (x : α) :
     cof (typein (α := α) (· < ·) x) = cofWithin x :=
   cof_type _

From 0e41dbc92dd94ff14fedb5eb8c1429ee69501614 Mon Sep 17 00:00:00 2001
From: vihdzp <vi.hdz.p@gmail.com>
Date: Fri, 22 May 2026 16:32:27 -0600
Subject: [PATCH 09/12] deprecation

---
 Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean b/Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean
index bfb7bd8b82b1cd..fbe639e68d5bea 100644
--- a/Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean
+++ b/Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean
@@ -83,6 +83,10 @@ theorem lift_cof (o : Ordinal.{u}) : Cardinal.lift.{v} (cof o) = cof (Ordinal.li
 theorem _root_.Order.cofWithin_ordinal (o : Ordinal.{u}) : cofWithin o = cof (lift.{u + 1} o) := by
   rw [← cof_typein, typein_ordinal]
 
+@[deprecated (since := "2026-05-22")]
+protected theorem cof_Iio (o : Ordinal.{u}) : Order.cof (Iio o) = cof (lift.{u + 1} o) :=
+  cofWithin_ordinal o
+
 theorem cof_le_card (o : Ordinal) : cof o ≤ card o := by
   simpa using cof_le_cardinalMk o.ToType
 

From 59fd5ecee40bda4d6021d3523372f7567f28be22 Mon Sep 17 00:00:00 2001
From: vihdzp <vi.hdz.p@gmail.com>
Date: Fri, 22 May 2026 16:32:52 -0600
Subject: [PATCH 10/12] fix

---
 Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean b/Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean
index fbe639e68d5bea..a4896b26fd0392 100644
--- a/Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean
+++ b/Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean
@@ -83,7 +83,7 @@ theorem lift_cof (o : Ordinal.{u}) : Cardinal.lift.{v} (cof o) = cof (Ordinal.li
 theorem _root_.Order.cofWithin_ordinal (o : Ordinal.{u}) : cofWithin o = cof (lift.{u + 1} o) := by
   rw [← cof_typein, typein_ordinal]
 
-@[deprecated (since := "2026-05-22")]
+@[deprecated cofWithin_ordinal (since := "2026-05-22")]
 protected theorem cof_Iio (o : Ordinal.{u}) : Order.cof (Iio o) = cof (lift.{u + 1} o) :=
   cofWithin_ordinal o
 

From 8539be99f47f18ccf1dce2cbcec324917cc01ff6 Mon Sep 17 00:00:00 2001
From: vihdzp <vi.hdz.p@gmail.com>
Date: Sun, 24 May 2026 11:38:02 -0600
Subject: [PATCH 11/12] unexpose

---
 Mathlib/SetTheory/Cardinal/Cofinality/Basic.lean | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/Mathlib/SetTheory/Cardinal/Cofinality/Basic.lean b/Mathlib/SetTheory/Cardinal/Cofinality/Basic.lean
index 512dcc044a8caa..48be5deee9f5b2 100644
--- a/Mathlib/SetTheory/Cardinal/Cofinality/Basic.lean
+++ b/Mathlib/SetTheory/Cardinal/Cofinality/Basic.lean
@@ -214,13 +214,12 @@ section Preorder
 variable [Preorder α]
 
 /-- The cofinality of an element `x` within a preorder is defined as `cof (Iio x)`. -/
-@[expose]
 def cofWithin (x : α) : Cardinal :=
   cof (Iio x)
 
 @[simp]
 theorem cof_Iio (x : α) : cof (Iio x) = cofWithin x :=
-  rfl
+  (rfl)
 
 theorem cofWithin_le {s : Set α} (hs : IsCofinalFor (Iio x) s) (hsx : s ⊆ Iio x) :
     cofWithin x ≤ #s := by

From 0129929a52c3e33bd1af4ef6bb2ce48d8ebc96f0 Mon Sep 17 00:00:00 2001
From: vihdzp <vi.hdz.p@gmail.com>
Date: Sun, 24 May 2026 14:52:12 -0600
Subject: [PATCH 12/12] fix

---
 Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean | 10 ++++++----
 1 file changed, 6 insertions(+), 4 deletions(-)

diff --git a/Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean b/Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean
index b6a60fd10036d0..f6d1b20211a7af 100644
--- a/Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean
+++ b/Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean
@@ -64,8 +64,9 @@ theorem cof_toType (o : Ordinal) : Order.cof o.ToType = o.cof := by
 
 @[simp]
 theorem cof_typein [LinearOrder α] [WellFoundedLT α] (x : α) :
-    cof (typein (α := α) (· < ·) x) = cofWithin x :=
-  cof_type _
+    cof (typein (α := α) (· < ·) x) = cofWithin x := by
+  rw [← cof_Iio]
+  exact cof_type _
 
 @[deprecated (since := "2026-02-18")] alias cof_eq_cof_toType := cof_toType
 @[deprecated (since := "2026-02-18")] alias le_cof_type := le_cof_iff
@@ -84,8 +85,9 @@ theorem _root_.Order.cofWithin_ordinal (o : Ordinal.{u}) : cofWithin o = cof (li
   rw [← cof_typein, typein_ordinal]
 
 @[deprecated cofWithin_ordinal (since := "2026-05-22")]
-protected theorem cof_Iio (o : Ordinal.{u}) : Order.cof (Iio o) = cof (lift.{u + 1} o) :=
-  cofWithin_ordinal o
+protected theorem cof_Iio (o : Ordinal.{u}) : Order.cof (Iio o) = cof (lift.{u + 1} o) := by
+  rw [cof_Iio]
+  exact cofWithin_ordinal o
 
 theorem cof_le_card (o : Ordinal) : cof o ≤ card o := by
   simpa using cof_le_cardinalMk o.ToType