chore(set_theory/ordinal/arithmetic): improve enum_iso def-eq (#15454)

By not casing on the argument of `to_fun`, we get much a much nicer `apply` projection.

src/set_theory/ordinal/basic.lean

@@ -741,15 +741,15 @@ end, λ h, by simp_rw h⟩
 
 /-- A well order `r` is order isomorphic to the set of ordinals smaller than `type r`. -/
 @[simps] def enum_iso (r : α → α → Prop) [is_well_order α r] : subrel (<) (< type r) ≃r r :=
-{ to_fun := λ ⟨o, h⟩, enum r o h,
+{ to_fun := λ x, enum r x.1 x.2,
   inv_fun := λ x, ⟨typein r x, typein_lt_type r x⟩,
   left_inv := λ ⟨o, h⟩, subtype.ext_val (typein_enum _ _),
   right_inv := λ h, enum_typein _ _,
   map_rel_iff' := by { rintros ⟨a, _⟩ ⟨b, _⟩, apply enum_lt_enum } }
 
 /-- The order isomorphism between ordinals less than `o` and `o.out.α`. -/
 @[simps] noncomputable def enum_iso_out (o : ordinal) : set.Iio o ≃o o.out.α :=
-{ to_fun := λ ⟨o', h⟩, enum (<) o' (by rwa type_lt),
+{ to_fun := λ x, enum (<) x.1 $ by { rw type_lt, exact x.2 },
   inv_fun := λ x, ⟨typein (<) x, typein_lt_self x⟩,
   left_inv := λ ⟨o', h⟩, subtype.ext_val (typein_enum _ _),
   right_inv := λ h, enum_typein _ _,