feat(set_theory/game/basic): mul_cases lemmas (#14343)

These are the multiplicative analogs for `{left/right}_moves_add_cases`.

Author: vihdzp

src/set_theory/game/basic.lean

@@ -218,6 +218,26 @@ rfl
    = x.move_right i * y + x * y.move_left j - x.move_right i * y.move_left j :=
 by { cases x, cases y, refl }
 
+lemma left_moves_mul_cases {x y : pgame} (k : (x * y).left_moves) :
+  (∃ ix iy, k = to_left_moves_mul (sum.inl ⟨ix, iy⟩)) ∨
+  ∃ jx jy, k = to_left_moves_mul (sum.inr ⟨jx, jy⟩) :=
+begin
+  rw ←to_left_moves_mul.apply_symm_apply k,
+  rcases to_left_moves_mul.symm k with ⟨ix, iy⟩ | ⟨jx, jy⟩,
+  { exact or.inl ⟨ix, iy, rfl⟩ },
+  { exact or.inr ⟨jx, jy, rfl⟩ }
+end
+
+lemma right_moves_mul_cases {x y : pgame} (k : (x * y).right_moves) :
+  (∃ ix jy, k = to_right_moves_mul (sum.inl ⟨ix, jy⟩)) ∨
+  ∃ jx iy, k = to_right_moves_mul (sum.inr ⟨jx, iy⟩) :=
+begin
+  rw ←to_right_moves_mul.apply_symm_apply k,
+  rcases to_right_moves_mul.symm k with ⟨ix, jy⟩ | ⟨jx, iy⟩,
+  { exact or.inl ⟨ix, jy, rfl⟩ },
+  { exact or.inr ⟨jx, iy, rfl⟩ }
+end
+
 theorem quot_mul_comm : Π (x y : pgame.{u}), ⟦x * y⟧ = ⟦y * x⟧
 | (mk xl xr xL xR) (mk yl yr yL yR) :=
 begin