English
To determine a property P on a right move k of x+y it suffices to verify P on all right moves arising from x and from y; i.e., knowing P on toRightMovesAdd(Sum.inl j) for all j in x.RightMoves and on toRightMovesAdd(Sum.inr j) for all j in y.RightMoves implies P(k) for all k.
Русский
Чтобы установить свойство P для правого хода k суммы x+y, достаточно проверить P на все правые ходы из x и из y; если P выполняется на toRightMovesAdd(Sum.inl j) для всех j из x.RightMoves и на toRightMovesAdd(Sum.inr j) для всех j из y.RightMoves, то P выполняется для всех k.
LaTeX
$$$ \forall k:(x+y).RightMoves,\; P(k) \\Leftarrow (\forall j: x.RightMoves, P(\mathrm{toRightMovesAdd}(\mathrm{Sum.inl} j))) \\quad\land\\ forall j: y.RightMoves, P(\mathrm{toRightMovesAdd}(\mathrm{Sum.inr} j)))$$
Lean4
/-- Case on possible right moves of `x + y`. -/
theorem rightMoves_add_cases {x y : PGame} (k) {P : (x + y).RightMoves → Prop}
(hl : ∀ j, P <| toRightMovesAdd (Sum.inl j)) (hr : ∀ j, P <| toRightMovesAdd (Sum.inr j)) : P k :=
by
rw [← toRightMovesAdd.apply_symm_apply k]
rcases toRightMovesAdd.symm k with i | i
· exact hl i
· exact hr i
