English
The left-move structure of x*y is determined by the left options of x and y and by the left options of (-x)(-y) up to an equivalence relation.
Русский
Структура левых ходов произведения x·y определяется левыми опциями x и y и левыми опциями (-x)·(-y) до эквивалентности.
LaTeX
$$(∀ k, P ⟦(x * y).moveLeft k⟧) ⇔ (∀ i j, P ⟦mulOption x y i j⟧) ∧ (∀ i j, P ⟦mulOption (-x) (-y) i j⟧)$$
Lean4
/-- The left options of `x * y` of the second kind are the left options of `(-x) * (-y)` of the
first kind, up to equivalence. -/
theorem leftMoves_mul_iff {x y : PGame} (P : Game → Prop) :
(∀ k, P ⟦(x * y).moveLeft 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
· exact h (Sum.inl (i, j))
convert h (Sum.inr (i, j)) using 1
on_goal 2 =>
rintro (⟨i, j⟩ | ⟨i, j⟩)
· exact h.1 i j
convert h.2 i j using 1
all_goals
dsimp only [mk_mul_moveLeft_inr, quot_sub, quot_add, neg_def, mulOption, moveLeft_mk]
rw [← neg_def, ← neg_def]
congr 1
on_goal 1 => congr 1
all_goals rw [quot_neg_mul_neg]
