x y : PGame
⊢ ((∀ (i : LeftMoves x), moveLeft x i ⧏ y) ∧ ∀ (j : RightMoves y), x ⧏ moveRight y j) ↔
    (∀ (i : LeftMoves x), (∃ i', moveLeft x i ≤ moveLeft y i') ∨ ∃ j, moveRight (moveLeft x i) j ≤ y) ∧
      ∀ (j : RightMoves y), (∃ i, x ≤ moveLeft (moveRight y j) i) ∨ ∃ j', moveRight x j' ≤ moveRight y j
x y : PGame
⊢ x ≤ y ↔
    (∀ (i : LeftMoves x), (∃ i', moveLeft x i ≤ moveLeft y i') ∨ ∃ j, moveRight (moveLeft x i) j ≤ y) ∧
      ∀ (j : RightMoves y), (∃ i, x ≤ moveLeft (moveRight y j) i) ∨ ∃ j', moveRight x j' ≤ moveRight y j
rw [le_iff_forall_lf]
no goals
x y : PGame
⊢ ((∀ (i : LeftMoves x), moveLeft x i ⧏ y) ∧ ∀ (j : RightMoves y), x ⧏ moveRight y j) ↔
    (∀ (i : LeftMoves x), (∃ i', moveLeft x i ≤ moveLeft y i') ∨ ∃ j, moveRight (moveLeft x i) j ≤ y) ∧
      ∀ (j : RightMoves y), (∃ i, x ≤ moveLeft (moveRight y j) i) ∨ ∃ j', moveRight x j' ≤ moveRight y j
conv =>
  lhs
  simp only [lf_iff_exists_le]