English
For i ∈ x.RightMoves and j ∈ y.LeftMoves, the left move of the product x*y with the inr index equals x.moveRight i times y plus x times y.moveLeft j minus x.moveRight i times y.moveLeft j.
Русский
Для i ∈ x.RightMoves и j ∈ y.LeftMoves левый ход произведения x*y, соответствующий inr, равен x.moveRight(i)·y + x·y.moveLeft(j) − x.moveRight(i)·y.moveLeft(j).
LaTeX
$$$$(x * y).moveLeft(\\mathrm{toLeftMovesMul}(\\mathrm{Sum.inr}(i,j))) = x.moveRight(i) * y + x * y.moveLeft(j) - x.moveRight(i) * y.moveLeft(j)$$$$
Lean4
@[simp]
theorem mul_moveLeft_inr {x y : PGame} {i j} :
(x * y).moveLeft (toLeftMovesMul (Sum.inr (i, j))) =
x.moveRight i * y + x * y.moveRight j - x.moveRight i * y.moveRight j :=
by
cases x
cases y
rfl
