-- Mathlib/SetTheory/Game/PGame.lean
theorem neg_add_cancel_le_zero : ∀ x : PGame, -x + x ≤ 0
  | ⟨xl, xr, xL, xR⟩ =>
    le_zero.2 fun i => by
      obtain i | i := i
      · -- If Left played in -x, Right responds with the same move in x.
        refine ⟨@toRightMovesAdd _ ⟨_, _, _, _⟩ (Sum.inr i), ?_⟩
        convert @neg_add_cancel_le_zero (xR i)
        apply add_moveRight_inr
      · -- If Left in x, Right responds with the same move in -x.
        dsimp
        refine ⟨@toRightMovesAdd ⟨_, _, _, _⟩ _ (Sum.inl i), ?_⟩
        convert @neg_add_cancel_le_zero (xL i)
        apply add_moveRight_inl

Proof state:
case h.e'_3
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
i : xr
⊢ ((-mk xl xr xL xR + mk xl xr xL xR).moveLeft (Sum.inl i)).moveRight (toRightMovesAdd (Sum.inr i)) = -xR i + xR i

Tactic:
apply add_moveRight_inr

Result:
no goals

Proof state:
case inr
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
i : xl
⊢ ∃ j, ((-mk xl xr xL xR + mk xl xr xL xR).moveLeft (Sum.inr i)).moveRight j ≤ 0

Tactic:
dsimp

Result:
case inr
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
i : xl
⊢ ∃ j, ((mk xr xl (fun x => -xR x) fun x => -xL x) + xL i).moveRight j ≤ 0

Proof state:
case inr
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
i : xl
⊢ ∃ j, ((mk xr xl (fun x => -xR x) fun x => -xL x) + xL i).moveRight j ≤ 0

Tactic:
refine ⟨@toRightMovesAdd ⟨_, _, _, _⟩ _ (Sum.inl i), ?_⟩

Result:
case inr
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
i : xl
⊢ ((mk xr xl (fun x => -xR x) fun x => -xL x) + xL i).moveRight (toRightMovesAdd (Sum.inl i)) ≤ 0

Proof state:
case inl
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
i : xr
⊢ ((-mk xl xr xL xR + mk xl xr xL xR).moveLeft (Sum.inl i)).moveRight (toRightMovesAdd (Sum.inr i)) ≤ 0

Tactic:
convert @neg_add_cancel_le_zero (xR i)

Result:
case h.e'_3
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
i : xr
⊢ ((-mk xl xr xL xR + mk xl xr xL xR).moveLeft (Sum.inl i)).moveRight (toRightMovesAdd (Sum.inr i)) = -xR i + xR i

Proof state:
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
i : (-mk xl xr xL xR + mk xl xr xL xR).LeftMoves
⊢ ∃ j, ((-mk xl xr xL xR + mk xl xr xL xR).moveLeft i).moveRight j ≤ 0

Tactic:
obtain i | i := i

Result:
case inl
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
i : xr
⊢ ∃ j, ((-mk xl xr xL xR + mk xl xr xL xR).moveLeft (Sum.inl i)).moveRight j ≤ 0

case inr
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
i : xl
⊢ ∃ j, ((-mk xl xr xL xR + mk xl xr xL xR).moveLeft (Sum.inr i)).moveRight j ≤ 0

Proof state:
case inl
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
i : xr
⊢ ∃ j, ((-mk xl xr xL xR + mk xl xr xL xR).moveLeft (Sum.inl i)).moveRight j ≤ 0

Tactic:
refine ⟨@toRightMovesAdd _ ⟨_, _, _, _⟩ (Sum.inr i), ?_⟩

Result:
case inl
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
i : xr
⊢ ((-mk xl xr xL xR + mk xl xr xL xR).moveLeft (Sum.inl i)).moveRight (toRightMovesAdd (Sum.inr i)) ≤ 0

Proof state:
case inr
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
i : xl
⊢ ((mk xr xl (fun x => -xR x) fun x => -xL x) + xL i).moveRight (toRightMovesAdd (Sum.inl i)) ≤ 0

Tactic:
convert @neg_add_cancel_le_zero (xL i)

Result:
case h.e'_3
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
i : xl
⊢ ((mk xr xl (fun x => -xR x) fun x => -xL x) + xL i).moveRight (toRightMovesAdd (Sum.inl i)) = -xL i + xL i

Proof state:
case h.e'_3
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
i : xl
⊢ ((mk xr xl (fun x => -xR x) fun x => -xL x) + xL i).moveRight (toRightMovesAdd (Sum.inl i)) = -xL i + xL i

Tactic:
apply add_moveRight_inl

Result:
no goals