chore: no_expose various Ordinal definitions (#34729)

These all have convoluted definitions that are better characterized by their API, or (in the case of `Ordinal.ToType`) are defined through choice and have no useful definitional equalities.

Author: vihdzp

Mathlib/SetTheory/Cardinal/Cofinality.lean

@@ -253,7 +253,7 @@ theorem cof_eq_sInf_lsub (o : Ordinal.{u}) : cof o =
     sInf { a : Cardinal | ∃ (ι : Type u) (f : ι → Ordinal), lsub.{u, u} f = o ∧ #ι = a } := by
   refine le_antisymm (le_csInf (cof_lsub_def_nonempty o) ?_) (csInf_le' ?_)
   · rintro a ⟨ι, f, hf, rfl⟩
-    rw [← type_toType o]
+    rw [← type_toType o, cof_type]
     refine
       (cof_le fun a => ?_).trans
         (@mk_le_of_injective _ _

Mathlib/SetTheory/Ordinal/Basic.lean

@@ -106,7 +106,7 @@ def Ordinal : Type (u + 1) :=
   Quotient Ordinal.isEquivalent
 
 /-- A "canonical" type order-isomorphic to the ordinal `o`, living in the same universe. This is
-defined through the axiom of choice.
+defined through the axiom of choice; in particular, it has no useful def-eqs, and it is not exposed.
 
 Use this over `Iio o` only when it is paramount to have a `Type u` rather than a `Type (u + 1)`,
 and convert using
@@ -116,23 +116,26 @@ Ordinal.ToType.mk : Iio o → o.ToType
 Ordinal.ToType.toOrd : o.ToType → Iio o
 ```
 -/
+@[no_expose]
 def Ordinal.ToType (o : Ordinal.{u}) : Type u :=
   o.out.α
 
 @[deprecated (since := "2025-12-04")]
 alias Ordinal.toType := Ordinal.ToType
 
-instance hasWellFounded_toType (o : Ordinal) : WellFoundedRelation o.ToType :=
-  ⟨o.out.r, o.out.wo.wf⟩
-
+@[no_expose]
 instance linearOrder_toType (o : Ordinal) : LinearOrder o.ToType :=
   @IsWellOrder.linearOrder _ o.out.r o.out.wo
 
 instance wellFoundedLT_toType (o : Ordinal) : WellFoundedLT o.ToType :=
   o.out.wo.toIsWellFounded
 
+instance hasWellFounded_toType (o : Ordinal) : WellFoundedRelation o.ToType :=
+  WellFoundedLT.toWellFoundedRelation
+
 namespace Ordinal
 
+@[no_expose]
 noncomputable instance (o : Ordinal) : SuccOrder o.ToType :=
   .ofLinearWellFoundedLT _
 
@@ -1077,6 +1080,7 @@ theorem mk_toType (o : Ordinal) : #o.ToType = o.card :=
 
 /-- The ordinal corresponding to a cardinal `c` is the least ordinal
   whose cardinal is `c`. For the order-embedding version, see `ord.order_embedding`. -/
+@[no_expose]
 def ord (c : Cardinal) : Ordinal :=
   Quot.liftOn c (fun α : Type u => ⨅ r : { r // IsWellOrder α r }, @type α r.1 r.2) <| by
   rintro α β ⟨f⟩
@@ -1085,8 +1089,10 @@ def ord (c : Cardinal) : Ordinal :=
     refine ⟨⟨_, RelIso.IsWellOrder.preimage r ?_⟩, type_preimage _ _⟩
   exacts [f.symm, f]
 
-theorem ord_eq_Inf (α : Type u) : ord #α = ⨅ r : { r // IsWellOrder α r }, @type α r.1 r.2 :=
-  rfl
+theorem ord_eq_iInf (α : Type u) : ord #α = ⨅ r : { r // IsWellOrder α r }, @type α r.1 r.2 :=
+  (rfl)
+
+@[deprecated (since := "2026-03-15")] alias ord_eq_Inf := ord_eq_iInf
 
 /-- There exists a well-order on `α` whose order type is exactly `ord #α`. -/
 theorem ord_eq (α) : ∃ (r : α → α → Prop) (wo : IsWellOrder α r), ord #α = @type α r wo :=

Mathlib/SetTheory/Ordinal/Exponential.lean

@@ -15,9 +15,7 @@ related by the lemma `Ordinal.opow_le_iff_le_log : b ^ c ≤ x ↔ c ≤ log b x
 `b`, `c`.
 -/
 
-@[expose] public section
-
-noncomputable section
+public noncomputable section
 
 open Function Set Equiv Order
 open scoped Cardinal Ordinal
@@ -29,6 +27,7 @@ namespace Ordinal
 /-- The ordinal exponential, defined by transfinite recursion.
 
 We call this `opow` in theorems in order to disambiguate from other exponentials. -/
+@[no_expose]
 instance instPow : Pow Ordinal Ordinal :=
   ⟨fun a b ↦ if a = 0 then 1 - b else
     limitRecOn b 1 (fun _ x ↦ x * a) fun o _ f ↦ ⨆ x : Iio o, f x.1 x.2⟩