case left
x y : PGame
L : LeftMoves x ≃ LeftMoves y
R : RightMoves x ≃ RightMoves y
hl : ∀ (i : LeftMoves x), moveLeft x i ≈ moveLeft y (↑L i)
hr : ∀ (j : RightMoves x), moveRight x j ≈ moveRight y (↑R 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

case right
x y : PGame
L : LeftMoves x ≃ LeftMoves y
R : RightMoves x ≃ RightMoves y
hl : ∀ (i : LeftMoves x), moveLeft x i ≈ moveLeft y (↑L i)
hr : ∀ (j : RightMoves x), moveRight x j ≈ moveRight y (↑R j)
⊢ (∀ (i : LeftMoves y), (∃ i', moveLeft y i ≤ moveLeft x i') ∨ ∃ j, moveRight (moveLeft y i) j ≤ x) ∧
    ∀ (j : RightMoves x), (∃ i, y ≤ moveLeft (moveRight x j) i) ∨ ∃ j', moveRight y j' ≤ moveRight x j
x y : PGame
L : LeftMoves x ≃ LeftMoves y
R : RightMoves x ≃ RightMoves y
hl : ∀ (i : LeftMoves x), moveLeft x i ≈ moveLeft y (↑L i)
hr : ∀ (j : RightMoves x), moveRight x j ≈ moveRight y (↑R j)
⊢ x ≈ y
constructor <;> rw [le_def]
no goals
case left
x y : PGame
L : LeftMoves x ≃ LeftMoves y
R : RightMoves x ≃ RightMoves y
hl : ∀ (i : LeftMoves x), moveLeft x i ≈ moveLeft y (↑L i)
hr : ∀ (j : RightMoves x), moveRight x j ≈ moveRight y (↑R 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
exact ⟨fun i => Or.inl ⟨_, (hl i).1⟩, fun j => Or.inr ⟨_, by simpa using (hr (R.symm j)).1⟩⟩
no goals
x y : PGame
L : LeftMoves x ≃ LeftMoves y
R : RightMoves x ≃ RightMoves y
hl : ∀ (i : LeftMoves x), moveLeft x i ≈ moveLeft y (↑L i)
hr : ∀ (j : RightMoves x), moveRight x j ≈ moveRight y (↑R j)
j : RightMoves y
⊢ moveRight x (?m.70452 j) ≤ moveRight y j
simpa using (hr (R.symm j)).1
no goals
case right
x y : PGame
L : LeftMoves x ≃ LeftMoves y
R : RightMoves x ≃ RightMoves y
hl : ∀ (i : LeftMoves x), moveLeft x i ≈ moveLeft y (↑L i)
hr : ∀ (j : RightMoves x), moveRight x j ≈ moveRight y (↑R j)
⊢ (∀ (i : LeftMoves y), (∃ i', moveLeft y i ≤ moveLeft x i') ∨ ∃ j, moveRight (moveLeft y i) j ≤ x) ∧
    ∀ (j : RightMoves x), (∃ i, y ≤ moveLeft (moveRight x j) i) ∨ ∃ j', moveRight y j' ≤ moveRight x j
exact ⟨fun i => Or.inl ⟨_, by simpa using (hl (L.symm i)).2⟩, fun j => Or.inr ⟨_, (hr j).2⟩⟩
no goals
x y : PGame
L : LeftMoves x ≃ LeftMoves y
R : RightMoves x ≃ RightMoves y
hl : ∀ (i : LeftMoves x), moveLeft x i ≈ moveLeft y (↑L i)
hr : ∀ (j : RightMoves x), moveRight x j ≈ moveRight y (↑R j)
i : LeftMoves y
⊢ moveLeft y i ≤ moveLeft x (?m.71074 i)
simpa using (hl (L.symm i)).2