English
For i ∈ x.RightMoves and j ∈ y.RightMoves, the right move of the product x*y with the toRightMovesMul (Sum.inr (i, j)) 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.RightMoves правый ход произведения x*y, соответствующий Sum.inr, равен x.moveRight(i)·y + x·y.moveLeft(j) − x.moveRight(i)·y.moveLeft(j).
LaTeX
$$$$(x * y).moveRight(\\mathrm{toRightMovesMul}(\\mathrm{Sum.inr}(i,j))) = x.moveRight(i) * y + x * y.moveLeft(j) - x.moveRight(i) * y.moveLeft(j)$$$$
Lean4
@[simp]
theorem mul_moveRight_inr {x y : PGame} {i j} :
(x * y).moveRight (toRightMovesMul (Sum.inr (i, j))) =
x.moveRight i * y + x * y.moveLeft j - x.moveRight i * y.moveLeft j :=
by
cases x
cases y
rfl
