English
Two games are equal if they have the same left/right moves and identical move results under equivalence.
Русский
Две игры равны, если их левые и правые ходы совпадают, а результаты ходов совпадают при эквиваленции.
LaTeX
$$$ x = y \\iff [x.LeftMoves = y.LeftMoves] \\land [x.RightMoves = y.RightMoves] \\land [\\forall i \\in x.LeftMoves,\\forall j \\in y.LeftMoves, i \\approx j \\Rightarrow x.moveLeft i = y.moveLeft j] \\land [\\forall i \\in x.RightMoves,\\forall j \\in y.RightMoves, i \\approx j \\Rightarrow x.moveRight i = y.moveRight j] $$$
Lean4
theorem ext {x y : PGame} (hl : x.LeftMoves = y.LeftMoves) (hr : x.RightMoves = y.RightMoves)
(hL : ∀ i j, i ≍ j → x.moveLeft i = y.moveLeft j) (hR : ∀ i j, i ≍ j → x.moveRight i = y.moveRight j) : x = y :=
by
cases x
cases y
subst hl hr
simp only [leftMoves_mk, rightMoves_mk, heq_eq_eq, forall_eq', mk.injEq, true_and] at *
exact
⟨funext hL, funext hR⟩
-- TODO define this at the level of games, as well, and perhaps also for finsets of games.
