chore: use notation3 for Ordinal.typeLT (#39798)

This creates a delaborator, which avoids goals from looking like `(type fun x1 x2 ↦ x1 < x2) < (type fun x1 x2 ↦ x1 < x2)`.

Author: vihdzp

Mathlib/SetTheory/Ordinal/Basic.lean

@@ -146,7 +146,11 @@ def type (r : α → α → Prop) [wo : IsWellOrder α r] : Ordinal :=
   ⟦⟨α, r, wo⟩⟧
 
 /-- `typeLT α` is an abbreviation for the order type of the `<` relation of `α`. -/
-scoped notation "typeLT " α:70 => @Ordinal.type α (· < ·) inferInstance
+scoped notation3 "typeLT " α:70 => @Ordinal.type α (· < ·) inferInstance
+
+/-- info: typeLT ℕ : Ordinal.{0} -/
+#guard_msgs in
+#check typeLT ℕ
 
 instance zero : Zero Ordinal :=
   ⟨type <| @emptyRelation PEmpty⟩