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