feat: more lemmas on Ordinal.type (leanprover-community#35519)

Extracted from leanprover-community#35513.

Author: vihdzp

Mathlib/Order/Max.lean

@@ -40,35 +40,36 @@ universe u v
 variable {α β : Type*}
 
 /-- Order without bottom elements. -/
+@[mk_iff noBotOrder_iff']
 class NoBotOrder (α : Type*) [LE α] : Prop where
   /-- For each term `a`, there is some `b` which is either incomparable or strictly smaller. -/
   exists_not_ge (a : α) : ∃ b, ¬a ≤ b
 
 /-- Order without top elements. -/
-@[to_dual]
+@[to_dual, mk_iff noTopOrder_iff']
 class NoTopOrder (α : Type*) [LE α] : Prop where
   /-- For each term `a`, there is some `b` which is either incomparable or strictly larger. -/
   exists_not_le (a : α) : ∃ b, ¬b ≤ a
 
 /-- Order without minimal elements. Sometimes called coinitial or dense. -/
+@[mk_iff noMinOrder_iff']
 class NoMinOrder (α : Type*) [LT α] : Prop where
   /-- For each term `a`, there is some strictly smaller `b`. -/
   exists_lt (a : α) : ∃ b, b < a
 
 /-- Order without maximal elements. Sometimes called cofinal. -/
-@[to_dual]
+@[to_dual, mk_iff noMaxOrder_iff']
 class NoMaxOrder (α : Type*) [LT α] : Prop where
   /-- For each term `a`, there is some strictly greater `b`. -/
   exists_gt (a : α) : ∃ b, a < b
 
 export NoBotOrder (exists_not_ge)
-
 export NoTopOrder (exists_not_le)
-
 export NoMinOrder (exists_lt)
-
 export NoMaxOrder (exists_gt)
 
+attribute [to_dual existing] noBotOrder_iff' noMinOrder_iff'
+
 @[to_dual nonempty_gt]
 instance nonempty_lt [LT α] [NoMinOrder α] (a : α) : Nonempty { x // x < a } :=
   nonempty_subtype.2 (exists_lt a)
@@ -147,6 +148,10 @@ conversion. -/]
 def IsMin (a : α) : Prop :=
   ∀ ⦃b⦄, b ≤ a → a ≤ b
 
+@[to_dual]
+theorem noBotOrder_iff : NoBotOrder α ↔ ∀ x : α, ¬ IsBot x := by
+  simp_rw [noBotOrder_iff', IsBot, not_forall]
+
 @[to_dual (attr := simp)]
 theorem not_isBot [NoBotOrder α] (a : α) : ¬IsBot a := fun h =>
   let ⟨_, hb⟩ := exists_not_ge a
@@ -194,6 +199,10 @@ section Preorder
 
 variable [Preorder α] {a b : α}
 
+@[to_dual]
+theorem noMinOrder_iff : NoMinOrder α ↔ ∀ x : α, ¬ IsMin x := by
+  simp [noMinOrder_iff', IsMin, lt_iff_le_not_ge]
+
 @[to_dual]
 theorem IsBot.mono (ha : IsBot a) (h : b ≤ a) : IsBot b := fun _ => h.trans <| ha _
 

Mathlib/SetTheory/Cardinal/Cofinality.lean

@@ -208,7 +208,7 @@ theorem cof_eq_sInf_lsub (o : Ordinal.{u}) : cof o =
 @[simp]
 theorem lift_cof (o) : Cardinal.lift.{u, v} (cof o) = cof (Ordinal.lift.{u, v} o) := by
   refine inductionOn o fun α r _ ↦ ?_
-  rw [← type_uLift, cof_type, cof_type, ← Cardinal.lift_id'.{v, u} (Order.cof _),
+  rw [← type_ulift, cof_type, cof_type, ← Cardinal.lift_id'.{v, u} (Order.cof _),
     ← Cardinal.lift_umax]
   apply RelIso.cof_eq_lift ⟨Equiv.ulift.symm, _⟩
   simp [swap]

Mathlib/SetTheory/Ordinal/Basic.lean

@@ -635,10 +635,17 @@ def lift (o : Ordinal.{v}) : Ordinal.{max v u} :=
       ⟨(RelIso.preimage Equiv.ulift r).trans <| f.trans (RelIso.preimage Equiv.ulift s).symm⟩
 
 @[simp]
-theorem type_uLift (r : α → α → Prop) [IsWellOrder α r] :
+theorem type_ulift (r : α → α → Prop) [IsWellOrder α r] :
     type (ULift.down ⁻¹'o r) = lift.{v} (type r) :=
   rfl
 
+@[deprecated (since := "2026-02-20")] alias type_uLift := type_ulift
+
+@[simp]
+theorem type_lt_ulift [LinearOrder α] [WellFoundedLT α] :
+    typeLT (ULift α) = lift.{v} (typeLT α) :=
+  rfl
+
 theorem _root_.RelIso.ordinal_lift_type_eq {r : α → α → Prop} {s : β → β → Prop}
     [IsWellOrder α r] [IsWellOrder β s] (f : r ≃r s) : lift.{v} (type r) = lift.{u} (type s) :=
   ((RelIso.preimage Equiv.ulift r).trans <|
@@ -949,6 +956,34 @@ instance uniqueToTypeOne : Unique (ToType 1) where
 theorem one_toType_eq (x : ToType 1) : x = enum (· < ·) ⟨0, by simp⟩ :=
   Unique.eq_default x
 
+theorem type_lt_mem_range_succ_iff [LinearOrder α] [WellFoundedLT α] :
+    typeLT α ∈ range succ ↔ ∃ x : α, IsMax x := by
+  simp_rw [← isTop_iff_isMax]
+  constructor <;> intro ⟨a, ha⟩
+  · refine ⟨enum (α := α) (· < ·) ⟨a, ?_⟩, fun b ↦ ?_⟩
+    · rw [mem_Iio, ← ha, lt_succ_iff]
+    · rw [← enum_typein (α := α) (· < ·) b, ← not_lt, enum_le_enum (r := (· < ·)),
+        Subtype.mk_le_mk, ← lt_succ_iff, ha]
+      exact typein_lt_type ..
+  · refine ⟨typein (α := α) (· < ·) a, eq_of_forall_lt_iff fun o ↦ ?_⟩
+    rw [lt_succ_iff]
+    refine ⟨fun h ↦ h.trans_lt (typein_lt_type _ _), fun h ↦ ?_⟩
+    rw [← typein_enum _ h, typein_le_typein, not_lt]
+    apply ha
+
+theorem type_lt_mem_range_succ [LinearOrder α] [WellFoundedLT α] [OrderTop α] :
+    typeLT α ∈ range succ :=
+  type_lt_mem_range_succ_iff.2 ⟨⊤, isMax_top⟩
+
+theorem isSuccPrelimit_type_lt_iff [LinearOrder α] [WellFoundedLT α] :
+    IsSuccPrelimit (typeLT α) ↔ NoMaxOrder α := by
+  rw [← not_iff_not, noMaxOrder_iff, not_isSuccPrelimit_iff', type_lt_mem_range_succ_iff]
+  simp [IsMax]
+
+theorem isSuccPrelimit_type_lt [LinearOrder α] [WellFoundedLT α] [h : NoMaxOrder α] :
+    IsSuccPrelimit (typeLT α) :=
+  isSuccPrelimit_type_lt_iff.2 h
+
 /-! ### Extra properties of typein and enum -/
 
 -- TODO: use `ToType.mk` for lemmas on `ToType` rather than `enum` and `typein`.