English
A second form of the multiplicativity correspondence for toPGame, via a left-right move decomposition.
Русский
Вторая форма соответствия умножения кtoPGame через разложение ходов слева/справа.
LaTeX
$$(a ⨳ b).toPGame ≈ a.toPGame * b.toPGame$$
Lean4
/-- The natural multiplication of ordinals corresponds to their product as pre-games. -/
theorem toPGame_nmul (a b : Ordinal) : (a ⨳ b).toPGame ≈ a.toPGame * b.toPGame :=
by
refine ⟨le_of_forall_lf (fun i => ?_) isEmptyElim, le_of_forall_lf (fun i => ?_) isEmptyElim⟩
· rw [toPGame_moveLeft']
rcases lt_nmul_iff.1 (toLeftMovesToPGame_symm_lt i) with ⟨c, hc, d, hd, h⟩
rw [← toPGame_le_iff, le_iff_game_le, mk_toPGame, mk_toPGame, toGame_nadd _ _, toGame_nadd _ _, ←
le_sub_iff_add_le] at h
refine
lf_of_le_of_lf h <|
(lf_congr_left ?_).1 <|
moveLeft_lf <| toLeftMovesMul <| Sum.inl ⟨toLeftMovesToPGame ⟨c, hc⟩, toLeftMovesToPGame ⟨d, hd⟩⟩
simp only [mul_moveLeft_inl, toPGame_moveLeft', Equiv.symm_apply_apply, equiv_iff_game_eq, quot_sub, quot_add]
repeat rw [← game_eq (toPGame_nmul _ _)]
rfl
· apply leftMoves_mul_cases i _ isEmptyElim
intro i j
rw [mul_moveLeft_inl, toPGame_moveLeft', toPGame_moveLeft', lf_iff_game_lf, quot_sub, quot_add, ← Game.not_le,
le_sub_iff_add_le]
repeat rw [← game_eq (toPGame_nmul _ _)]
simp_rw [mk_toPGame, ← toGame_nadd]
apply toPGame_lf (nmul_nadd_lt _ _) <;> exact toLeftMovesToPGame_symm_lt _
termination_by (a, b)
