-- Mathlib/SetTheory/Game/PGame.lean
/-- A new left option cannot hurt Left. -/
lemma le_insertLeft (x x' : PGame) : x ≤ insertLeft x x'

Proof state:
case left
x x' : PGame
i : x.LeftMoves
⊢ (∃ i', x.moveLeft i ≤ (x.insertLeft x').moveLeft i') ∨ ∃ j, (x.moveLeft i).moveRight j ≤ x.insertLeft x'

Tactic:
left

Result:
case left.h
x x' : PGame
i : x.LeftMoves
⊢ ∃ i', x.moveLeft i ≤ (x.insertLeft x').moveLeft i'

Proof state:
x x' : PGame
⊢ (∀ (i : x.LeftMoves),
      (∃ i', x.moveLeft i ≤ (x.insertLeft x').moveLeft i') ∨ ∃ j, (x.moveLeft i).moveRight j ≤ x.insertLeft x') ∧
    ∀ (j : (x.insertLeft x').RightMoves),
      (∃ i, x ≤ ((x.insertLeft x').moveRight j).moveLeft i) ∨ ∃ j', x.moveRight j' ≤ (x.insertLeft x').moveRight j

Tactic:
constructor

Result:
case left
x x' : PGame
⊢ ∀ (i : x.LeftMoves),
    (∃ i', x.moveLeft i ≤ (x.insertLeft x').moveLeft i') ∨ ∃ j, (x.moveLeft i).moveRight j ≤ x.insertLeft x'

case right
x x' : PGame
⊢ ∀ (j : (x.insertLeft x').RightMoves),
    (∃ i, x ≤ ((x.insertLeft x').moveRight j).moveLeft i) ∨ ∃ j', x.moveRight j' ≤ (x.insertLeft x').moveRight j

Proof state:
case left.h.mk.h
x' : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
i : (mk xl xr xL xR).LeftMoves
⊢ ∃ a, xL i ≤ xL a

Tactic:
use i

Result:
no goals

Proof state:
case left.h.mk
x' : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
i : (mk xl xr xL xR).LeftMoves
⊢ ∃ i', (mk xl xr xL xR).moveLeft i ≤ ((mk xl xr xL xR).insertLeft x').moveLeft i'

Tactic:
simp only [insertLeft, leftMoves_mk, moveLeft_mk, Sum.exists, Sum.elim_inl]

Result:
case left.h.mk
x' : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
i : (mk xl xr xL xR).LeftMoves
⊢ (∃ a, xL i ≤ xL a) ∨ ∃ b, xL i ≤ Sum.elim xL (fun x => x') (Sum.inr b)

Proof state:
case right.h
x x' : PGame
j : (x.insertLeft x').RightMoves
⊢ ∃ j', x.moveRight j' ≤ (x.insertLeft x').moveRight j

Tactic:
rcases x with ⟨xl, xr, xL, xR⟩

Result:
case right.h.mk
x' : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
j : ((mk xl xr xL xR).insertLeft x').RightMoves
⊢ ∃ j', (mk xl xr xL xR).moveRight j' ≤ ((mk xl xr xL xR).insertLeft x').moveRight j

Proof state:
case right.h.mk
x' : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
j : ((mk xl xr xL xR).insertLeft x').RightMoves
⊢ ∃ j', xR j' ≤ xR j

Tactic:
use j

Result:
no goals

Proof state:
case right.h.mk
x' : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
j : ((mk xl xr xL xR).insertLeft x').RightMoves
⊢ ∃ j', (mk xl xr xL xR).moveRight j' ≤ ((mk xl xr xL xR).insertLeft x').moveRight j

Tactic:
simp only [rightMoves_mk, moveRight_mk, insertLeft]

Result:
case right.h.mk
x' : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
j : ((mk xl xr xL xR).insertLeft x').RightMoves
⊢ ∃ j', xR j' ≤ xR j

Proof state:
x x' : PGame
⊢ x ≤ x.insertLeft x'

Tactic:
rw [le_def]

Result:
x x' : PGame
⊢ (∀ (i : x.LeftMoves),
      (∃ i', x.moveLeft i ≤ (x.insertLeft x').moveLeft i') ∨ ∃ j, (x.moveLeft i).moveRight j ≤ x.insertLeft x') ∧
    ∀ (j : (x.insertLeft x').RightMoves),
      (∃ i, x ≤ ((x.insertLeft x').moveRight j).moveLeft i) ∨ ∃ j', x.moveRight j' ≤ (x.insertLeft x').moveRight j

Proof state:
case left
x x' : PGame
⊢ ∀ (i : x.LeftMoves),
    (∃ i', x.moveLeft i ≤ (x.insertLeft x').moveLeft i') ∨ ∃ j, (x.moveLeft i).moveRight j ≤ x.insertLeft x'

Tactic:
intro i

Result:
case left
x x' : PGame
i : x.LeftMoves
⊢ (∃ i', x.moveLeft i ≤ (x.insertLeft x').moveLeft i') ∨ ∃ j, (x.moveLeft i).moveRight j ≤ x.insertLeft x'

Proof state:
case right
x x' : PGame
⊢ ∀ (j : (x.insertLeft x').RightMoves),
    (∃ i, x ≤ ((x.insertLeft x').moveRight j).moveLeft i) ∨ ∃ j', x.moveRight j' ≤ (x.insertLeft x').moveRight j

Tactic:
intro j

Result:
case right
x x' : PGame
j : (x.insertLeft x').RightMoves
⊢ (∃ i, x ≤ ((x.insertLeft x').moveRight j).moveLeft i) ∨ ∃ j', x.moveRight j' ≤ (x.insertLeft x').moveRight j

Proof state:
case right
x x' : PGame
j : (x.insertLeft x').RightMoves
⊢ (∃ i, x ≤ ((x.insertLeft x').moveRight j).moveLeft i) ∨ ∃ j', x.moveRight j' ≤ (x.insertLeft x').moveRight j

Tactic:
right

Result:
case right.h
x x' : PGame
j : (x.insertLeft x').RightMoves
⊢ ∃ j', x.moveRight j' ≤ (x.insertLeft x').moveRight j

Proof state:
case left.h.mk
x' : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
i : (mk xl xr xL xR).LeftMoves
⊢ (∃ a, xL i ≤ xL a) ∨ ∃ b, xL i ≤ Sum.elim xL (fun x => x') (Sum.inr b)

Tactic:
left

Result:
case left.h.mk.h
x' : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
i : (mk xl xr xL xR).LeftMoves
⊢ ∃ a, xL i ≤ xL a

Proof state:
case left.h
x x' : PGame
i : x.LeftMoves
⊢ ∃ i', x.moveLeft i ≤ (x.insertLeft x').moveLeft i'

Tactic:
rcases x with ⟨xl, xr, xL, xR⟩

Result:
case left.h.mk
x' : PGame
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
i : (mk xl xr xL xR).LeftMoves
⊢ ∃ i', (mk xl xr xL xR).moveLeft i ≤ ((mk xl xr xL xR).insertLeft x').moveLeft i'