x y : PGame
⊢ ((¬∀ (i : LeftMoves y), moveLeft y i ⧏ x) ∨ ¬∀ (j : RightMoves x), y ⧏ moveRight x j) ↔
    (∃ i, x ≤ moveLeft y i) ∨ ∃ j, moveRight x j ≤ y
x y : PGame
⊢ x ⧏ y ↔ (∃ i, x ≤ moveLeft y i) ∨ ∃ j, moveRight x j ≤ y
rw [Lf, le_iff_forall_lf, not_and_or]
no goals
x y : PGame
⊢ ((¬∀ (i : LeftMoves y), moveLeft y i ⧏ x) ∨ ¬∀ (j : RightMoves x), y ⧏ moveRight x j) ↔
    (∃ i, x ≤ moveLeft y i) ∨ ∃ j, moveRight x j ≤ y
simp