feat(set_theory/game/birthday): More basic birthdays (#14287)

leanprover-community · May 22, 2022 · d8b6f76 · d8b6f76
1 parent f04684f
commit d8b6f76
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 6 deletions.
diff --git a/src/set_theory/game/birthday.lean b/src/set_theory/game/birthday.lean
@@ -101,13 +101,16 @@ using_well_founded { dec_tac := pgame_wf_tac }
 by rw [birthday_def, max_eq_zero, lsub_eq_zero_iff, lsub_eq_zero_iff]
 
 @[simp] theorem birthday_zero : birthday 0 = 0 :=
-by { rw birthday_eq_zero, split; apply_instance }
+by simp [pempty.is_empty]
 
 @[simp] theorem birthday_one : birthday 1 = 1 :=
-begin
-  have : (λ i, (move_left 1 i).birthday) = λ i, 0 := funext (λ x, by simp),
-  rw [birthday_def, @lsub_empty (right_moves 1), this, lsub_const, succ_zero, max_zero_right]
-end
+by { rw birthday_def, simp }
+
+@[simp] theorem birthday_star : birthday star = 1 :=
+by { rw birthday_def, simp }
+
+@[simp] theorem birthday_half : birthday half = 2 :=
+by { rw birthday_def, simpa using max_eq_right (lt_succ_self 1).le }
 
 @[simp] theorem neg_birthday : ∀ x : pgame, (-x).birthday = x.birthday
 | ⟨xl, xr, xL, xR⟩ := begin
@@ -119,7 +122,7 @@ end
 begin
   induction o using ordinal.induction with o IH,
   rw [to_pgame_def, pgame.birthday],
-  convert max_eq_left_iff.2 (ordinal.zero_le _),
+  convert max_eq_left (ordinal.zero_le _),
   { apply lsub_empty },
   { nth_rewrite 0 ←lsub_typein o,
     congr,

diff --git a/src/set_theory/ordinal/arithmetic.lean b/src/set_theory/ordinal/arithmetic.lean
@@ -99,6 +99,7 @@ theorem add_succ (o₁ o₂ : ordinal) : o₁ + succ o₂ = succ (o₁ + o₂) :
 (add_assoc _ _ _).symm
 
 @[simp] theorem succ_zero : succ 0 = 1 := zero_add _
+@[simp] theorem succ_one : succ 1 = 2 := rfl
 
 theorem one_le_iff_pos {o : ordinal} : 1 ≤ o ↔ 0 < o :=
 by rw [← succ_zero, succ_le]