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