English
If k is a right move of x*y, then k arises from either the left-inl or left-inr decomposition of the right moves; i.e., each right move originates from one of the two corresponding structured sources.
Русский
Если k является правым ходом x*y, то он возникает либо из разложения правых ходов слева, либо из разложения справа слева; то есть каждый правый ход исходит из одного из двух структурированных источников.
LaTeX
$$$$k \\in (x*y).RightMoves \\Rightarrow (\\exists i,j\\, k = toRightMovesMul(\\mathrm{Sum.inl}(i,j)) \\,\\lor\\, \\exists jx, jy\\, k = toRightMovesMul(\\mathrm{Sum.inr}(jx,jy))).$$$$
Lean4
theorem rightMoves_mul_cases {x y : PGame} (k) {P : (x * y).RightMoves → Prop}
(hl : ∀ ix jy, P <| toRightMovesMul (Sum.inl ⟨ix, jy⟩)) (hr : ∀ jx iy, P <| toRightMovesMul (Sum.inr ⟨jx, iy⟩)) :
P k := by
rw [← toRightMovesMul.apply_symm_apply k]
rcases toRightMovesMul.symm k with (⟨ix, iy⟩ | ⟨jx, jy⟩)
· apply hl
· apply hr
