chore(SetTheory/Ordinal/Basic): remove simps from enumIsoToType (#1…

…6907)

Since lemmas like [`Ordinal.enum_lt_enum`](https://leanprover-community.github.io/mathlib4_docs/Mathlib/SetTheory/Ordinal/Basic.html#Ordinal.enum_lt_enum) can't be made into `simp` lemmas, we actually *lose* `simp` capability by having the `simps` attribute here. This was breaking some proofs in my nimber project.

Mathlib/SetTheory/Ordinal/Basic.lean

@@ -1002,7 +1002,7 @@ theorem enum_inj {r : α → α → Prop} [IsWellOrder α r] {o₁ o₂ : {o //
   rw [EmbeddingLike.apply_eq_iff_eq, Subtype.mk.injEq]
 
 /-- The order isomorphism between ordinals less than `o` and `o.toType`. -/
-@[simps!]
+@[simps! (config := .lemmasOnly)]
 noncomputable def enumIsoToType (o : Ordinal) : Set.Iio o ≃o o.toType where
   toFun x :=
     enum (α := o.toType) (· < ·) ⟨x.1, by