a lot

Author: vihdzp

Mathlib/Data/Fintype/Order.lean

@@ -195,6 +195,14 @@ lemma Directed.finite_le {ι κ : Sort*} [Nonempty ι] [Finite κ] {f : ι → 
   simpa using
     (hf.comp_of_surjective PLift.down_surjective).finite_set_le (Set.finite_range (PLift.up ∘ g))
 
+theorem DirectedOn.finite_le {s : Set α} (hs₀ : s.Nonempty) (D : DirectedOn r s)
+    (hs : s.Finite) : ∃ z ∈ s, ∀ i ∈ s, r i z := by
+  have := hs₀.to_subtype
+  have := hs.to_subtype
+  obtain ⟨⟨z, hzs⟩, hz⟩ := D.directed_val.finite_le id
+  use z, hzs
+  simpa using hz
+
 variable [Nonempty α] [Preorder α]
 
 theorem Finite.exists_le [IsDirectedOrder α] (f : β → α) : ∃ M, ∀ i, f i ≤ M :=

Mathlib/Order/DirSupClosed.lean

@@ -5,11 +5,12 @@ Authors: Christopher Hoskin, Violeta Hernández Palacios
 -/
 module
 
+public import Mathlib.Data.Fintype.Order
 public import Mathlib.Order.Antisymmetrization
 public import Mathlib.Order.CompleteLattice.Defs
 public import Mathlib.Order.UpperLower.Basic
 
-import Mathlib.Data.Set.Lattice
+import Mathlib.Data.Nat.Lattice
 
 /-!
 # Sets closed under directed suprema
@@ -300,6 +301,29 @@ theorem dirSupClosed_singleton (a : α) : DirSupClosed {a} := by
 theorem dirSupClosedOn_singleton (a : α) : DirSupClosedOn D {a} :=
   (dirSupClosed_singleton a).dirSupClosedOn
 
+theorem DirSupClosed.of_finite (hs : s.Finite) : DirSupClosed s := by
+  intro t ht ht₀ ht₁ a ha
+  obtain ⟨b, hbt, hb⟩ := ht₁.finite_le ht₀ (hs.subset ht)
+  exact ht <| ha.unique ⟨hb, fun x hx ↦ hx hbt⟩ ▸ hbt
+
+theorem dirSupClosed_range_nat {f : ℕ → α} (hf : Monotone f) (hf' : IsCofinal (.range f)) :
+    DirSupClosed (range f) := by
+  intro s hs hs₀ hs₁ a ha
+  obtain ⟨_, ⟨n, rfl⟩, han⟩ := hf' a
+  obtain rfl | han := han.eq_or_lt
+  · simp
+  have hfb : BddAbove (f ⁻¹' s) := by
+    refine ⟨n, fun m hm ↦ ?_⟩
+    by_contra! hnm
+    exact (ha.1 hm).not_gt (han.trans_le (hf hnm.le))
+  refine ⟨sSup (f ⁻¹' s), IsLUB.unique ⟨?_, ?_⟩ ha⟩ <;> intro x hx
+  · obtain ⟨m, rfl⟩ := hs hx
+    exact hf (le_csSup hfb hx)
+  · apply hx (Nat.sSup_mem _ hfb)
+    obtain ⟨x, hx⟩ := hs₀
+    obtain ⟨m, rfl⟩ := hs hx
+    exact ⟨m, hx⟩
+
 end PartialOrder
 
 section LinearOrder

Mathlib/SetTheory/Cardinal/Cofinality/Basic.lean

@@ -131,6 +131,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/Club.lean

@@ -5,9 +5,7 @@ Authors: Violeta Hernández Palacios
 -/
 module
 
-public import Mathlib.Order.DirSupClosed
-public import Mathlib.Order.IsNormal
-public import Mathlib.SetTheory.Cardinal.Cofinality.Basic
+public import Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
 
 /-!
 # Club sets
@@ -27,7 +25,7 @@ public section
 
 universe u v
 
-open Cardinal Order
+open Cardinal Order Ordinal
 
 /-- A club set is closed under suprema and cofinal. -/
 structure IsClub {α : Type*} [LinearOrder α] (s : Set α) where
@@ -51,7 +49,7 @@ theorem IsClub.univ : IsClub (α := α) .univ :=
 protected theorem IsClub.nonempty [Nonempty α] (hs : IsClub s) : s.Nonempty :=
   hs.isCofinal.nonempty
 
-theorem _root_.isClub_empty_iff : IsClub (α := α) ∅ ↔ IsEmpty α :=
+theorem isClub_empty_iff : IsClub (α := α) ∅ ↔ IsEmpty α :=
   ⟨fun h ↦ isCofinal_empty_iff.1 h.isCofinal, fun _ ↦ .of_isEmpty⟩
 
 theorem IsClub.union (hs : IsClub s) (ht : IsClub t) : IsClub (s ∪ t) :=
@@ -127,7 +125,7 @@ theorem IsClub.inter {s t : Set α} (hα : cof α ≠ ℵ₀) (hs : IsClub s) (h
   rw [← Set.sInter_pair]
   have H : ∀ x ∈ ({s, t} : Set _), IsClub x := by simpa [hs]
   obtain hα | hα' := hα.lt_or_gt
-  · rw [cof_lt_aleph0_iff] at hα
+  · rw [Order.cof_lt_aleph0_iff] at hα
     exact .sInter_of_cof_le_one hα H
   · exact .sInter hα (hα'.trans_le' <| by simp) H
 
@@ -180,7 +178,7 @@ theorem not_isStationary_empty : ¬ IsStationary (∅ : Set α) := by
 
 theorem IsClub.isStationary [Nonempty α] [WellFoundedLT α] (hα : cof α ≠ ℵ₀) (hs : IsClub s) :
     IsStationary s :=
-  fun t ht ↦ (hs.inter hα ht).nonempty
+  fun _ ht ↦ (hs.inter hα ht).nonempty
 
 /-- Non-stationary sets form an ideal. -/
 theorem not_isStationary_union [WellFoundedLT α] (hα : cof α ≠ ℵ₀)
@@ -191,6 +189,11 @@ theorem not_isStationary_union [WellFoundedLT α] (hα : cof α ≠ ℵ₀)
   refine ⟨_, hu.inter hα hv, ?_⟩
   grind
 
+theorem dirSupClosed_of_type_le_omega0 [WellFoundedLT α] {s : Set α} (hs : typeLT s ≤ ω) :
+    DirSupClosed s := by
+  
+  sorry
+
 theorem IsStationary.of_not_isCofinal_compl (hs : ¬ IsCofinal (sᶜ)) : IsStationary s := by
   intro t ht
   obtain ⟨a, ha⟩ := not_isCofinal_iff.1 hs
@@ -199,5 +202,9 @@ theorem IsStationary.of_not_isCofinal_compl (hs : ¬ IsCofinal (sᶜ)) : IsStati
   contrapose! ha
   exact ⟨b, ha, hb'⟩
 
-proof_wanted isStationary_iff_not_isCofinal_compl (hα : cof α ≤ ℵ₀) :
-    IsStationary s ↔ ¬ IsCofinal (sᶜ)
+theorem isStationary_iff_not_isCofinal_compl [WellFoundedLT α] (hα : cof α ≤ ℵ₀) :
+    IsStationary s ↔ ¬ IsCofinal (sᶜ) where
+  mp hs h := by
+    obtain ⟨t, ht, ht', htα⟩ := Ordinal.ord_cof_eq_of_isCofinal h
+    sorry
+  mpr := .of_not_isCofinal_compl

Mathlib/SetTheory/Cardinal/Cofinality/Ordinal.lean

@@ -151,7 +151,8 @@ 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
+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,8 +167,18 @@ theorem ord_cof_eq (α : Type*) [LinearOrder α] [WellFoundedLT α] :
     · obtain ⟨x, z, hz, rfl⟩ := x
       exact (hz _ hxy').asymm hxy
 
+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
+
+variable (α) in
 @[simp]
-theorem _root_.Order.cof_ord_cof (α : Type*) [LinearOrder α] [WellFoundedLT α] :
+theorem _root_.Order.cof_ord_cof [LinearOrder α] [WellFoundedLT α] :
     (Order.cof α).ord.cof = Order.cof α := by
   obtain ⟨s, hs, hs'⟩ := ord_cof_eq α
   rw [← hs', cof_type]
@@ -183,6 +194,14 @@ theorem cof_ord_cof (o : Ordinal) : o.cof.ord.cof = o.cof := by
 
 @[deprecated (since := "2026-03-21")] alias cof_cof := cof_ord_cof
 
+theorem dirSupClosed_of_type_le_omega0 [LinearOrder α] [WellFoundedLT α]
+    {s : Set α} (hs : IsCofinal s) (hs' : typeLT s ≤ ω) : DirSupClosed s := by
+  obtain rfl | hs₀ := s.eq_empty_or_nonempty
+  · simp
+  let f (n : ℕ) : α := if hn : n < typeLT s then enum (· < · : s → _) ⟨n, hn⟩
+  sorry
+
+#exit
 /-! ### Cofinalities and suprema -/
 
 section LinearOrder

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