-- Mathlib/SetTheory/Game/Birthday.lean
theorem lt_birthday_iff {x : PGame} {o : Ordinal} :
    o < x.birthday ↔
      (∃ i : x.LeftMoves, o ≤ (x.moveLeft i).birthday) ∨
        ∃ i : x.RightMoves, o ≤ (x.moveRight i).birthday

Proof state:
case mp
x : PGame
o : Ordinal.{u_1}
h : o < (lsub fun i => (x.moveLeft i).birthday) ⊔ lsub fun i => (x.moveRight i).birthday
⊢ (∃ i, o ≤ (x.moveLeft i).birthday) ∨ ∃ i, o ≤ (x.moveRight i).birthday

Tactic:
rcases lt_max_iff.1 h with h' | h'

Result:
case mp.inl
x : PGame
o : Ordinal.{u_1}
h : o < (lsub fun i => (x.moveLeft i).birthday) ⊔ lsub fun i => (x.moveRight i).birthday
h' : o < lsub fun i => (x.moveLeft i).birthday
⊢ (∃ i, o ≤ (x.moveLeft i).birthday) ∨ ∃ i, o ≤ (x.moveRight i).birthday

case mp.inr
x : PGame
o : Ordinal.{u_1}
h : o < (lsub fun i => (x.moveLeft i).birthday) ⊔ lsub fun i => (x.moveRight i).birthday
h' : o < lsub fun i => (x.moveRight i).birthday
⊢ (∃ i, o ≤ (x.moveLeft i).birthday) ∨ ∃ i, o ≤ (x.moveRight i).birthday

Proof state:
case mp.inr.h
x : PGame
o : Ordinal.{u_1}
h : o < (lsub fun i => (x.moveLeft i).birthday) ⊔ lsub fun i => (x.moveRight i).birthday
h' : o < lsub fun i => (x.moveRight i).birthday
⊢ ∃ i, o ≤ (x.moveRight i).birthday

Tactic:
rwa [lt_lsub_iff] at h'

Result:
no goals

Proof state:
case mp.inr
x : PGame
o : Ordinal.{u_1}
h : o < (lsub fun i => (x.moveLeft i).birthday) ⊔ lsub fun i => (x.moveRight i).birthday
h' : o < lsub fun i => (x.moveRight i).birthday
⊢ (∃ i, o ≤ (x.moveLeft i).birthday) ∨ ∃ i, o ≤ (x.moveRight i).birthday

Tactic:
right

Result:
case mp.inr.h
x : PGame
o : Ordinal.{u_1}
h : o < (lsub fun i => (x.moveLeft i).birthday) ⊔ lsub fun i => (x.moveRight i).birthday
h' : o < lsub fun i => (x.moveRight i).birthday
⊢ ∃ i, o ≤ (x.moveRight i).birthday

Proof state:
case mp.inl
x : PGame
o : Ordinal.{u_1}
h : o < (lsub fun i => (x.moveLeft i).birthday) ⊔ lsub fun i => (x.moveRight i).birthday
h' : o < lsub fun i => (x.moveLeft i).birthday
⊢ (∃ i, o ≤ (x.moveLeft i).birthday) ∨ ∃ i, o ≤ (x.moveRight i).birthday

Tactic:
left

Result:
case mp.inl.h
x : PGame
o : Ordinal.{u_1}
h : o < (lsub fun i => (x.moveLeft i).birthday) ⊔ lsub fun i => (x.moveRight i).birthday
h' : o < lsub fun i => (x.moveLeft i).birthday
⊢ ∃ i, o ≤ (x.moveLeft i).birthday

Proof state:
case mpr.inl.intro
x : PGame
o : Ordinal.{u_1}
i : x.LeftMoves
hi : o ≤ (x.moveLeft i).birthday
⊢ o < x.birthday

Tactic:
exact hi.trans_lt (birthday_moveLeft_lt i)

Result:
no goals

Proof state:
x : PGame
o : Ordinal.{u_1}
⊢ o < x.birthday ↔ (∃ i, o ≤ (x.moveLeft i).birthday) ∨ ∃ i, o ≤ (x.moveRight i).birthday

Tactic:
constructor

Result:
case mp
x : PGame
o : Ordinal.{u_1}
⊢ o < x.birthday → (∃ i, o ≤ (x.moveLeft i).birthday) ∨ ∃ i, o ≤ (x.moveRight i).birthday

case mpr
x : PGame
o : Ordinal.{u_1}
⊢ ((∃ i, o ≤ (x.moveLeft i).birthday) ∨ ∃ i, o ≤ (x.moveRight i).birthday) → o < x.birthday

Proof state:
case mp.inl.h
x : PGame
o : Ordinal.{u_1}
h : o < (lsub fun i => (x.moveLeft i).birthday) ⊔ lsub fun i => (x.moveRight i).birthday
h' : o < lsub fun i => (x.moveLeft i).birthday
⊢ ∃ i, o ≤ (x.moveLeft i).birthday

Tactic:
rwa [lt_lsub_iff] at h'

Result:
no goals

Proof state:
case mp
x : PGame
o : Ordinal.{u_1}
⊢ o < x.birthday → (∃ i, o ≤ (x.moveLeft i).birthday) ∨ ∃ i, o ≤ (x.moveRight i).birthday

Tactic:
rw [birthday_def]

Result:
case mp
x : PGame
o : Ordinal.{u_1}
⊢ (o < (lsub fun i => (x.moveLeft i).birthday) ⊔ lsub fun i => (x.moveRight i).birthday) →
    (∃ i, o ≤ (x.moveLeft i).birthday) ∨ ∃ i, o ≤ (x.moveRight i).birthday

Proof state:
case mp
x : PGame
o : Ordinal.{u_1}
⊢ (o < (lsub fun i => (x.moveLeft i).birthday) ⊔ lsub fun i => (x.moveRight i).birthday) →
    (∃ i, o ≤ (x.moveLeft i).birthday) ∨ ∃ i, o ≤ (x.moveRight i).birthday

Tactic:
intro h

Result:
case mp
x : PGame
o : Ordinal.{u_1}
h : o < (lsub fun i => (x.moveLeft i).birthday) ⊔ lsub fun i => (x.moveRight i).birthday
⊢ (∃ i, o ≤ (x.moveLeft i).birthday) ∨ ∃ i, o ≤ (x.moveRight i).birthday

Proof state:
case mpr.inr.intro
x : PGame
o : Ordinal.{u_1}
i : x.RightMoves
hi : o ≤ (x.moveRight i).birthday
⊢ o < x.birthday

Tactic:
exact hi.trans_lt (birthday_moveRight_lt i)

Result:
no goals

Proof state:
case mpr
x : PGame
o : Ordinal.{u_1}
⊢ ((∃ i, o ≤ (x.moveLeft i).birthday) ∨ ∃ i, o ≤ (x.moveRight i).birthday) → o < x.birthday

Tactic:
rintro (⟨i, hi⟩ | ⟨i, hi⟩)

Result:
case mpr.inl.intro
x : PGame
o : Ordinal.{u_1}
i : x.LeftMoves
hi : o ≤ (x.moveLeft i).birthday
⊢ o < x.birthday

case mpr.inr.intro
x : PGame
o : Ordinal.{u_1}
i : x.RightMoves
hi : o ≤ (x.moveRight i).birthday
⊢ o < x.birthday