-- Mathlib/SetTheory/Game/Nim.lean
theorem equiv_nim_grundyValue (G : PGame.{u}) [G.Impartial] :
    G ≈ nim (toOrdinal (grundyValue G))

Proof state:
case hl
G : PGame
inst✝ : G.Impartial
x : (G + nim (toOrdinal G.grundyValue)).LeftMoves
i : G.LeftMoves
⊢ (G + nim (toOrdinal G.grundyValue)).moveLeft (toLeftMovesAdd (Sum.inl i)) ‖ 0

Tactic:
rw [add_moveLeft_inl,
  ← fuzzy_congr_left (add_congr_left (Equiv.symm (equiv_nim_grundyValue _))),
  nim_add_fuzzy_zero_iff]

Result:
case hl
G : PGame
inst✝ : G.Impartial
x : (G + nim (toOrdinal G.grundyValue)).LeftMoves
i : G.LeftMoves
⊢ toOrdinal (G.moveLeft i).grundyValue ≠ toOrdinal G.grundyValue

Proof state:
case hl
G : PGame
inst✝ : G.Impartial
x : (G + nim (toOrdinal G.grundyValue)).LeftMoves
i : G.LeftMoves
⊢ toOrdinal (G.moveLeft i).grundyValue ≠ toOrdinal G.grundyValue

Tactic:
exact grundyValue_ne_moveLeft i

Result:
no goals

Proof state:
case h
G : PGame
inst✝ : G.Impartial
x : (G + nim (toOrdinal G.grundyValue)).LeftMoves
i : (nim (toOrdinal G.grundyValue)).LeftMoves
j : G.LeftMoves
hj : (G.moveLeft j).grundyValue = ↑(toLeftMovesNim.symm i)
⊢ G.moveLeft j + nim ↑(toLeftMovesNim.symm i) ≈ 0

Tactic:
exact Equiv.trans (add_congr_left (equiv_nim_grundyValue _)) (hj ▸ Impartial.add_self _)

Result:
no goals

Proof state:
case hr.intro
G : PGame
inst✝ : G.Impartial
x : (G + nim (toOrdinal G.grundyValue)).LeftMoves
i : (nim (toOrdinal G.grundyValue)).LeftMoves
j : G.LeftMoves
hj : (G.moveLeft j).grundyValue = ↑(toLeftMovesNim.symm i)
⊢ ∃ i_1, (G + (nim (toOrdinal G.grundyValue)).moveLeft i).moveLeft i_1 ≈ 0

Tactic:
use toLeftMovesAdd (Sum.inl j)

Result:
case h
G : PGame
inst✝ : G.Impartial
x : (G + nim (toOrdinal G.grundyValue)).LeftMoves
i : (nim (toOrdinal G.grundyValue)).LeftMoves
j : G.LeftMoves
hj : (G.moveLeft j).grundyValue = ↑(toLeftMovesNim.symm i)
⊢ (G + (nim (toOrdinal G.grundyValue)).moveLeft i).moveLeft (toLeftMovesAdd (Sum.inl j)) ≈ 0

Proof state:
case h
G : PGame
inst✝ : G.Impartial
x : (G + nim (toOrdinal G.grundyValue)).LeftMoves
i : (nim (toOrdinal G.grundyValue)).LeftMoves
j : G.LeftMoves
hj : (G.moveLeft j).grundyValue = ↑(toLeftMovesNim.symm i)
⊢ (G + (nim (toOrdinal G.grundyValue)).moveLeft i).moveLeft (toLeftMovesAdd (Sum.inl j)) ≈ 0

Tactic:
rw [add_moveLeft_inl, moveLeft_nim]

Result:
case h
G : PGame
inst✝ : G.Impartial
x : (G + nim (toOrdinal G.grundyValue)).LeftMoves
i : (nim (toOrdinal G.grundyValue)).LeftMoves
j : G.LeftMoves
hj : (G.moveLeft j).grundyValue = ↑(toLeftMovesNim.symm i)
⊢ G.moveLeft j + nim ↑(toLeftMovesNim.symm i) ≈ 0

Proof state:
case hr
G : PGame
inst✝ : G.Impartial
x : (G + nim (toOrdinal G.grundyValue)).LeftMoves
i : (nim (toOrdinal G.grundyValue)).LeftMoves
⊢ (G + nim (toOrdinal G.grundyValue)).moveLeft (toLeftMovesAdd (Sum.inr i)) ‖ 0

Tactic:
rw [add_moveLeft_inr, ← Impartial.exists_left_move_equiv_iff_fuzzy_zero]

Result:
case hr
G : PGame
inst✝ : G.Impartial
x : (G + nim (toOrdinal G.grundyValue)).LeftMoves
i : (nim (toOrdinal G.grundyValue)).LeftMoves
⊢ ∃ i_1, (G + (nim (toOrdinal G.grundyValue)).moveLeft i).moveLeft i_1 ≈ 0

Proof state:
G : PGame
inst✝ : G.Impartial
x : (G + nim (toOrdinal G.grundyValue)).LeftMoves
⊢ (G + nim (toOrdinal G.grundyValue)).moveLeft x ‖ 0

Tactic:
apply leftMoves_add_cases x <;>
intro i

Result:
case hl
G : PGame
inst✝ : G.Impartial
x : (G + nim (toOrdinal G.grundyValue)).LeftMoves
i : G.LeftMoves
⊢ (G + nim (toOrdinal G.grundyValue)).moveLeft (toLeftMovesAdd (Sum.inl i)) ‖ 0

case hr
G : PGame
inst✝ : G.Impartial
x : (G + nim (toOrdinal G.grundyValue)).LeftMoves
i : (nim (toOrdinal G.grundyValue)).LeftMoves
⊢ (G + nim (toOrdinal G.grundyValue)).moveLeft (toLeftMovesAdd (Sum.inr i)) ‖ 0

Proof state:
G : PGame
inst✝ : G.Impartial
⊢ G ≈ nim (toOrdinal G.grundyValue)

Tactic:
rw [Impartial.equiv_iff_add_equiv_zero, ← Impartial.forall_leftMoves_fuzzy_iff_equiv_zero]

Result:
G : PGame
inst✝ : G.Impartial
⊢ ∀ (i : (G + nim (toOrdinal G.grundyValue)).LeftMoves), (G + nim (toOrdinal G.grundyValue)).moveLeft i ‖ 0

Proof state:
G : PGame
inst✝ : G.Impartial
⊢ ∀ (i : (G + nim (toOrdinal G.grundyValue)).LeftMoves), (G + nim (toOrdinal G.grundyValue)).moveLeft i ‖ 0

Tactic:
intro x

Result:
G : PGame
inst✝ : G.Impartial
x : (G + nim (toOrdinal G.grundyValue)).LeftMoves
⊢ (G + nim (toOrdinal G.grundyValue)).moveLeft x ‖ 0

Proof state:
case hr
G : PGame
inst✝ : G.Impartial
x : (G + nim (toOrdinal G.grundyValue)).LeftMoves
i : (nim (toOrdinal G.grundyValue)).LeftMoves
⊢ ∃ i_1, (G + (nim (toOrdinal G.grundyValue)).moveLeft i).moveLeft i_1 ≈ 0

Tactic:
obtain ⟨j, hj⟩ := exists_grundyValue_moveLeft_of_lt <| toLeftMovesNim_symm_lt i

Result:
case hr.intro
G : PGame
inst✝ : G.Impartial
x : (G + nim (toOrdinal G.grundyValue)).LeftMoves
i : (nim (toOrdinal G.grundyValue)).LeftMoves
j : G.LeftMoves
hj : (G.moveLeft j).grundyValue = ↑(toLeftMovesNim.symm i)
⊢ ∃ i_1, (G + (nim (toOrdinal G.grundyValue)).moveLeft i).moveLeft i_1 ≈ 0