chore(SetTheory/Ordinal/Arithmetic): fix Ordinal.enum type signature (

#17601)

For some reason, Lean was inferring [some nonsense](https://leanprover-community.github.io/mathlib4_docs/Mathlib/SetTheory/Ordinal/Basic.html#Ordinal.enum).

Unfortunately, the explicit typing is required for `simp`; see [Zulip](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/simp.20and.20subrel).

Mathlib/SetTheory/Ordinal/Basic.lean

@@ -449,7 +449,7 @@ the elements of `α`. -/
 -- The explicit typing is required in order for `simp` to work properly.
 @[simps! symm_apply_coe]
 def enum (r : α → α → Prop) [IsWellOrder α r] :
-    @RelIso (Subtype fun o => o < type r) α (Subrel (· < · ) _) r :=
+    @RelIso { o // o < type r } α (Subrel (· < ·) { o | o < type r }) r :=
   (typein.principalSeg r).subrelIso
 
 @[simp]