-- Mathlib/SetTheory/Game/Birthday.lean
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)

Proof state:
case e_a.a.mk.inl.intro
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
i : Ordinal.{u}
hi : i ∈ Set.Iio (mk yl yr yL yR).birthday
j : (mk yl yr yL yR).LeftMoves
hj : i ≤ ((mk yl yr yL yR).moveLeft j).birthday
⊢ (mk xl xr xL xR).birthday ♯ ↑⟨i, hi⟩ <
    (lsub fun b => (mk xl xr xL xR).birthday ♯ (yL b).birthday) ⊔
      lsub fun b => (mk xl xr xL xR).birthday ♯ (yR b).birthday

Tactic:
exact lt_max_of_lt_left ((nadd_le_nadd_left hj _).trans_lt (lt_lsub _ _))

Result:
no goals

Proof state:
case e_a.a.refine_2
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
i : yr
⊢ (yR i).birthday ∈ Set.Iio (mk yl yr yL yR).birthday

Tactic:
apply_rules [birthday_moveLeft_lt, birthday_moveRight_lt]

Result:
no goals

Proof state:
case e_a.a.mk
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
i : Ordinal.{u}
hi : i ∈ Set.Iio (mk yl yr yL yR).birthday
⊢ Order.succ ((mk xl xr xL xR).birthday ♯ ↑⟨i, hi⟩) ≤
    (lsub fun b => (mk xl xr xL xR).birthday ♯ (yL b).birthday) ⊔
      lsub fun b => (mk xl xr xL xR).birthday ♯ (yR b).birthday

Tactic:
obtain ⟨j, hj⟩ | ⟨j, hj⟩ := lt_birthday_iff.1 hi <;> rw [Order.succ_le_iff]

Result:
case e_a.a.mk.inl.intro
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
i : Ordinal.{u}
hi : i ∈ Set.Iio (mk yl yr yL yR).birthday
j : (mk yl yr yL yR).LeftMoves
hj : i ≤ ((mk yl yr yL yR).moveLeft j).birthday
⊢ (mk xl xr xL xR).birthday ♯ ↑⟨i, hi⟩ <
    (lsub fun b => (mk xl xr xL xR).birthday ♯ (yL b).birthday) ⊔
      lsub fun b => (mk xl xr xL xR).birthday ♯ (yR b).birthday

case e_a.a.mk.inr.intro
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
i : Ordinal.{u}
hi : i ∈ Set.Iio (mk yl yr yL yR).birthday
j : (mk yl yr yL yR).RightMoves
hj : i ≤ ((mk yl yr yL yR).moveRight j).birthday
⊢ (mk xl xr xL xR).birthday ♯ ↑⟨i, hi⟩ <
    (lsub fun b => (mk xl xr xL xR).birthday ♯ (yL b).birthday) ⊔
      lsub fun b => (mk xl xr xL xR).birthday ♯ (yR b).birthday

Proof state:
case e_a.a.refine_2
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
i : yr
⊢ Order.succ ((mk xl xr xL xR).birthday ♯ (yR i).birthday) ≤ ⨆ x, Order.succ ((mk xl xr xL xR).birthday ♯ ↑x)

Tactic:
refine Ordinal.le_iSup (fun _ : Set.Iio _ ↦ _) ⟨_, ?_⟩

Result:
case e_a.a.refine_2
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
i : yr
⊢ (yR i).birthday ∈ Set.Iio (mk yl yr yL yR).birthday

Proof state:
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ ((lsub fun a => (xL a).birthday ♯ (mk yl yr yL yR).birthday) ⊔
        lsub fun a => (xR a).birthday ♯ (mk yl yr yL yR).birthday) ⊔
      ((lsub fun b => (mk xl xr xL xR).birthday ♯ (yL b).birthday) ⊔
        lsub fun b => (mk xl xr xL xR).birthday ♯ (yR b).birthday) =
    (⨆ x, Order.succ (↑x ♯ (mk yl yr yL yR).birthday)) ⊔ ⨆ x, Order.succ ((mk xl xr xL xR).birthday ♯ ↑x)

Tactic:
congr <;> apply le_antisymm

Result:
case e_a.a
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ ((lsub fun a => (xL a).birthday ♯ (mk yl yr yL yR).birthday) ⊔
      lsub fun a => (xR a).birthday ♯ (mk yl yr yL yR).birthday) ≤
    ⨆ x, Order.succ (↑x ♯ (mk yl yr yL yR).birthday)

case e_a.a
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ ⨆ x, Order.succ (↑x ♯ (mk yl yr yL yR).birthday) ≤
    (lsub fun a => (xL a).birthday ♯ (mk yl yr yL yR).birthday) ⊔
      lsub fun a => (xR a).birthday ♯ (mk yl yr yL yR).birthday

case e_a.a
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ ((lsub fun b => (mk xl xr xL xR).birthday ♯ (yL b).birthday) ⊔
      lsub fun b => (mk xl xr xL xR).birthday ♯ (yR b).birthday) ≤
    ⨆ x, Order.succ ((mk xl xr xL xR).birthday ♯ ↑x)

case e_a.a
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ ⨆ x, Order.succ ((mk xl xr xL xR).birthday ♯ ↑x) ≤
    (lsub fun b => (mk xl xr xL xR).birthday ♯ (yL b).birthday) ⊔
      lsub fun b => (mk xl xr xL xR).birthday ♯ (yR b).birthday

Proof state:
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ ((lsub fun a => ((mk xl xr xL xR + mk yl yr yL yR).moveLeft (Sum.inl a)).birthday) ⊔
        lsub fun b => ((mk xl xr xL xR + mk yl yr yL yR).moveLeft (Sum.inr b)).birthday) ⊔
      ((lsub fun a => ((mk xl xr xL xR + mk yl yr yL yR).moveRight (Sum.inl a)).birthday) ⊔
        lsub fun b => ((mk xl xr xL xR + mk yl yr yL yR).moveRight (Sum.inr b)).birthday) =
    (⨆ x, Order.succ (↑x ♯ (mk yl yr yL yR).birthday)) ⊔ ⨆ x, Order.succ ((mk xl xr xL xR).birthday ♯ ↑x)

Tactic:
simp only [mk_add_moveLeft_inl, mk_add_moveLeft_inr, mk_add_moveRight_inl, mk_add_moveRight_inr,
  moveLeft_mk, moveRight_mk]

Result:
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ ((lsub fun a => (xL a + mk yl yr yL yR).birthday) ⊔ lsub fun b => (mk xl xr xL xR + yL b).birthday) ⊔
      ((lsub fun a => (xR a + mk yl yr yL yR).birthday) ⊔ lsub fun b => (mk xl xr xL xR + yR b).birthday) =
    (⨆ x, Order.succ (↑x ♯ (mk yl yr yL yR).birthday)) ⊔ ⨆ x, Order.succ ((mk xl xr xL xR).birthday ♯ ↑x)