-- 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
xl xr : Type u
xL : xl → PGame
xR : xr → PGame
yl yr : Type u
yL : yl → PGame
yR : yr → PGame
⊢ ∀ (i : ↑(Set.Iio (mk yl yr yL yR).birthday)),
    Order.succ ((mk xl xr xL xR).birthday ♯ ↑i) ≤
      (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:
rintro ⟨i, hi⟩

Result:
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

Proof state:
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)

Tactic:
refine max_le_iff.2 ⟨?_, ?_⟩

Result:
case e_a.a.refine_1
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) ≤ ⨆ x, Order.succ ((mk xl xr xL xR).birthday ♯ ↑x)

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
⊢ (lsub fun b => (mk xl xr xL xR).birthday ♯ (yR b).birthday) ≤ ⨆ x, Order.succ ((mk xl xr xL xR).birthday ♯ ↑x)

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 b => (mk xl xr xL xR).birthday ♯ (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)

Tactic:
conv_lhs => right; left; right; intro a; rw [birthday_add (xR a) ⟨yl, yr, yL, yR⟩]

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).birthday ♯ (mk yl yr yL yR).birthday) ⊔
        lsub fun b => (mk xl xr xL xR).birthday ♯ (yL b).birthday) ⊔
      ((lsub fun a => (xR a).birthday ♯ (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)

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
⊢ (lsub fun b => (mk xl xr xL xR).birthday ♯ (yR b).birthday) ≤ ⨆ x, Order.succ ((mk xl xr xL xR).birthday ♯ ↑x)

Tactic:
refine lsub_le_iff.2 fun i ↦ ?_

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
⊢ (mk xl xr xL xR).birthday ♯ (yR i).birthday < ⨆ x, Order.succ ((mk xl xr xL xR).birthday ♯ ↑x)

Proof state:
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

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

Result:
no goals

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 b => (mk xl xr xL xR).birthday ♯ (yL b).birthday) ⊔
      ((lsub fun a => (xR a).birthday ♯ (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)

Tactic:
conv_lhs => right; right; right; intro b; rw [birthday_add ⟨xl, xr, xL, xR⟩ (yR b)]

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).birthday ♯ (mk yl yr yL yR).birthday) ⊔
        lsub fun b => (mk xl xr xL xR).birthday ♯ (yL b).birthday) ⊔
      ((lsub fun a => (xR a).birthday ♯ (mk yl yr yL yR).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)

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 b => (mk xl xr xL xR).birthday ♯ (yL b).birthday) ⊔
      ((lsub fun a => (xR a).birthday ♯ (mk yl yr yL yR).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:
rw [max_max_max_comm]

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).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)

Proof state:
case e_a.a.refine_1
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) ≤ ⨆ x, Order.succ ((mk xl xr xL xR).birthday ♯ ↑x)

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
⊢ (lsub fun b => (mk xl xr xL xR).birthday ♯ (yR b).birthday) ≤ ⨆ x, Order.succ ((mk xl xr xL xR).birthday ♯ ↑x)

Tactic:
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]

Result:
no goals