English
Left-mmove case analysis for the product: if P holds for all left-moves coming from the left factor and for all left-moves coming from the right factor, then P holds for k.
Русский
Анализ случаев левых ходов для произведения: если P истинно для всех левых ходов, полученных от левого множителя, и для всех левых ходов от правого множителя, то P верно для k.
LaTeX
$$$\forall x,y : PGame,\ (k) : (x * y).LeftMoves,\ (hl) : \forall ix,iy, P \big| toLeftMovesMul(\text{Sum.inl} \langle ix,iy\rangle \big),\ (hr) : \forall jx,jy, P \big| toLeftMovesMul(\text{Sum.inr} \langle jx,jy\rangle) \Rightarrow P(k)$$$
Lean4
theorem leftMoves_mul_cases {x y : PGame} (k) {P : (x * y).LeftMoves → Prop}
(hl : ∀ ix iy, P <| toLeftMovesMul (Sum.inl ⟨ix, iy⟩)) (hr : ∀ jx jy, P <| toLeftMovesMul (Sum.inr ⟨jx, jy⟩)) :
P k := by
rw [← toLeftMovesMul.apply_symm_apply k]
rcases toLeftMovesMul.symm k with (⟨ix, iy⟩ | ⟨jx, jy⟩)
· apply hl
· apply hr
