English
If x,y have left/right moves related by equivalences L and R and corresponding left/right moves map to equal Games, then the quotients [x] and [y] in PGame-setoid are equal in Game.
Русский
Если x,y имеют левые и правые ходы, связанные эквивалностями L и R, и соответствующие ходы отображаются в равные игры, то квоты [x] и [y] в множестве PGame равны как объекты Game.
LaTeX
$$$ (\forall L,R) \; (\forall i, \llbracket x.moveLeft i \rrbracket = \llbracket y.moveLeft (L i) \rrbracket) \land (\forall j, \llbracket x.moveRight j \rrbracket = \llbracket y.moveRight (R j) \rrbracket) \Rightarrow \llbracket x \rrbracket = \llbracket y \rrbracket $$$
Lean4
theorem quot_eq_of_mk'_quot_eq {x y : PGame} (L : x.LeftMoves ≃ y.LeftMoves) (R : x.RightMoves ≃ y.RightMoves)
(hl : ∀ i, (⟦x.moveLeft i⟧ : Game) = ⟦y.moveLeft (L i)⟧)
(hr : ∀ j, (⟦x.moveRight j⟧ : Game) = ⟦y.moveRight (R j)⟧) : (⟦x⟧ : Game) = ⟦y⟧ :=
game_eq (.of_equiv L R (fun _ => equiv_iff_game_eq.2 (hl _)) (fun _ => equiv_iff_game_eq.2 (hr _)))
