feat(set_theory/game/pgame): Define is_option relation (#13700)

src/set_theory/game/pgame.lean

@@ -155,6 +155,26 @@ Both this and `pgame.rec_on` describe Conway induction on games. -/
   (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)
 
+/-- `is_option x y` means that `x` is either a left or right option for `y`. -/
+@[mk_iff] inductive is_option : pgame → pgame → Prop
+| move_left {x : pgame} (i : x.left_moves) : is_option (x.move_left i) x
+| move_right {x : pgame} (i : x.right_moves) : is_option (x.move_right i) x
+
+theorem is_option.mk_left {xl xr : Type u} (xL : xl → pgame) (xR : xr → pgame) (i : xl) :
+  (xL i).is_option (mk xl xr xL xR) :=
+@is_option.move_left (mk _ _ _ _) i
+
+theorem is_option.mk_right {xl xr : Type u} (xL : xl → pgame) (xR : xr → pgame) (i : xr) :
+  (xR i).is_option (mk xl xr xL xR) :=
+@is_option.move_right (mk _ _ _ _) i
+
+theorem wf_is_option : well_founded is_option :=
+⟨λ x, move_rec_on x $ λ x IHl IHr, acc.intro x $ λ y h, begin
+  induction h with _ i _ j,
+  { exact IHl i },
+  { exact IHr j }
+end⟩
+
 /-- `subsequent p q` says that `p` can be obtained by playing
   some nonempty sequence of moves from `q`. -/
 inductive subsequent : pgame → pgame → Prop