English
The right-move structure of x*y corresponds to the left moves of x*(-y) and of (-x)*y, up to equivalence.
Русский
Структура правых ходов x·y соответствует левых ходам x·(-y) и (-x)·y до эквивалентности.
LaTeX
$$(∀ k, P ⟦(x * y).moveRight k⟧) ⇔ (∀ i j, P (-⟦mulOption x (-y) i j⟧)) ∧ (∀ i j, P (-⟦mulOption (-x) y i j⟧))$$
Lean4
/-- The right options of `x * y` are the left options of `x * (-y)` and of `(-x) * y` of the first
kind, up to equivalence. -/
theorem rightMoves_mul_iff {x y : PGame} (P : Game → Prop) :
(∀ k, P ⟦(x * y).moveRight k⟧) ↔ (∀ i j, P (-⟦mulOption x (-y) i j⟧)) ∧ (∀ i j, P (-⟦mulOption (-x) y i j⟧)) :=
by
cases x; cases y
constructor <;> intro h
on_goal 1 =>
constructor <;> intro i j
on_goal 1 => convert h (Sum.inl (i, j))
on_goal 2 => convert h (Sum.inr (i, j))
on_goal 3 =>
rintro (⟨i, j⟩ | ⟨i, j⟩)
on_goal 1 => convert h.1 i j using 1
on_goal 2 => convert h.2 i j using 1
all_goals
dsimp [mulOption]
rw [neg_sub', neg_add, ← neg_def]
congr 1
on_goal 1 => congr 1
any_goals rw [quot_neg_mul, neg_neg]
iterate 6 rw [quot_mul_neg, neg_neg]
