feat(set_theory/game/ordinal): golf to_pgame_injective (#14661)

We also add the `eq_iff` version and remove an outdated todo comment.

src/set_theory/game/ordinal.lean

@@ -99,13 +99,10 @@ lt_of_le_of_lf (to_pgame_le h.le) (to_pgame_lf h)
 by rw [pgame.equiv, le_antisymm_iff, to_pgame_le_iff, to_pgame_le_iff]
 
 theorem to_pgame_injective : function.injective ordinal.to_pgame :=
-λ a b h, begin
-  by_contra hne,
-  cases lt_or_gt_of_ne hne with hlt hlt;
-  { have := to_pgame_lt hlt,
-    rw h at this,
-    exact lt_irrefl _ this }
-end
+λ a b h, to_pgame_equiv_iff.1 $ equiv_of_eq h
+
+@[simp] theorem to_pgame_eq_iff {a b : ordinal} : a.to_pgame = b.to_pgame ↔ a = b :=
+to_pgame_injective.eq_iff
 
 /-- The order embedding version of `to_pgame`. -/
 @[simps] noncomputable def to_pgame_embedding : ordinal.{u} ↪o pgame.{u} :=

src/set_theory/game/pgame.lean

@@ -503,8 +503,6 @@ classical.some_spec $ (zero_le.1 h) j
 If `x ≈ 0`, then the second player can always win `x`. -/
 def equiv (x y : pgame) : Prop := x ≤ y ∧ y ≤ x
 
--- TODO: add `equiv.le` and `equiv.ge` synonyms for `equiv.1` and `equiv.2`.
-
 local infix ` ≈ ` := pgame.equiv
 
 instance : is_equiv _ (≈) :=
@@ -520,6 +518,8 @@ theorem equiv_refl (x) : x ≈ x := refl x
 @[symm] protected theorem equiv.symm {x y} : x ≈ y → y ≈ x := symm
 @[trans] protected theorem equiv.trans {x y z} : x ≈ y → y ≈ z → x ≈ z := trans
 
+theorem equiv_of_eq {x y} (h : x = y) : x ≈ y := by subst h
+
 @[trans] theorem le_of_le_of_equiv {x y z} (h₁ : x ≤ y) (h₂ : y ≈ z) : x ≤ z := h₁.trans h₂.1
 @[trans] theorem le_of_equiv_of_le {x y z} (h₁ : x ≈ y) : y ≤ z → x ≤ z := h₁.1.trans