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

case inr
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
i : xl
⊢ ∃ j, moveRight (moveLeft (-mk xl xr xL xR + mk xl xr xL xR) (Sum.inr i)) j ≤ 0
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
i : LeftMoves (-mk xl xr xL xR + mk xl xr xL xR)
⊢ ∃ j, moveRight (moveLeft (-mk xl xr xL xR + mk xl xr xL xR) i) j ≤ 0
cases' i with i i
case inl
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
i : xr
⊢ moveRight (moveLeft (-mk xl xr xL xR + mk xl xr xL xR) (Sum.inl i)) (↑toRightMovesAdd (Sum.inr i)) ≤ 0
case inl
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
i : xr
⊢ ∃ j, moveRight (moveLeft (-mk xl xr xL xR + mk xl xr xL xR) (Sum.inl i)) j ≤ 0
refine' ⟨@toRightMovesAdd _ ⟨_, _, _, _⟩ (Sum.inr i), _⟩
case h.e'_3
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
i : xr
⊢ moveRight (moveLeft (-mk xl xr xL xR + mk xl xr xL xR) (Sum.inl i)) (↑toRightMovesAdd (Sum.inr i)) = -xR i + xR i
case inl
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
i : xr
⊢ moveRight (moveLeft (-mk xl xr xL xR + mk xl xr xL xR) (Sum.inl i)) (↑toRightMovesAdd (Sum.inr i)) ≤ 0
convert @add_left_neg_le_zero (xR i)
no goals
case h.e'_3
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
i : xr
⊢ moveRight (moveLeft (-mk xl xr xL xR + mk xl xr xL xR) (Sum.inl i)) (↑toRightMovesAdd (Sum.inr i)) = -xR i + xR i
apply add_moveRight_inr
case inr
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
i : xl
⊢ ∃ j, moveRight ((mk xr xl (fun j => -xR j) fun i => -xL i) + xL i) j ≤ 0
case inr
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
i : xl
⊢ ∃ j, moveRight (moveLeft (-mk xl xr xL xR + mk xl xr xL xR) (Sum.inr i)) j ≤ 0
dsimp
case inr
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
i : xl
⊢ moveRight ((mk xr xl (fun j => -xR j) fun i => -xL i) + xL i) (↑toRightMovesAdd (Sum.inl i)) ≤ 0
case inr
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
i : xl
⊢ ∃ j, moveRight ((mk xr xl (fun j => -xR j) fun i => -xL i) + xL i) j ≤ 0
refine' ⟨@toRightMovesAdd ⟨_, _, _, _⟩ _ (Sum.inl i), _⟩
case h.e'_3
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
i : xl
⊢ moveRight ((mk xr xl (fun j => -xR j) fun i => -xL i) + xL i) (↑toRightMovesAdd (Sum.inl i)) = -xL i + xL i
case inr
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
i : xl
⊢ moveRight ((mk xr xl (fun j => -xR j) fun i => -xL i) + xL i) (↑toRightMovesAdd (Sum.inl i)) ≤ 0
convert @add_left_neg_le_zero (xL i)
no goals
case h.e'_3
xl xr : Type u_1
xL : xl → PGame
xR : xr → PGame
i : xl
⊢ moveRight ((mk xr xl (fun j => -xR j) fun i => -xL i) + xL i) (↑toRightMovesAdd (Sum.inl i)) = -xL i + xL i
apply add_moveRight_inl