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