case mk
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
i : RightMoves (-mk α✝ β✝ a✝¹ a✝)
⊢ moveRight (-mk α✝ β✝ a✝¹ a✝) i = -moveLeft (mk α✝ β✝ a✝¹ a✝) (↑toRightMovesNeg.symm i)
x : PGame
i : RightMoves (-x)
⊢ moveRight (-x) i = -moveLeft x (↑toRightMovesNeg.symm i)
cases x
no goals
case mk
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
i : RightMoves (-mk α✝ β✝ a✝¹ a✝)
⊢ moveRight (-mk α✝ β✝ a✝¹ a✝) i = -moveLeft (mk α✝ β✝ a✝¹ a✝) (↑toRightMovesNeg.symm i)
rfl