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