refactor(SetTheory/Ordinal): redefine Ordinal.ToType as Shrink (Iio o)

Mathlib/CategoryTheory/Presentable/Directed.lean

@@ -533,8 +533,10 @@ lemma exists_cardinal_directed (J : Type w) [SmallCategory J] (κ : Cardinal.{w}
   obtain ⟨α, _, _, F, _⟩ :=
     exists_cardinal_directed.aux (J × κ.ord.ToType) κ (fun ⟨j, x⟩ ↦
       ⟨⟨j, Order.succ x⟩, (𝟙 _, homOfLE (Order.le_succ x)), ⟨fun ⟨_, f⟩ ↦ by
-        have : NoMaxOrder κ.ord.ToType :=
-          Cardinal.noMaxOrder (Cardinal.IsRegular.aleph0_le Fact.out)
+        have : NoMaxOrder κ.ord.ToType := by
+          rw [← Ordinal.isSuccPrelimit_type_lt_iff, Ordinal.type_toType]
+          exact (Cardinal.isSuccLimit_ord
+            (Cardinal.IsRegular.aleph0_le Fact.out)).isSuccPrelimit
         exact not_isMax _ (Order.max_of_succ_le (leOfHom f))⟩⟩)
   exact ⟨_, _, inferInstance, F ⋙ Prod.fst _ _, inferInstance⟩
 

Mathlib/CategoryTheory/Presentable/IsCardinalFiltered.lean

@@ -197,11 +197,12 @@ lemma isCardinalFiltered_preorder (J : Type w) [Preorder J]
       { app a := homOfLE (hj a)
         naturality _ _ _ := rfl }⟩
 
-set_option backward.isDefEq.respectTransparency.types false in
 instance (κ : Cardinal.{w}) [hκ : Fact κ.IsRegular] :
     IsCardinalFiltered κ.ord.ToType κ :=
   isCardinalFiltered_preorder _ _ (fun ι f hs ↦ by
-    have h : Function.Surjective (fun i ↦ (⟨f i, i, rfl⟩ : Set.range f)) := fun _ ↦ by aesop
+    have h : Function.Surjective (fun i ↦ (⟨f i, i, rfl⟩ : Set.range f)) := by
+      rintro ⟨_, i, rfl⟩
+      exact ⟨i, rfl⟩
     contrapose! hs
     rw [← hκ.out.cof_ord, ← Ordinal.cof_toType]
     refine (Order.cof_le fun j ↦ ?_).trans (Cardinal.mk_le_of_surjective h)

Mathlib/CategoryTheory/Presentable/OrthogonalReflection.lean

@@ -367,7 +367,10 @@ variable [Fact κ.IsRegular]
 noncomputable def iterationObjSuccIso (j : κ.ord.ToType) :
   (iteration W Z κ).obj (Order.succ j) ≅ succ W ((iteration W Z κ).obj j) :=
     (succStruct W Z).iterationFunctorObjSuccIso j (by
-      have := Cardinal.noMaxOrder (Fact.elim inferInstance : κ.IsRegular).aleph0_le
+      have : NoMaxOrder κ.ord.ToType := by
+        rw [← Ordinal.isSuccPrelimit_type_lt_iff, Ordinal.type_toType]
+        exact (Cardinal.isSuccLimit_ord
+          (Fact.elim inferInstance : κ.IsRegular).aleph0_le).isSuccPrelimit
       exact not_isMax j)
 
 @[reassoc]

Mathlib/CategoryTheory/Presentable/SharplyLT/Basic.lean

@@ -230,7 +230,9 @@ lemma isCardinalFiltered_iUnion :
   obtain ⟨⟨x, hx⟩, hx'⟩ := hφ₀ Y hY' m hm _
     (hasCardinalLT_transfiniteIterate_φ h₀ Y hY m A hA _) f hK
   refine ⟨⟨x, ?_⟩, hx'⟩
-  have : NoMaxOrder κ₁.ord.ToType := noMaxOrder (IsRegular.aleph0_le Fact.out)
+  have : NoMaxOrder κ₁.ord.ToType := by
+    rw [← Ordinal.isSuccPrelimit_type_lt_iff, Ordinal.type_toType]
+    exact (isSuccLimit_ord (IsRegular.aleph0_le Fact.out)).isSuccPrelimit
   rwa [transfiniteIterate_succ _ _ _ (not_isMax j),
     φ_eq _ _ _ (hasCardinalLT_transfiniteIterate_φ h₀ Y hY m A hA _)]
 

Mathlib/CategoryTheory/SmallObject/IsCardinalForSmallObjectArgument.lean

@@ -245,7 +245,10 @@ lemma iterationFunctorObjObjRightIso_ιIteration_app_right (f : Arrow C) (j : κ
 lemma prop_iterationFunctor_map_succ (j : κ.ord.ToType) :
     (succStruct I κ).prop ((iterationFunctor I κ).map (homOfLE (Order.le_succ j))) := by
   have := hasIterationOfShape I κ
-  have := Cardinal.noMaxOrder (Fact.elim inferInstance : κ.IsRegular).aleph0_le
+  have : NoMaxOrder κ.ord.ToType := by
+    rw [← Ordinal.isSuccPrelimit_type_lt_iff, Ordinal.type_toType]
+    exact (Cardinal.isSuccLimit_ord
+      (Fact.elim inferInstance : κ.IsRegular).aleph0_le).isSuccPrelimit
   exact (succStruct I κ).prop_iterationFunctor_map_succ j (not_isMax j)
 
 set_option backward.defeqAttrib.useBackward true in
@@ -259,7 +262,10 @@ noncomputable def iterationFunctorMapSuccAppArrowIso (f : Arrow C) (j : κ.ord.T
     Arrow.mk (((iterationFunctor I κ).map (homOfLE (Order.le_succ j))).app f) ≅
       (ε I.homFamily).app (((iterationFunctor I κ).obj j).obj f) :=
   have := hasIterationOfShape I κ
-  have := Cardinal.noMaxOrder (Fact.elim inferInstance : κ.IsRegular).aleph0_le
+  have : NoMaxOrder κ.ord.ToType := by
+    rw [← Ordinal.isSuccPrelimit_type_lt_iff, Ordinal.type_toType]
+    exact (Cardinal.isSuccLimit_ord
+      (Fact.elim inferInstance : κ.IsRegular).aleph0_le).isSuccPrelimit
   Arrow.isoMk (Iso.refl _)
     (((evaluation _ _).obj f).mapIso
       ((succStruct I κ).iterationFunctorObjSuccIso j (not_isMax j))) (by

Mathlib/FieldTheory/CardinalEmb.lean

@@ -103,7 +103,9 @@ section Algebraic
 
 variable [rank_inf : Fact (ℵ₀ ≤ Module.rank F E)]
 
-lemma noMaxOrder_rank_toType : NoMaxOrder ι := Cardinal.noMaxOrder Fact.out
+lemma noMaxOrder_rank_toType : NoMaxOrder ι := by
+  rw [← Ordinal.isSuccPrelimit_type_lt_iff, Ordinal.type_toType]
+  exact (Cardinal.isSuccLimit_ord Fact.out).isSuccPrelimit
 attribute [local instance] noMaxOrder_rank_toType
 
 open _root_.Algebra (IsAlgebraic)

Mathlib/SetTheory/Ordinal/Arithmetic.lean

@@ -1021,9 +1021,10 @@ theorem isSuccLimit_ord {c} (hc : ℵ₀ ≤ c) : IsSuccLimit (ord c) := by
     · exact hc.trans ha
     · simp
 
--- TODO: deprecate in favor of `isSuccPrelimit_type_lt_iff`
+@[deprecated "This theorem exposes `Ordinal.ToType`; inline the proof if you already have an \
+`ord.ToType` goal." (since := "2026-06-18")]
 theorem noMaxOrder {c} (h : ℵ₀ ≤ c) : NoMaxOrder c.ord.ToType := by
-  rw [← isSuccPrelimit_type_lt_iff, type_toType]
+  rw [← Ordinal.isSuccPrelimit_type_lt_iff, Ordinal.type_toType]
   exact (isSuccLimit_ord h).isSuccPrelimit
 
 instance : Nonempty (ℵ₀ : Cardinal.{u}).ord.ToType := by simp