case mk
y : PGame
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
i : RightMoves (mk α✝ β✝ a✝¹ a✝)
⊢ moveRight (mk α✝ β✝ a✝¹ a✝ + y) (↑toRightMovesAdd (Sum.inl i)) = moveRight (mk α✝ β✝ a✝¹ a✝) i + y
x y : PGame
i : RightMoves x
⊢ moveRight (x + y) (↑toRightMovesAdd (Sum.inl i)) = moveRight x i + y
cases x
case mk.mk
α✝¹ β✝¹ : Type u_1
a✝³ : α✝¹ → PGame
a✝² : β✝¹ → PGame
i : RightMoves (mk α✝¹ β✝¹ a✝³ a✝²)
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
⊢ moveRight (mk α✝¹ β✝¹ a✝³ a✝² + mk α✝ β✝ a✝¹ a✝) (↑toRightMovesAdd (Sum.inl i)) =
    moveRight (mk α✝¹ β✝¹ a✝³ a✝²) i + mk α✝ β✝ a✝¹ a✝
case mk
y : PGame
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
i : RightMoves (mk α✝ β✝ a✝¹ a✝)
⊢ moveRight (mk α✝ β✝ a✝¹ a✝ + y) (↑toRightMovesAdd (Sum.inl i)) = moveRight (mk α✝ β✝ a✝¹ a✝) i + y
cases y
no goals
case mk.mk
α✝¹ β✝¹ : Type u_1
a✝³ : α✝¹ → PGame
a✝² : β✝¹ → PGame
i : RightMoves (mk α✝¹ β✝¹ a✝³ a✝²)
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
⊢ moveRight (mk α✝¹ β✝¹ a✝³ a✝² + mk α✝ β✝ a✝¹ a✝) (↑toRightMovesAdd (Sum.inl i)) =
    moveRight (mk α✝¹ β✝¹ a✝³ a✝²) i + mk α✝ β✝ a✝¹ a✝
rfl