English
The birthday of a sum is the natural sum of birthdays: (x + y).birthday = x.birthday.nadd y.birthday.
Русский
Дни рождения суммы равны естественному суммированию дней рождения: (x + y).birthday = x.birthday.nadd y.birthday.
LaTeX
$$$ (x + y).birthday = x.birthday \;\\; y.birthday \\text{ with natural addition } nadd $$$
Lean4
@[simp]
theorem birthday_add : ∀ x y : PGame.{u}, (x + y).birthday = x.birthday ♯ y.birthday
| ⟨xl, xr, xL, xR⟩, ⟨yl, yr, yL, yR⟩ =>
by
rw [birthday_def, nadd, lsub_sum, lsub_sum]
simp only [mk_add_moveLeft_inl, mk_add_moveLeft_inr, mk_add_moveRight_inl, mk_add_moveRight_inr, moveLeft_mk,
moveRight_mk]
conv_lhs => left; left; right; intro a; rw [birthday_add (xL a) ⟨yl, yr, yL, yR⟩]
conv_lhs => left; right; right; intro b; rw [birthday_add ⟨xl, xr, xL, xR⟩ (yL b)]
conv_lhs => right; left; right; intro a; rw [birthday_add (xR a) ⟨yl, yr, yL, yR⟩]
conv_lhs => right; right; right; intro b; rw [birthday_add ⟨xl, xr, xL, xR⟩ (yR b)]
rw [max_max_max_comm]
congr <;> apply le_antisymm
any_goals
refine max_le_iff.2 ⟨?_, ?_⟩
all_goals
refine lsub_le_iff.2 fun i ↦ ?_
rw [← Order.succ_le_iff]
refine Ordinal.le_iSup (fun _ : Set.Iio _ ↦ _) ⟨_, ?_⟩
apply_rules [birthday_moveLeft_lt, birthday_moveRight_lt]
all_goals
rw [Ordinal.iSup_le_iff]
rintro ⟨i, hi⟩
obtain ⟨j, hj⟩ | ⟨j, hj⟩ := lt_birthday_iff.1 hi <;> rw [Order.succ_le_iff]
· exact lt_max_of_lt_left ((nadd_le_nadd_right hj _).trans_lt (lt_lsub _ _))
· exact lt_max_of_lt_right ((nadd_le_nadd_right hj _).trans_lt (lt_lsub _ _))
· exact lt_max_of_lt_left ((nadd_le_nadd_left hj _).trans_lt (lt_lsub _ _))
· exact lt_max_of_lt_right ((nadd_le_nadd_left hj _).trans_lt (lt_lsub _ _))
termination_by a b => (a, b)
