x : PGame
⊢ ((∀ (i : LeftMoves 0), (∃ i', moveLeft 0 i ≤ moveLeft x i') ∨ ∃ j, moveRight (moveLeft 0 i) j ≤ x) ∧
      ∀ (j : RightMoves x), (∃ i, 0 ≤ moveLeft (moveRight x j) i) ∨ ∃ j', moveRight 0 j' ≤ moveRight x j) ↔
    ∀ (j : RightMoves x), ∃ i, 0 ≤ moveLeft (moveRight x j) i
x : PGame
⊢ 0 ≤ x ↔ ∀ (j : RightMoves x), ∃ i, 0 ≤ moveLeft (moveRight x j) i
rw [le_def]
no goals
x : PGame
⊢ ((∀ (i : LeftMoves 0), (∃ i', moveLeft 0 i ≤ moveLeft x i') ∨ ∃ j, moveRight (moveLeft 0 i) j ≤ x) ∧
      ∀ (j : RightMoves x), (∃ i, 0 ≤ moveLeft (moveRight x j) i) ∨ ∃ j', moveRight 0 j' ≤ moveRight x j) ↔
    ∀ (j : RightMoves x), ∃ i, 0 ≤ moveLeft (moveRight x j) i
simp