feat(set_theory/ordinal/basic): Order isomorphism between o.out.α a…

…nd `set.Iio o` (#14074)

This strengthens the previously existing equivalence.

src/set_theory/game/nim.lean

@@ -107,12 +107,12 @@ lemma move_right_nim_heq (O : ordinal) : (nim O).move_right == λ i : O.out.α,
 by { rw nim_def, refl }
 
 /-- Turns an ordinal less than `O` into a left move for `nim O` and viceversa. -/
-noncomputable def to_left_moves_nim {O : ordinal} : {O' // O' < O} ≃ (nim O).left_moves :=
-(out_equiv_lt O).trans (equiv.cast (left_moves_nim O).symm)
+noncomputable def to_left_moves_nim {O : ordinal} : set.Iio O ≃ (nim O).left_moves :=
+(enum_iso_out O).to_equiv.trans (equiv.cast (left_moves_nim O).symm)
 
 /-- Turns an ordinal less than `O` into a right move for `nim O` and viceversa. -/
-noncomputable def to_right_moves_nim {O : ordinal} : {O' // O' < O} ≃ (nim O).right_moves :=
-(out_equiv_lt O).trans (equiv.cast (right_moves_nim O).symm)
+noncomputable def to_right_moves_nim {O : ordinal} : set.Iio O ≃ (nim O).right_moves :=
+(enum_iso_out O).to_equiv.trans (equiv.cast (right_moves_nim O).symm)
 
 @[simp] theorem to_left_moves_nim_symm_lt {O : ordinal} (i : (nim O).left_moves) :
   ↑(to_left_moves_nim.symm i) < O :=

src/set_theory/game/ordinal.lean

@@ -53,8 +53,8 @@ by { rw to_pgame_right_moves, apply_instance }
 
 /-- Converts an ordinal less than `o` into a move for the `pgame` corresponding to `o`, and vice
 versa. -/
-noncomputable def to_left_moves_to_pgame {o : ordinal} : {o' // o' < o} ≃ o.to_pgame.left_moves :=
-(out_equiv_lt o).trans (equiv.cast (to_pgame_left_moves o).symm)
+noncomputable def to_left_moves_to_pgame {o : ordinal} : set.Iio o ≃ o.to_pgame.left_moves :=
+(enum_iso_out o).to_equiv.trans (equiv.cast (to_pgame_left_moves o).symm)
 
 @[simp] theorem to_left_moves_to_pgame_symm_lt {o : ordinal} (i : o.to_pgame.left_moves) :
   ↑(to_left_moves_to_pgame.symm i) < o :=
@@ -77,7 +77,8 @@ by { convert pgame.move_left_lt (to_left_moves_to_pgame ⟨a, h⟩), rw to_pgame
 
 theorem to_pgame_le {a b : ordinal} (h : a ≤ b) : a.to_pgame ≤ b.to_pgame :=
 pgame.le_def.2 ⟨λ i, or.inl ⟨to_left_moves_to_pgame
-  ⟨_, (to_left_moves_to_pgame_symm_lt i).trans_le h⟩, by simp⟩, is_empty_elim⟩
+  ⟨(to_left_moves_to_pgame.symm i).val, (to_left_moves_to_pgame_symm_lt i).trans_le h⟩, by simp⟩,
+  is_empty_elim⟩
 
 @[simp] theorem to_pgame_lt_iff {a b : ordinal} : a.to_pgame < b.to_pgame ↔ a < b :=
 ⟨by { contrapose, rw [not_lt, pgame.not_lt], exact to_pgame_le }, to_pgame_lt⟩

src/set_theory/ordinal/arithmetic.lean

@@ -374,7 +374,7 @@ lemma type_subrel_lt (o : ordinal.{u}) :
 begin
   refine quotient.induction_on o _,
   rintro ⟨α, r, wo⟩, resetI, apply quotient.sound,
-  constructor, symmetry, refine (rel_iso.preimage equiv.ulift r).trans (typein_iso r)
+  constructor, symmetry, refine (rel_iso.preimage equiv.ulift r).trans (enum_iso r).symm
 end
 
 lemma mk_initial_seg (o : ordinal.{u}) :

src/set_theory/ordinal/basic.lean

@@ -681,20 +681,6 @@ enum_type (principal_seg.of_element r a)
 let ⟨a, e⟩ := typein_surj r h in
 by clear _let_match; subst e; rw enum_typein
 
-/-- The equivalence between ordinals less than `o` and `o.out.α`. -/
-@[simps] noncomputable def out_equiv_lt (o : ordinal) : {o' : ordinal // o' < o} ≃ o.out.α :=
-{ to_fun := λ ⟨o', h⟩, enum (<) o' (by rwa type_lt),
-  inv_fun := λ x, ⟨typein (<) x, typein_lt_self x⟩,
-  left_inv := λ ⟨o', h⟩, subtype.ext_val (typein_enum _ _),
-  right_inv := λ h, enum_typein _ _ }
-
-/-- A well order `r` is order isomorphic to the set of ordinals strictly smaller than the
-ordinal version of `r`. -/
-def typein_iso (r : α → α → Prop) [is_well_order α r] : r ≃r subrel (<) (< type r) :=
-⟨⟨λ x, ⟨typein r x, typein_lt_type r x⟩, λ x, enum r x.1 x.2, λ y, enum_typein r y,
- λ ⟨y, hy⟩, subtype.eq (typein_enum r hy)⟩,
-  λ a b, (typein_lt_typein r)⟩
-
 theorem enum_lt_enum {r : α → α → Prop} [is_well_order α r]
   {o₁ o₂ : ordinal} (h₁ : o₁ < type r) (h₂ : o₂ < type r) :
   r (enum r o₁ h₁) (enum r o₂ h₂) ↔ o₁ < o₂ :=
@@ -1130,6 +1116,22 @@ theorem enum_inj {r : α → α → Prop} [is_well_order α r] {o₁ o₂ : ordi
     { change _ < _ at hlt, rwa [←@enum_lt_enum α r _ o₂ o₁ h₂ h₁, h] at hlt }
 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,
+  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.{u}) : set.Iio o ≃o o.out.α :=
+{ to_fun := λ ⟨o', h⟩, enum (<) o' (by rwa type_lt),
+  inv_fun := λ x, ⟨typein (<) x, typein_lt_self x⟩,
+  left_inv := λ ⟨o', h⟩, subtype.ext_val (typein_enum _ _),
+  right_inv := λ h, enum_typein _ _,
+  map_rel_iff' := by { rintros ⟨a, _⟩ ⟨b, _⟩, apply enum_le_enum' } }
+
 /-- `o.out.α` is an `order_bot` whenever `0 < o`. -/
 def out_order_bot_of_pos {o : ordinal} (ho : 0 < o) : order_bot o.out.α :=
 ⟨_, enum_zero_le' ho⟩