x y : PGame
k : RightMoves (x + y)
P : RightMoves (x + y) → Prop
hl : ∀ (j : RightMoves x), P (↑toRightMovesAdd (Sum.inl j))
hr : ∀ (j : RightMoves y), P (↑toRightMovesAdd (Sum.inr j))
⊢ P (↑toRightMovesAdd (↑toRightMovesAdd.symm k))
x y : PGame
k : RightMoves (x + y)
P : RightMoves (x + y) → Prop
hl : ∀ (j : RightMoves x), P (↑toRightMovesAdd (Sum.inl j))
hr : ∀ (j : RightMoves y), P (↑toRightMovesAdd (Sum.inr j))
⊢ P k
rw [← toRightMovesAdd.apply_symm_apply k]
case inl
x y : PGame
k : RightMoves (x + y)
P : RightMoves (x + y) → Prop
hl : ∀ (j : RightMoves x), P (↑toRightMovesAdd (Sum.inl j))
hr : ∀ (j : RightMoves y), P (↑toRightMovesAdd (Sum.inr j))
i : RightMoves x
⊢ P (↑toRightMovesAdd (Sum.inl i))

case inr
x y : PGame
k : RightMoves (x + y)
P : RightMoves (x + y) → Prop
hl : ∀ (j : RightMoves x), P (↑toRightMovesAdd (Sum.inl j))
hr : ∀ (j : RightMoves y), P (↑toRightMovesAdd (Sum.inr j))
i : RightMoves y
⊢ P (↑toRightMovesAdd (Sum.inr i))
x y : PGame
k : RightMoves (x + y)
P : RightMoves (x + y) → Prop
hl : ∀ (j : RightMoves x), P (↑toRightMovesAdd (Sum.inl j))
hr : ∀ (j : RightMoves y), P (↑toRightMovesAdd (Sum.inr j))
⊢ P (↑toRightMovesAdd (↑toRightMovesAdd.symm k))
cases' toRightMovesAdd.symm k with i i
no goals
case inl
x y : PGame
k : RightMoves (x + y)
P : RightMoves (x + y) → Prop
hl : ∀ (j : RightMoves x), P (↑toRightMovesAdd (Sum.inl j))
hr : ∀ (j : RightMoves y), P (↑toRightMovesAdd (Sum.inr j))
i : RightMoves x
⊢ P (↑toRightMovesAdd (Sum.inl i))
exact hl i
no goals
case inr
x y : PGame
k : RightMoves (x + y)
P : RightMoves (x + y) → Prop
hl : ∀ (j : RightMoves x), P (↑toRightMovesAdd (Sum.inl j))
hr : ∀ (j : RightMoves y), P (↑toRightMovesAdd (Sum.inr j))
i : RightMoves y
⊢ P (↑toRightMovesAdd (Sum.inr i))
exact hr i