case mk
y : PGame
i : LeftMoves y
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
⊢ moveLeft (mk α✝ β✝ a✝¹ a✝ + y) (↑toLeftMovesAdd (Sum.inr i)) = mk α✝ β✝ a✝¹ a✝ + moveLeft y i
x y : PGame
i : LeftMoves y
⊢ moveLeft (x + y) (↑toLeftMovesAdd (Sum.inr i)) = x + moveLeft y i
cases x
case mk.mk
α✝¹ β✝¹ : Type u_1
a✝³ : α✝¹ → PGame
a✝² : β✝¹ → PGame
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
i : LeftMoves (mk α✝ β✝ a✝¹ a✝)
⊢ moveLeft (mk α✝¹ β✝¹ a✝³ a✝² + mk α✝ β✝ a✝¹ a✝) (↑toLeftMovesAdd (Sum.inr i)) =
    mk α✝¹ β✝¹ a✝³ a✝² + moveLeft (mk α✝ β✝ a✝¹ a✝) i
case mk
y : PGame
i : LeftMoves y
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
⊢ moveLeft (mk α✝ β✝ a✝¹ a✝ + y) (↑toLeftMovesAdd (Sum.inr i)) = mk α✝ β✝ a✝¹ a✝ + moveLeft y i
cases y
no goals
case mk.mk
α✝¹ β✝¹ : Type u_1
a✝³ : α✝¹ → PGame
a✝² : β✝¹ → PGame
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
i : LeftMoves (mk α✝ β✝ a✝¹ a✝)
⊢ moveLeft (mk α✝¹ β✝¹ a✝³ a✝² + mk α✝ β✝ a✝¹ a✝) (↑toLeftMovesAdd (Sum.inr i)) =
    mk α✝¹ β✝¹ a✝³ a✝² + moveLeft (mk α✝ β✝ a✝¹ a✝) i
rfl