-- Mathlib/SetTheory/Game/Nim.lean
theorem grundyValue_nim_add_nim (x y : Ordinal) : grundyValue (nim x + nim y) = ∗x + ∗y

Proof state:
x y : Ordinal.{u_1}
⊢ (nim x + nim y).grundyValue = toNimber x + toNimber y

Tactic:
apply (grundyValue_le_of_forall_moveLeft _).antisymm (le_grundyValue_of_Iio_subset_moveLeft _)

Result:
x y : Ordinal.{u_1}
⊢ ∀ (i : (nim x + nim y).LeftMoves), ((nim x + nim y).moveLeft i).grundyValue ≠ toNimber x + toNimber y

x y : Ordinal.{u_1}
⊢ Set.Iio (toNimber x + toNimber y) ⊆ Set.range (grundyValue ∘ (nim x + nim y).moveLeft)

Proof state:
case inr
x y : Ordinal.{u_1}
k : Nimber
hk : k ∈ Set.Iio (toNimber x + toNimber y)
h : k + toNimber x < toNimber y
a : Ordinal.{u_1} := toOrdinal (k + toNimber x)
⊢ k ∈ Set.range (grundyValue ∘ (nim x + nim y).moveLeft)

Tactic:
use toLeftMovesAdd (Sum.inr (toLeftMovesNim ⟨a, h⟩))

Result:
case h
x y : Ordinal.{u_1}
k : Nimber
hk : k ∈ Set.Iio (toNimber x + toNimber y)
h : k + toNimber x < toNimber y
a : Ordinal.{u_1} := toOrdinal (k + toNimber x)
⊢ (grundyValue ∘ (nim x + nim y).moveLeft) (toLeftMovesAdd (Sum.inr (toLeftMovesNim ⟨a, h⟩))) = k

Proof state:
x y : Ordinal.{u_1}
⊢ Set.Iio (toNimber x + toNimber y) ⊆ Set.range (grundyValue ∘ (nim x + nim y).moveLeft)

Tactic:
intro k hk

Result:
x y : Ordinal.{u_1}
k : Nimber
hk : k ∈ Set.Iio (toNimber x + toNimber y)
⊢ k ∈ Set.range (grundyValue ∘ (nim x + nim y).moveLeft)

Proof state:
case hl
x y : Ordinal.{u_1}
i : (nim x + nim y).LeftMoves
j : (nim x).LeftMoves
this : ↑(toLeftMovesNim.symm j) ≠ x
⊢ ((nim x + nim y).moveLeft (toLeftMovesAdd (Sum.inl j))).grundyValue ≠ toNimber x + toNimber y

Tactic:
simpa [grundyValue_nim_add_nim (toLeftMovesNim.symm j) y]

Result:
no goals

Proof state:
case inl
x y : Ordinal.{u_1}
k : Nimber
hk : k ∈ Set.Iio (toNimber x + toNimber y)
h : k + toNimber y < toNimber x
a : Ordinal.{u_1} := toOrdinal (k + toNimber y)
⊢ k ∈ Set.range (grundyValue ∘ (nim x + nim y).moveLeft)

Tactic:
use toLeftMovesAdd (Sum.inl (toLeftMovesNim ⟨a, h⟩))

Result:
case h
x y : Ordinal.{u_1}
k : Nimber
hk : k ∈ Set.Iio (toNimber x + toNimber y)
h : k + toNimber y < toNimber x
a : Ordinal.{u_1} := toOrdinal (k + toNimber y)
⊢ (grundyValue ∘ (nim x + nim y).moveLeft) (toLeftMovesAdd (Sum.inl (toLeftMovesNim ⟨a, h⟩))) = k

Proof state:
case h
x y : Ordinal.{u_1}
k : Nimber
hk : k ∈ Set.Iio (toNimber x + toNimber y)
h : k + toNimber y < toNimber x
a : Ordinal.{u_1} := toOrdinal (k + toNimber y)
⊢ (grundyValue ∘ (nim x + nim y).moveLeft) (toLeftMovesAdd (Sum.inl (toLeftMovesNim ⟨a, h⟩))) = k

Tactic:
simp [a, grundyValue_nim_add_nim a y]

Result:
no goals

Proof state:
case inl
x y : Ordinal.{u_1}
k : Nimber
hk : k ∈ Set.Iio (toNimber x + toNimber y)
h : k + toNimber y < toNimber x
⊢ k ∈ Set.range (grundyValue ∘ (nim x + nim y).moveLeft)

Tactic:
let a := toOrdinal (k + ∗y)

Result:
case inl
x y : Ordinal.{u_1}
k : Nimber
hk : k ∈ Set.Iio (toNimber x + toNimber y)
h : k + toNimber y < toNimber x
a : Ordinal.{u_1} := toOrdinal (k + toNimber y)
⊢ k ∈ Set.range (grundyValue ∘ (nim x + nim y).moveLeft)

Proof state:
case inr
x y : Ordinal.{u_1}
k : Nimber
hk : k ∈ Set.Iio (toNimber x + toNimber y)
h : k + toNimber x < toNimber y
⊢ k ∈ Set.range (grundyValue ∘ (nim x + nim y).moveLeft)

Tactic:
let a := toOrdinal (k + ∗x)

Result:
case inr
x y : Ordinal.{u_1}
k : Nimber
hk : k ∈ Set.Iio (toNimber x + toNimber y)
h : k + toNimber x < toNimber y
a : Ordinal.{u_1} := toOrdinal (k + toNimber x)
⊢ k ∈ Set.range (grundyValue ∘ (nim x + nim y).moveLeft)

Proof state:
x y : Ordinal.{u_1}
i : (nim x + nim y).LeftMoves
⊢ ((nim x + nim y).moveLeft i).grundyValue ≠ toNimber x + toNimber y

Tactic:
apply leftMoves_add_cases i <;> intro j <;> have := (toLeftMovesNim_symm_lt j).ne

Result:
case hl
x y : Ordinal.{u_1}
i : (nim x + nim y).LeftMoves
j : (nim x).LeftMoves
this : ↑(toLeftMovesNim.symm j) ≠ x
⊢ ((nim x + nim y).moveLeft (toLeftMovesAdd (Sum.inl j))).grundyValue ≠ toNimber x + toNimber y

case hr
x y : Ordinal.{u_1}
i : (nim x + nim y).LeftMoves
j : (nim y).LeftMoves
this : ↑(toLeftMovesNim.symm j) ≠ y
⊢ ((nim x + nim y).moveLeft (toLeftMovesAdd (Sum.inr j))).grundyValue ≠ toNimber x + toNimber y

Proof state:
x y : Ordinal.{u_1}
k : Nimber
hk : k ∈ Set.Iio (toNimber x + toNimber y)
⊢ k ∈ Set.range (grundyValue ∘ (nim x + nim y).moveLeft)

Tactic:
obtain h | h := Nimber.lt_add_cases hk

Result:
case inl
x y : Ordinal.{u_1}
k : Nimber
hk : k ∈ Set.Iio (toNimber x + toNimber y)
h : k + toNimber y < toNimber x
⊢ k ∈ Set.range (grundyValue ∘ (nim x + nim y).moveLeft)

case inr
x y : Ordinal.{u_1}
k : Nimber
hk : k ∈ Set.Iio (toNimber x + toNimber y)
h : k + toNimber x < toNimber y
⊢ k ∈ Set.range (grundyValue ∘ (nim x + nim y).moveLeft)

Proof state:
case h
x y : Ordinal.{u_1}
k : Nimber
hk : k ∈ Set.Iio (toNimber x + toNimber y)
h : k + toNimber x < toNimber y
a : Ordinal.{u_1} := toOrdinal (k + toNimber x)
⊢ (grundyValue ∘ (nim x + nim y).moveLeft) (toLeftMovesAdd (Sum.inr (toLeftMovesNim ⟨a, h⟩))) = k

Tactic:
simp [a, grundyValue_nim_add_nim x a, add_comm (∗x)]

Result:
no goals

Proof state:
x y : Ordinal.{u_1}
⊢ ∀ (i : (nim x + nim y).LeftMoves), ((nim x + nim y).moveLeft i).grundyValue ≠ toNimber x + toNimber y

Tactic:
intro i

Result:
x y : Ordinal.{u_1}
i : (nim x + nim y).LeftMoves
⊢ ((nim x + nim y).moveLeft i).grundyValue ≠ toNimber x + toNimber y

Proof state:
case hr
x y : Ordinal.{u_1}
i : (nim x + nim y).LeftMoves
j : (nim y).LeftMoves
this : ↑(toLeftMovesNim.symm j) ≠ y
⊢ ((nim x + nim y).moveLeft (toLeftMovesAdd (Sum.inr j))).grundyValue ≠ toNimber x + toNimber y

Tactic:
simpa [grundyValue_nim_add_nim x (toLeftMovesNim.symm j)]

Result:
no goals