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