feat(set_theory/game/pgame): Conway induction on games (#13699)

This is a more convenient restatement of the induction principle of the type.

src/set_theory/game/pgame.lean

@@ -148,6 +148,13 @@ def move_right : Π (g : pgame), right_moves g → pgame
 @[simp] lemma right_moves_mk {xl xr xL xR} : (⟨xl, xr, xL, xR⟩ : pgame).right_moves = xr := rfl
 @[simp] lemma move_right_mk {xl xr xL xR} : (⟨xl, xr, xL, xR⟩ : pgame).move_right = xR := rfl
 
+/-- A variant of `pgame.rec_on` expressed in terms of `pgame.move_left` and `pgame.move_right`.
+
+Both this and `pgame.rec_on` describe Conway induction on games. -/
+@[elab_as_eliminator] def move_rec_on {C : pgame → Sort*} (x : pgame)
+  (IH : ∀ (y : pgame), (∀ i, C (y.move_left i)) → (∀ j, C (y.move_right j)) → C y) : C x :=
+x.rec_on $ λ yl yr yL yR, IH (mk yl yr yL yR)
+
 /-- `subsequent p q` says that `p` can be obtained by playing
   some nonempty sequence of moves from `q`. -/
 inductive subsequent : pgame → pgame → Prop