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