[GOAL]
o : Ordinal.{u_1}
⊢ let_fun this := (_ : IsWellOrder (Quotient.out o).α fun x x_1 => x < x_1);
  nim o =
    mk (Quotient.out o).α (Quotient.out o).α (fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)) fun o₂ =>
      nim (typein (fun x x_1 => x < x_1) o₂)
[PROOFSTEP]
rw [nim]
[GOAL]
o : Ordinal.{u_1}
⊢ let_fun this := (_ : IsWellOrder (Quotient.out o).α fun x x_1 => x < x_1);
  (mk (Quotient.out o).α (Quotient.out o).α
      (fun o₂ =>
        let_fun x := (_ : typein (fun x x_1 => x < x_1) o₂ < o);
        nim (typein (Quotient.out o).r o₂))
      fun o₂ =>
      let_fun x := (_ : typein (fun x x_1 => x < x_1) o₂ < o);
      nim (typein (Quotient.out o).r o₂)) =
    mk (Quotient.out o).α (Quotient.out o).α (fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)) fun o₂ =>
      nim (typein (fun x x_1 => x < x_1) o₂)
[PROOFSTEP]
rfl
[GOAL]
o : Ordinal.{u_1}
⊢ LeftMoves (nim o) = (Quotient.out o).α
[PROOFSTEP]
rw [nim_def]
[GOAL]
o : Ordinal.{u_1}
⊢ LeftMoves
      (mk (Quotient.out o).α (Quotient.out o).α (fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)) fun o₂ =>
        nim (typein (fun x x_1 => x < x_1) o₂)) =
    (Quotient.out o).α
[PROOFSTEP]
rfl
[GOAL]
o : Ordinal.{u_1}
⊢ RightMoves (nim o) = (Quotient.out o).α
[PROOFSTEP]
rw [nim_def]
[GOAL]
o : Ordinal.{u_1}
⊢ RightMoves
      (mk (Quotient.out o).α (Quotient.out o).α (fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)) fun o₂ =>
        nim (typein (fun x x_1 => x < x_1) o₂)) =
    (Quotient.out o).α
[PROOFSTEP]
rfl
[GOAL]
o : Ordinal.{u_1}
⊢ let_fun this := (_ : IsWellOrder (Quotient.out o).α fun x x_1 => x < x_1);
  HEq (moveLeft (nim o)) fun i => nim (typein (fun x x_1 => x < x_1) i)
[PROOFSTEP]
rw [nim_def]
[GOAL]
o : Ordinal.{u_1}
⊢ let_fun this := (_ : IsWellOrder (Quotient.out o).α fun x x_1 => x < x_1);
  HEq
    (moveLeft
      (mk (Quotient.out o).α (Quotient.out o).α (fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)) fun o₂ =>
        nim (typein (fun x x_1 => x < x_1) o₂)))
    fun i => nim (typein (fun x x_1 => x < x_1) i)
[PROOFSTEP]
rfl
[GOAL]
o : Ordinal.{u_1}
⊢ let_fun this := (_ : IsWellOrder (Quotient.out o).α fun x x_1 => x < x_1);
  HEq (moveRight (nim o)) fun i => nim (typein (fun x x_1 => x < x_1) i)
[PROOFSTEP]
rw [nim_def]
[GOAL]
o : Ordinal.{u_1}
⊢ let_fun this := (_ : IsWellOrder (Quotient.out o).α fun x x_1 => x < x_1);
  HEq
    (moveRight
      (mk (Quotient.out o).α (Quotient.out o).α (fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)) fun o₂ =>
        nim (typein (fun x x_1 => x < x_1) o₂)))
    fun i => nim (typein (fun x x_1 => x < x_1) i)
[PROOFSTEP]
rfl
[GOAL]
o : Ordinal.{u_1}
i : ↑(Set.Iio o)
⊢ moveLeft (nim o) (↑toLeftMovesNim i) = nim ↑i
[PROOFSTEP]
simp
[GOAL]
o : Ordinal.{u_1}
i : ↑(Set.Iio o)
⊢ moveRight (nim o) (↑toRightMovesNim i) = nim ↑i
[PROOFSTEP]
simp
[GOAL]
o : Ordinal.{?u.16630}
P : LeftMoves (nim o) → Sort u_1
i : LeftMoves (nim o)
H : (a : Ordinal.{?u.16630}) → (H : a < o) → P (↑toLeftMovesNim { val := a, property := H })
⊢ P i
[PROOFSTEP]
rw [← toLeftMovesNim.apply_symm_apply i]
[GOAL]
o : Ordinal.{?u.16630}
P : LeftMoves (nim o) → Sort u_1
i : LeftMoves (nim o)
H : (a : Ordinal.{?u.16630}) → (H : a < o) → P (↑toLeftMovesNim { val := a, property := H })
⊢ P (↑toLeftMovesNim (↑toLeftMovesNim.symm i))
[PROOFSTEP]
apply H
[GOAL]
o : Ordinal.{?u.17085}
P : RightMoves (nim o) → Sort u_1
i : RightMoves (nim o)
H : (a : Ordinal.{?u.17085}) → (H : a < o) → P (↑toRightMovesNim { val := a, property := H })
⊢ P i
[PROOFSTEP]
rw [← toRightMovesNim.apply_symm_apply i]
[GOAL]
o : Ordinal.{?u.17085}
P : RightMoves (nim o) → Sort u_1
i : RightMoves (nim o)
H : (a : Ordinal.{?u.17085}) → (H : a < o) → P (↑toRightMovesNim { val := a, property := H })
⊢ P (↑toRightMovesNim (↑toRightMovesNim.symm i))
[PROOFSTEP]
apply H
[GOAL]
⊢ IsEmpty (LeftMoves (nim 0))
[PROOFSTEP]
rw [nim_def]
[GOAL]
⊢ IsEmpty
    (LeftMoves
      (mk (Quotient.out 0).α (Quotient.out 0).α (fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)) fun o₂ =>
        nim (typein (fun x x_1 => x < x_1) o₂)))
[PROOFSTEP]
exact Ordinal.isEmpty_out_zero
[GOAL]
⊢ IsEmpty (RightMoves (nim 0))
[PROOFSTEP]
rw [nim_def]
[GOAL]
⊢ IsEmpty
    (RightMoves
      (mk (Quotient.out 0).α (Quotient.out 0).α (fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)) fun o₂ =>
        nim (typein (fun x x_1 => x < x_1) o₂)))
[PROOFSTEP]
exact Ordinal.isEmpty_out_zero
[GOAL]
i : LeftMoves (nim 1)
⊢ ↑toLeftMovesNim.symm i = { val := 0, property := (_ : 0 ∈ Set.Iio 1) }
[PROOFSTEP]
simp
[GOAL]
i : RightMoves (nim 1)
⊢ ↑toRightMovesNim.symm i = { val := 0, property := (_ : 0 ∈ Set.Iio 1) }
[PROOFSTEP]
simp
[GOAL]
x : LeftMoves (nim 1)
⊢ moveLeft (nim 1) x = nim 0
[PROOFSTEP]
simp
[GOAL]
x : RightMoves (nim 1)
⊢ moveRight (nim 1) x = nim 0
[PROOFSTEP]
simp
[GOAL]
⊢ nim 1 ≡r star
[PROOFSTEP]
rw [nim_def]
[GOAL]
⊢ (mk (Quotient.out 1).α (Quotient.out 1).α (fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)) fun o₂ =>
      nim (typein (fun x x_1 => x < x_1) o₂)) ≡r
    star
[PROOFSTEP]
refine' ⟨_, _, fun i => _, fun j => _⟩
[GOAL]
case refine'_1
⊢ LeftMoves
      (mk (Quotient.out 1).α (Quotient.out 1).α (fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)) fun o₂ =>
        nim (typein (fun x x_1 => x < x_1) o₂)) ≃
    LeftMoves star
case refine'_2
⊢ RightMoves
      (mk (Quotient.out 1).α (Quotient.out 1).α (fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)) fun o₂ =>
        nim (typein (fun x x_1 => x < x_1) o₂)) ≃
    RightMoves star
case refine'_3
i :
  LeftMoves
    (mk (Quotient.out 1).α (Quotient.out 1).α (fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)) fun o₂ =>
      nim (typein (fun x x_1 => x < x_1) o₂))
⊢ moveLeft
      (mk (Quotient.out 1).α (Quotient.out 1).α (fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)) fun o₂ =>
        nim (typein (fun x x_1 => x < x_1) o₂))
      i ≡r
    moveLeft star (↑?refine'_1 i)
case refine'_4
j :
  RightMoves
    (mk (Quotient.out 1).α (Quotient.out 1).α (fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)) fun o₂ =>
      nim (typein (fun x x_1 => x < x_1) o₂))
⊢ moveRight
      (mk (Quotient.out 1).α (Quotient.out 1).α (fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)) fun o₂ =>
        nim (typein (fun x x_1 => x < x_1) o₂))
      j ≡r
    moveRight star (↑?refine'_2 j)
[PROOFSTEP]
any_goals dsimp; apply Equiv.equivOfUnique
[GOAL]
case refine'_1
⊢ LeftMoves
      (mk (Quotient.out 1).α (Quotient.out 1).α (fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)) fun o₂ =>
        nim (typein (fun x x_1 => x < x_1) o₂)) ≃
    LeftMoves star
[PROOFSTEP]
dsimp
[GOAL]
case refine'_1
⊢ (Quotient.out 1).α ≃ PUnit
[PROOFSTEP]
apply Equiv.equivOfUnique
[GOAL]
case refine'_2
⊢ RightMoves
      (mk (Quotient.out 1).α (Quotient.out 1).α (fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)) fun o₂ =>
        nim (typein (fun x x_1 => x < x_1) o₂)) ≃
    RightMoves star
[PROOFSTEP]
dsimp
[GOAL]
case refine'_2
⊢ (Quotient.out 1).α ≃ PUnit
[PROOFSTEP]
apply Equiv.equivOfUnique
[GOAL]
case refine'_3
i :
  LeftMoves
    (mk (Quotient.out 1).α (Quotient.out 1).α (fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)) fun o₂ =>
      nim (typein (fun x x_1 => x < x_1) o₂))
⊢ moveLeft
      (mk (Quotient.out 1).α (Quotient.out 1).α (fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)) fun o₂ =>
        nim (typein (fun x x_1 => x < x_1) o₂))
      i ≡r
    moveLeft star (↑(id (Equiv.equivOfUnique (Quotient.out 1).α PUnit)) i)
[PROOFSTEP]
dsimp
[GOAL]
case refine'_3
i :
  LeftMoves
    (mk (Quotient.out 1).α (Quotient.out 1).α (fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)) fun o₂ =>
      nim (typein (fun x x_1 => x < x_1) o₂))
⊢ nim (typein (fun x x_1 => x < x_1) i) ≡r 0
[PROOFSTEP]
apply Equiv.equivOfUnique
[GOAL]
case refine'_4
j :
  RightMoves
    (mk (Quotient.out 1).α (Quotient.out 1).α (fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)) fun o₂ =>
      nim (typein (fun x x_1 => x < x_1) o₂))
⊢ moveRight
      (mk (Quotient.out 1).α (Quotient.out 1).α (fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)) fun o₂ =>
        nim (typein (fun x x_1 => x < x_1) o₂))
      j ≡r
    moveRight star (↑(id (Equiv.equivOfUnique (Quotient.out 1).α PUnit)) j)
[PROOFSTEP]
dsimp
[GOAL]
case refine'_4
j :
  RightMoves
    (mk (Quotient.out 1).α (Quotient.out 1).α (fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)) fun o₂ =>
      nim (typein (fun x x_1 => x < x_1) o₂))
⊢ nim (typein (fun x x_1 => x < x_1) j) ≡r 0
[PROOFSTEP]
apply Equiv.equivOfUnique
[GOAL]
case refine'_3
i :
  LeftMoves
    (mk (Quotient.out 1).α (Quotient.out 1).α (fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)) fun o₂ =>
      nim (typein (fun x x_1 => x < x_1) o₂))
⊢ moveLeft
      (mk (Quotient.out 1).α (Quotient.out 1).α (fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)) fun o₂ =>
        nim (typein (fun x x_1 => x < x_1) o₂))
      i ≡r
    moveLeft star (↑(id (Equiv.equivOfUnique (Quotient.out 1).α PUnit)) i)
case refine'_4
j :
  RightMoves
    (mk (Quotient.out 1).α (Quotient.out 1).α (fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)) fun o₂ =>
      nim (typein (fun x x_1 => x < x_1) o₂))
⊢ moveRight
      (mk (Quotient.out 1).α (Quotient.out 1).α (fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)) fun o₂ =>
        nim (typein (fun x x_1 => x < x_1) o₂))
      j ≡r
    moveRight star (↑(id (Equiv.equivOfUnique (Quotient.out 1).α PUnit)) j)
[PROOFSTEP]
all_goals simp; exact nimZeroRelabelling
[GOAL]
case refine'_3
i :
  LeftMoves
    (mk (Quotient.out 1).α (Quotient.out 1).α (fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)) fun o₂ =>
      nim (typein (fun x x_1 => x < x_1) o₂))
⊢ moveLeft
      (mk (Quotient.out 1).α (Quotient.out 1).α (fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)) fun o₂ =>
        nim (typein (fun x x_1 => x < x_1) o₂))
      i ≡r
    moveLeft star (↑(id (Equiv.equivOfUnique (Quotient.out 1).α PUnit)) i)
[PROOFSTEP]
simp
[GOAL]
case refine'_3
i :
  LeftMoves
    (mk (Quotient.out 1).α (Quotient.out 1).α (fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)) fun o₂ =>
      nim (typein (fun x x_1 => x < x_1) o₂))
⊢ nim 0 ≡r 0
[PROOFSTEP]
exact nimZeroRelabelling
[GOAL]
case refine'_4
j :
  RightMoves
    (mk (Quotient.out 1).α (Quotient.out 1).α (fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)) fun o₂ =>
      nim (typein (fun x x_1 => x < x_1) o₂))
⊢ moveRight
      (mk (Quotient.out 1).α (Quotient.out 1).α (fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)) fun o₂ =>
        nim (typein (fun x x_1 => x < x_1) o₂))
      j ≡r
    moveRight star (↑(id (Equiv.equivOfUnique (Quotient.out 1).α PUnit)) j)
[PROOFSTEP]
simp
[GOAL]
case refine'_4
j :
  RightMoves
    (mk (Quotient.out 1).α (Quotient.out 1).α (fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)) fun o₂ =>
      nim (typein (fun x x_1 => x < x_1) o₂))
⊢ nim 0 ≡r 0
[PROOFSTEP]
exact nimZeroRelabelling
[GOAL]
o : Ordinal.{u_1}
⊢ birthday (nim o) = o
[PROOFSTEP]
induction' o using Ordinal.induction with o IH
[GOAL]
case h
o : Ordinal.{u_1}
IH : ∀ (k : Ordinal.{u_1}), k < o → birthday (nim k) = k
⊢ birthday (nim o) = o
[PROOFSTEP]
rw [nim_def, birthday_def]
[GOAL]
case h
o : Ordinal.{u_1}
IH : ∀ (k : Ordinal.{u_1}), k < o → birthday (nim k) = k
⊢ max
      (lsub fun i =>
        birthday
          (moveLeft
            (mk (Quotient.out o).α (Quotient.out o).α (fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)) fun o₂ =>
              nim (typein (fun x x_1 => x < x_1) o₂))
            i))
      (lsub fun i =>
        birthday
          (moveRight
            (mk (Quotient.out o).α (Quotient.out o).α (fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)) fun o₂ =>
              nim (typein (fun x x_1 => x < x_1) o₂))
            i)) =
    o
[PROOFSTEP]
dsimp
[GOAL]
case h
o : Ordinal.{u_1}
IH : ∀ (k : Ordinal.{u_1}), k < o → birthday (nim k) = k
⊢ max (lsub fun i => birthday (nim (typein (fun x x_1 => x < x_1) i)))
      (lsub fun i => birthday (nim (typein (fun x x_1 => x < x_1) i))) =
    o
[PROOFSTEP]
rw [max_eq_right le_rfl]
[GOAL]
case h
o : Ordinal.{u_1}
IH : ∀ (k : Ordinal.{u_1}), k < o → birthday (nim k) = k
⊢ (lsub fun i => birthday (nim (typein (fun x x_1 => x < x_1) i))) = o
[PROOFSTEP]
convert lsub_typein o with i
[GOAL]
case h.e'_2.h.e'_2.h
o : Ordinal.{u_1}
IH : ∀ (k : Ordinal.{u_1}), k < o → birthday (nim k) = k
i : (Quotient.out o).α
⊢ birthday (nim (typein (fun x x_1 => x < x_1) i)) = typein (fun x x_1 => x < x_1) i
[PROOFSTEP]
exact IH _ (typein_lt_self i)
[GOAL]
o : Ordinal.{u_1}
⊢ -nim o = nim o
[PROOFSTEP]
induction' o using Ordinal.induction with o IH
[GOAL]
case h
o : Ordinal.{u_1}
IH : ∀ (k : Ordinal.{u_1}), k < o → -nim k = nim k
⊢ -nim o = nim o
[PROOFSTEP]
rw [nim_def]
[GOAL]
case h
o : Ordinal.{u_1}
IH : ∀ (k : Ordinal.{u_1}), k < o → -nim k = nim k
⊢ (-mk (Quotient.out o).α (Quotient.out o).α (fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)) fun o₂ =>
        nim (typein (fun x x_1 => x < x_1) o₂)) =
    mk (Quotient.out o).α (Quotient.out o).α (fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)) fun o₂ =>
      nim (typein (fun x x_1 => x < x_1) o₂)
[PROOFSTEP]
dsimp
[GOAL]
case h
o : Ordinal.{u_1}
IH : ∀ (k : Ordinal.{u_1}), k < o → -nim k = nim k
⊢ (mk (Quotient.out o).α (Quotient.out o).α (fun j => -nim (typein (fun x x_1 => x < x_1) j)) fun i =>
      -nim (typein (fun x x_1 => x < x_1) i)) =
    mk (Quotient.out o).α (Quotient.out o).α (fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)) fun o₂ =>
      nim (typein (fun x x_1 => x < x_1) o₂)
[PROOFSTEP]
congr
[GOAL]
case h.e_a
o : Ordinal.{u_1}
IH : ∀ (k : Ordinal.{u_1}), k < o → -nim k = nim k
⊢ (fun j => -nim (typein (fun x x_1 => x < x_1) j)) = fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)
[PROOFSTEP]
funext i
[GOAL]
case h.e_a
o : Ordinal.{u_1}
IH : ∀ (k : Ordinal.{u_1}), k < o → -nim k = nim k
⊢ (fun i => -nim (typein (fun x x_1 => x < x_1) i)) = fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)
[PROOFSTEP]
funext i
[GOAL]
case h.e_a.h
o : Ordinal.{u_1}
IH : ∀ (k : Ordinal.{u_1}), k < o → -nim k = nim k
i : (Quotient.out o).α
⊢ -nim (typein (fun x x_1 => x < x_1) i) = nim (typein (fun x x_1 => x < x_1) i)
[PROOFSTEP]
exact IH _ (Ordinal.typein_lt_self i)
[GOAL]
case h.e_a.h
o : Ordinal.{u_1}
IH : ∀ (k : Ordinal.{u_1}), k < o → -nim k = nim k
i : (Quotient.out o).α
⊢ -nim (typein (fun x x_1 => x < x_1) i) = nim (typein (fun x x_1 => x < x_1) i)
[PROOFSTEP]
exact IH _ (Ordinal.typein_lt_self i)
[GOAL]
o : Ordinal.{?u.36099}
⊢ Impartial (nim o)
[PROOFSTEP]
induction' o using Ordinal.induction with o IH
[GOAL]
case h
o : Ordinal.{?u.36117}
IH : ∀ (k : Ordinal.{?u.36117}), k < o → Impartial (nim k)
⊢ Impartial (nim o)
[PROOFSTEP]
rw [impartial_def, neg_nim]
[GOAL]
case h
o : Ordinal.{?u.36117}
IH : ∀ (k : Ordinal.{?u.36117}), k < o → Impartial (nim k)
⊢ nim o ≈ nim o ∧
    (∀ (i : LeftMoves (nim o)), Impartial (moveLeft (nim o) i)) ∧
      ∀ (j : RightMoves (nim o)), Impartial (moveRight (nim o) j)
[PROOFSTEP]
refine' ⟨equiv_rfl, fun i => _, fun i => _⟩
[GOAL]
case h.refine'_1
o : Ordinal.{?u.36117}
IH : ∀ (k : Ordinal.{?u.36117}), k < o → Impartial (nim k)
i : LeftMoves (nim o)
⊢ Impartial (moveLeft (nim o) i)
[PROOFSTEP]
simpa using IH _ (typein_lt_self _)
[GOAL]
case h.refine'_2
o : Ordinal.{?u.37361}
IH : ∀ (k : Ordinal.{?u.37361}), k < o → Impartial (nim k)
i : RightMoves (nim o)
⊢ Impartial (moveRight (nim o) i)
[PROOFSTEP]
simpa using IH _ (typein_lt_self _)
[GOAL]
o : Ordinal.{u_1}
ho : o ≠ 0
⊢ nim o ‖ 0
[PROOFSTEP]
rw [Impartial.fuzzy_zero_iff_lf, nim_def, lf_zero_le]
[GOAL]
o : Ordinal.{u_1}
ho : o ≠ 0
⊢ ∃ j,
    moveRight
        (mk (Quotient.out o).α (Quotient.out o).α (fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)) fun o₂ =>
          nim (typein (fun x x_1 => x < x_1) o₂))
        j ≤
      0
[PROOFSTEP]
rw [← Ordinal.pos_iff_ne_zero] at ho 
[GOAL]
o : Ordinal.{u_1}
ho : 0 < o
⊢ ∃ j,
    moveRight
        (mk (Quotient.out o).α (Quotient.out o).α (fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)) fun o₂ =>
          nim (typein (fun x x_1 => x < x_1) o₂))
        j ≤
      0
[PROOFSTEP]
exact ⟨(Ordinal.principalSegOut ho).top, by simp⟩
[GOAL]
o : Ordinal.{u_1}
ho : 0 < o
⊢ moveRight
      (mk (Quotient.out o).α (Quotient.out o).α (fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)) fun o₂ =>
        nim (typein (fun x x_1 => x < x_1) o₂))
      (principalSegOut ho).top ≤
    0
[PROOFSTEP]
simp
[GOAL]
o₁ o₂ : Ordinal.{u_1}
⊢ nim o₁ + nim o₂ ≈ 0 ↔ o₁ = o₂
[PROOFSTEP]
constructor
[GOAL]
case mp
o₁ o₂ : Ordinal.{u_1}
⊢ nim o₁ + nim o₂ ≈ 0 → o₁ = o₂
[PROOFSTEP]
refine' not_imp_not.1 fun hne : _ ≠ _ => (Impartial.not_equiv_zero_iff (nim o₁ + nim o₂)).2 _
[GOAL]
case mp
o₁ o₂ : Ordinal.{u_1}
hne : o₁ ≠ o₂
⊢ nim o₁ + nim o₂ ‖ 0
[PROOFSTEP]
wlog h : o₁ < o₂
[GOAL]
case mp.inr
o₁ o₂ : Ordinal.{u_1}
hne : o₁ ≠ o₂
this : ∀ (o₁ o₂ : Ordinal.{u_1}), o₁ ≠ o₂ → o₁ < o₂ → nim o₁ + nim o₂ ‖ 0
h : ¬o₁ < o₂
⊢ nim o₁ + nim o₂ ‖ 0
[PROOFSTEP]
exact (fuzzy_congr_left add_comm_equiv).1 (this _ _ hne.symm (hne.lt_or_lt.resolve_left h))
[GOAL]
o₁ o₂ : Ordinal.{u_1}
hne : o₁ ≠ o₂
h : o₁ < o₂
⊢ nim o₁ + nim o₂ ‖ 0
[PROOFSTEP]
rw [Impartial.fuzzy_zero_iff_gf, zero_lf_le, nim_def o₂]
[GOAL]
o₁ o₂ : Ordinal.{u_1}
hne : o₁ ≠ o₂
h : o₁ < o₂
⊢ ∃ i,
    0 ≤
      moveLeft
        (nim o₁ +
          mk (Quotient.out o₂).α (Quotient.out o₂).α (fun o₂_1 => nim (typein (fun x x_1 => x < x_1) o₂_1)) fun o₂_1 =>
            nim (typein (fun x x_1 => x < x_1) o₂_1))
        i
[PROOFSTEP]
refine' ⟨toLeftMovesAdd (Sum.inr _), _⟩
[GOAL]
case refine'_1
o₁ o₂ : Ordinal.{u_1}
hne : o₁ ≠ o₂
h : o₁ < o₂
⊢ LeftMoves
    (mk (Quotient.out o₂).α (Quotient.out o₂).α (fun o₂_1 => nim (typein (fun x x_1 => x < x_1) o₂_1)) fun o₂_1 =>
      nim (typein (fun x x_1 => x < x_1) o₂_1))
[PROOFSTEP]
exact (Ordinal.principalSegOut h).top
[GOAL]
case refine'_2
o₁ o₂ : Ordinal.{u_1}
hne : o₁ ≠ o₂
h : o₁ < o₂
⊢ 0 ≤
    moveLeft
      (nim o₁ +
        mk (Quotient.out o₂).α (Quotient.out o₂).α (fun o₂_1 => nim (typein (fun x x_1 => x < x_1) o₂_1)) fun o₂_1 =>
          nim (typein (fun x x_1 => x < x_1) o₂_1))
      (↑toLeftMovesAdd (Sum.inr (principalSegOut h).top))
[PROOFSTEP]
simpa only [Ordinal.typein_top, Ordinal.type_lt, PGame.add_moveLeft_inr, PGame.moveLeft_mk] using
  (Impartial.add_self (nim o₁)).2
[GOAL]
case mpr
o₁ o₂ : Ordinal.{u_1}
⊢ o₁ = o₂ → nim o₁ + nim o₂ ≈ 0
[PROOFSTEP]
rintro rfl
[GOAL]
case mpr
o₁ : Ordinal.{u_1}
⊢ nim o₁ + nim o₁ ≈ 0
[PROOFSTEP]
exact Impartial.add_self (nim o₁)
[GOAL]
o₁ o₂ : Ordinal.{u_1}
⊢ nim o₁ + nim o₂ ‖ 0 ↔ o₁ ≠ o₂
[PROOFSTEP]
rw [iff_not_comm, Impartial.not_fuzzy_zero_iff, nim_add_equiv_zero_iff]
[GOAL]
o₁ o₂ : Ordinal.{u_1}
⊢ nim o₁ ≈ nim o₂ ↔ o₁ = o₂
[PROOFSTEP]
rw [Impartial.equiv_iff_add_equiv_zero, nim_add_equiv_zero_iff]
[GOAL]
x✝ : PGame
G : PGame := x✝
i : LeftMoves G
⊢ (invImage (fun a => a) instWellFoundedRelationPGame).1 (moveLeft G i) x✝
[PROOFSTEP]
pgame_wf_tac
[GOAL]
G : PGame
⊢ grundyValue G = mex fun i => grundyValue (moveLeft G i)
[PROOFSTEP]
rw [grundyValue]
[GOAL]
x✝ : PGame
inst✝ : Impartial x✝
G : PGame := x✝
⊢ x✝ ≈ nim (grundyValue x✝)
[PROOFSTEP]
rw [Impartial.equiv_iff_add_equiv_zero, ← Impartial.forall_leftMoves_fuzzy_iff_equiv_zero]
[GOAL]
x✝ : PGame
inst✝ : Impartial x✝
G : PGame := x✝
⊢ ∀ (i : LeftMoves (x✝ + nim (grundyValue x✝))), moveLeft (x✝ + nim (grundyValue x✝)) i ‖ 0
[PROOFSTEP]
intro i
[GOAL]
x✝ : PGame
inst✝ : Impartial x✝
G : PGame := x✝
i : LeftMoves (x✝ + nim (grundyValue x✝))
⊢ moveLeft (x✝ + nim (grundyValue x✝)) i ‖ 0
[PROOFSTEP]
apply leftMoves_add_cases i
[GOAL]
case hl
x✝ : PGame
inst✝ : Impartial x✝
G : PGame := x✝
i : LeftMoves (x✝ + nim (grundyValue x✝))
⊢ ∀ (i : LeftMoves x✝), moveLeft (x✝ + nim (grundyValue x✝)) (↑toLeftMovesAdd (Sum.inl i)) ‖ 0
[PROOFSTEP]
intro i₁
[GOAL]
case hl
x✝ : PGame
inst✝ : Impartial x✝
G : PGame := x✝
i : LeftMoves (x✝ + nim (grundyValue x✝))
i₁ : LeftMoves x✝
⊢ moveLeft (x✝ + nim (grundyValue x✝)) (↑toLeftMovesAdd (Sum.inl i₁)) ‖ 0
[PROOFSTEP]
rw [add_moveLeft_inl]
[GOAL]
case hl
x✝ : PGame
inst✝ : Impartial x✝
G : PGame := x✝
i : LeftMoves (x✝ + nim (grundyValue x✝))
i₁ : LeftMoves x✝
⊢ moveLeft x✝ i₁ + nim (grundyValue x✝) ‖ 0
[PROOFSTEP]
apply (fuzzy_congr_left (add_congr_left (Equiv.symm (equiv_nim_grundyValue (G.moveLeft i₁))))).1
[GOAL]
case hl
x✝ : PGame
inst✝ : Impartial x✝
G : PGame := x✝
i : LeftMoves (x✝ + nim (grundyValue x✝))
i₁ : LeftMoves x✝
⊢ nim (grundyValue (moveLeft G i₁)) + nim (grundyValue x✝) ‖ 0
[PROOFSTEP]
rw [nim_add_fuzzy_zero_iff]
[GOAL]
case hl
x✝ : PGame
inst✝ : Impartial x✝
G : PGame := x✝
i : LeftMoves (x✝ + nim (grundyValue x✝))
i₁ : LeftMoves x✝
⊢ grundyValue (moveLeft G i₁) ≠ grundyValue x✝
[PROOFSTEP]
intro heq
[GOAL]
case hl
x✝ : PGame
inst✝ : Impartial x✝
G : PGame := x✝
i : LeftMoves (x✝ + nim (grundyValue x✝))
i₁ : LeftMoves x✝
heq : grundyValue (moveLeft G i₁) = grundyValue x✝
⊢ False
[PROOFSTEP]
rw [eq_comm, grundyValue_eq_mex_left G] at heq 
[GOAL]
case hl
x✝ : PGame
inst✝ : Impartial x✝
G : PGame := x✝
i : LeftMoves (x✝ + nim (grundyValue x✝))
i₁ : LeftMoves x✝
heq : (mex fun i => grundyValue (moveLeft G i)) = grundyValue (moveLeft G i₁)
⊢ False
[PROOFSTEP]
have h := Ordinal.ne_mex.{u, u} (fun i ↦ grundyValue (moveLeft G i))
[GOAL]
case hl
x✝ : PGame
inst✝ : Impartial x✝
G : PGame := x✝
i : LeftMoves (x✝ + nim (grundyValue x✝))
i₁ : LeftMoves x✝
heq : (mex fun i => grundyValue (moveLeft G i)) = grundyValue (moveLeft G i₁)
h : ∀ (i : LeftMoves G), grundyValue (moveLeft G i) ≠ mex fun i => grundyValue (moveLeft G i)
⊢ False
[PROOFSTEP]
rw [heq] at h 
[GOAL]
case hl
x✝ : PGame
inst✝ : Impartial x✝
G : PGame := x✝
i : LeftMoves (x✝ + nim (grundyValue x✝))
i₁ : LeftMoves x✝
heq : (mex fun i => grundyValue (moveLeft G i)) = grundyValue (moveLeft G i₁)
h : ∀ (i : LeftMoves G), grundyValue (moveLeft G i) ≠ grundyValue (moveLeft G i₁)
⊢ False
[PROOFSTEP]
exact (h i₁).irrefl
[GOAL]
case hr
x✝ : PGame
inst✝ : Impartial x✝
G : PGame := x✝
i : LeftMoves (x✝ + nim (grundyValue x✝))
⊢ ∀ (i : LeftMoves (nim (grundyValue x✝))), moveLeft (x✝ + nim (grundyValue x✝)) (↑toLeftMovesAdd (Sum.inr i)) ‖ 0
[PROOFSTEP]
intro i₂
[GOAL]
case hr
x✝ : PGame
inst✝ : Impartial x✝
G : PGame := x✝
i : LeftMoves (x✝ + nim (grundyValue x✝))
i₂ : LeftMoves (nim (grundyValue x✝))
⊢ moveLeft (x✝ + nim (grundyValue x✝)) (↑toLeftMovesAdd (Sum.inr i₂)) ‖ 0
[PROOFSTEP]
rw [add_moveLeft_inr, ← Impartial.exists_left_move_equiv_iff_fuzzy_zero]
[GOAL]
case hr
x✝ : PGame
inst✝ : Impartial x✝
G : PGame := x✝
i : LeftMoves (x✝ + nim (grundyValue x✝))
i₂ : LeftMoves (nim (grundyValue x✝))
⊢ ∃ i, moveLeft (x✝ + moveLeft (nim (grundyValue x✝)) i₂) i ≈ 0
[PROOFSTEP]
revert i₂
[GOAL]
case hr
x✝ : PGame
inst✝ : Impartial x✝
G : PGame := x✝
i : LeftMoves (x✝ + nim (grundyValue x✝))
⊢ ∀ (i₂ : LeftMoves (nim (grundyValue x✝))), ∃ i, moveLeft (x✝ + moveLeft (nim (grundyValue x✝)) i₂) i ≈ 0
[PROOFSTEP]
rw [nim_def]
[GOAL]
case hr
x✝ : PGame
inst✝ : Impartial x✝
G : PGame := x✝
i : LeftMoves (x✝ + nim (grundyValue x✝))
⊢ ∀
    (i₂ :
      LeftMoves
        (mk (Quotient.out (grundyValue x✝)).α (Quotient.out (grundyValue x✝)).α
          (fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)) fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂))),
    ∃ i,
      moveLeft
          (x✝ +
            moveLeft
              (mk (Quotient.out (grundyValue x✝)).α (Quotient.out (grundyValue x✝)).α
                (fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)) fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂))
              i₂)
          i ≈
        0
[PROOFSTEP]
intro i₂
[GOAL]
case hr
x✝ : PGame
inst✝ : Impartial x✝
G : PGame := x✝
i : LeftMoves (x✝ + nim (grundyValue x✝))
i₂ :
  LeftMoves
    (mk (Quotient.out (grundyValue x✝)).α (Quotient.out (grundyValue x✝)).α
      (fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)) fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂))
⊢ ∃ i,
    moveLeft
        (x✝ +
          moveLeft
            (mk (Quotient.out (grundyValue x✝)).α (Quotient.out (grundyValue x✝)).α
              (fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)) fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂))
            i₂)
        i ≈
      0
[PROOFSTEP]
have h' : ∃ i : G.LeftMoves, grundyValue (G.moveLeft i) = Ordinal.typein (Quotient.out (grundyValue G)).r i₂ :=
  by
  revert i₂
  rw [grundyValue_eq_mex_left]
  intro i₂
  have hnotin : _ ∉ _ := fun hin => (le_not_le_of_lt (Ordinal.typein_lt_self i₂)).2 (csInf_le' hin)
  simpa using hnotin
[GOAL]
x✝ : PGame
inst✝ : Impartial x✝
G : PGame := x✝
i : LeftMoves (x✝ + nim (grundyValue x✝))
i₂ :
  LeftMoves
    (mk (Quotient.out (grundyValue x✝)).α (Quotient.out (grundyValue x✝)).α
      (fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)) fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂))
⊢ ∃ i, grundyValue (moveLeft G i) = typein (Quotient.out (grundyValue G)).r i₂
[PROOFSTEP]
revert i₂
[GOAL]
x✝ : PGame
inst✝ : Impartial x✝
G : PGame := x✝
i : LeftMoves (x✝ + nim (grundyValue x✝))
⊢ ∀
    (i₂ :
      LeftMoves
        (mk (Quotient.out (grundyValue x✝)).α (Quotient.out (grundyValue x✝)).α
          (fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)) fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂))),
    ∃ i, grundyValue (moveLeft G i) = typein (Quotient.out (grundyValue G)).r i₂
[PROOFSTEP]
rw [grundyValue_eq_mex_left]
[GOAL]
x✝ : PGame
inst✝ : Impartial x✝
G : PGame := x✝
i : LeftMoves (x✝ + nim (grundyValue x✝))
⊢ ∀
    (i₂ :
      LeftMoves
        (mk (Quotient.out (mex fun i => grundyValue (moveLeft x✝ i))).α
          (Quotient.out (mex fun i => grundyValue (moveLeft x✝ i))).α (fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂))
          fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂))),
    ∃ i, grundyValue (moveLeft G i) = typein (Quotient.out (mex fun i => grundyValue (moveLeft x✝ i))).r i₂
[PROOFSTEP]
intro i₂
[GOAL]
x✝ : PGame
inst✝ : Impartial x✝
G : PGame := x✝
i : LeftMoves (x✝ + nim (grundyValue x✝))
i₂ :
  LeftMoves
    (mk (Quotient.out (mex fun i => grundyValue (moveLeft x✝ i))).α
      (Quotient.out (mex fun i => grundyValue (moveLeft x✝ i))).α (fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂))
      fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂))
⊢ ∃ i, grundyValue (moveLeft G i) = typein (Quotient.out (mex fun i => grundyValue (moveLeft x✝ i))).r i₂
[PROOFSTEP]
have hnotin : _ ∉ _ := fun hin => (le_not_le_of_lt (Ordinal.typein_lt_self i₂)).2 (csInf_le' hin)
[GOAL]
x✝ : PGame
inst✝ : Impartial x✝
G : PGame := x✝
i : LeftMoves (x✝ + nim (grundyValue x✝))
i₂ :
  LeftMoves
    (mk (Quotient.out (mex fun i => grundyValue (moveLeft x✝ i))).α
      (Quotient.out (mex fun i => grundyValue (moveLeft x✝ i))).α (fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂))
      fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂))
hnotin : ¬typein (fun x x_1 => x < x_1) i₂ ∈ (Set.range fun i => grundyValue (moveLeft x✝ i))ᶜ
⊢ ∃ i, grundyValue (moveLeft G i) = typein (Quotient.out (mex fun i => grundyValue (moveLeft x✝ i))).r i₂
[PROOFSTEP]
simpa using hnotin
[GOAL]
case hr
x✝ : PGame
inst✝ : Impartial x✝
G : PGame := x✝
i : LeftMoves (x✝ + nim (grundyValue x✝))
i₂ :
  LeftMoves
    (mk (Quotient.out (grundyValue x✝)).α (Quotient.out (grundyValue x✝)).α
      (fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)) fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂))
h' : ∃ i, grundyValue (moveLeft G i) = typein (Quotient.out (grundyValue G)).r i₂
⊢ ∃ i,
    moveLeft
        (x✝ +
          moveLeft
            (mk (Quotient.out (grundyValue x✝)).α (Quotient.out (grundyValue x✝)).α
              (fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)) fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂))
            i₂)
        i ≈
      0
[PROOFSTEP]
cases' h' with i hi
[GOAL]
case hr.intro
x✝ : PGame
inst✝ : Impartial x✝
G : PGame := x✝
i✝ : LeftMoves (x✝ + nim (grundyValue x✝))
i₂ :
  LeftMoves
    (mk (Quotient.out (grundyValue x✝)).α (Quotient.out (grundyValue x✝)).α
      (fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)) fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂))
i : LeftMoves G
hi : grundyValue (moveLeft G i) = typein (Quotient.out (grundyValue G)).r i₂
⊢ ∃ i,
    moveLeft
        (x✝ +
          moveLeft
            (mk (Quotient.out (grundyValue x✝)).α (Quotient.out (grundyValue x✝)).α
              (fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)) fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂))
            i₂)
        i ≈
      0
[PROOFSTEP]
use toLeftMovesAdd (Sum.inl i)
[GOAL]
case h
x✝ : PGame
inst✝ : Impartial x✝
G : PGame := x✝
i✝ : LeftMoves (x✝ + nim (grundyValue x✝))
i₂ :
  LeftMoves
    (mk (Quotient.out (grundyValue x✝)).α (Quotient.out (grundyValue x✝)).α
      (fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)) fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂))
i : LeftMoves G
hi : grundyValue (moveLeft G i) = typein (Quotient.out (grundyValue G)).r i₂
⊢ moveLeft
      (x✝ +
        moveLeft
          (mk (Quotient.out (grundyValue x✝)).α (Quotient.out (grundyValue x✝)).α
            (fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)) fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂))
          i₂)
      (↑toLeftMovesAdd (Sum.inl i)) ≈
    0
[PROOFSTEP]
rw [add_moveLeft_inl, moveLeft_mk]
[GOAL]
case h
x✝ : PGame
inst✝ : Impartial x✝
G : PGame := x✝
i✝ : LeftMoves (x✝ + nim (grundyValue x✝))
i₂ :
  LeftMoves
    (mk (Quotient.out (grundyValue x✝)).α (Quotient.out (grundyValue x✝)).α
      (fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)) fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂))
i : LeftMoves G
hi : grundyValue (moveLeft G i) = typein (Quotient.out (grundyValue G)).r i₂
⊢ moveLeft x✝ i + nim (typein (fun x x_1 => x < x_1) i₂) ≈ 0
[PROOFSTEP]
apply Equiv.trans (add_congr_left (equiv_nim_grundyValue (G.moveLeft i)))
[GOAL]
case h
x✝ : PGame
inst✝ : Impartial x✝
G : PGame := x✝
i✝ : LeftMoves (x✝ + nim (grundyValue x✝))
i₂ :
  LeftMoves
    (mk (Quotient.out (grundyValue x✝)).α (Quotient.out (grundyValue x✝)).α
      (fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)) fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂))
i : LeftMoves G
hi : grundyValue (moveLeft G i) = typein (Quotient.out (grundyValue G)).r i₂
⊢ nim (grundyValue (moveLeft G i)) + nim (typein (fun x x_1 => x < x_1) i₂) ≈ 0
[PROOFSTEP]
simpa only [hi] using Impartial.add_self (nim (grundyValue (G.moveLeft i)))
[GOAL]
x✝ : PGame
inst✝ : Impartial x✝
a✝ :
  ∀ (y : (x : PGame) ×' Impartial x),
    (invImage (fun a => PSigma.casesOn a fun G snd => G) instWellFoundedRelationPGame).1 y { fst := x✝, snd := inst✝ } →
      y.1 ≈ nim (grundyValue y.1)
G : PGame := x✝
i₁ : LeftMoves x✝
⊢ (invImage (fun a => PSigma.casesOn a fun G snd => G) instWellFoundedRelationPGame).1
    { fst := moveLeft G i₁, snd := (_ : Impartial (moveLeft G i₁)) } { fst := x✝, snd := inst✝ }
[PROOFSTEP]
pgame_wf_tac
[GOAL]
x✝ : PGame
inst✝ : Impartial x✝
a✝ :
  ∀ (y : (x : PGame) ×' Impartial x),
    (invImage (fun a => PSigma.casesOn a fun G snd => G) instWellFoundedRelationPGame).1 y { fst := x✝, snd := inst✝ } →
      y.1 ≈ nim (grundyValue y.1)
G : PGame := x✝
i₂ :
  LeftMoves
    (mk (Quotient.out (grundyValue x✝)).α (Quotient.out (grundyValue x✝)).α
      (fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂)) fun o₂ => nim (typein (fun x x_1 => x < x_1) o₂))
h' : ∃ i, grundyValue (moveLeft G i) = typein (Quotient.out (grundyValue G)).r i₂
i : LeftMoves G
hi : grundyValue (moveLeft G i) = typein (Quotient.out (grundyValue G)).r i₂
h✝ : h' = (_ : ∃ i, grundyValue (moveLeft G i) = typein (Quotient.out (grundyValue G)).r i₂)
⊢ (invImage (fun a => PSigma.casesOn a fun G snd => G) instWellFoundedRelationPGame).1
    { fst := moveLeft G i, snd := (_ : Impartial (moveLeft G i)) } { fst := x✝, snd := inst✝ }
[PROOFSTEP]
pgame_wf_tac
[GOAL]
G : PGame
inst✝ : Impartial G
o : Ordinal.{u_1}
⊢ grundyValue G = o → G ≈ nim o
[PROOFSTEP]
rintro rfl
[GOAL]
G : PGame
inst✝ : Impartial G
⊢ G ≈ nim (grundyValue G)
[PROOFSTEP]
exact equiv_nim_grundyValue G
[GOAL]
G : PGame
inst✝ : Impartial G
o : Ordinal.{u_1}
⊢ G ≈ nim o → grundyValue G = o
[PROOFSTEP]
intro h
[GOAL]
G : PGame
inst✝ : Impartial G
o : Ordinal.{u_1}
h : G ≈ nim o
⊢ grundyValue G = o
[PROOFSTEP]
rw [← nim_equiv_iff_eq]
[GOAL]
G : PGame
inst✝ : Impartial G
o : Ordinal.{u_1}
h : G ≈ nim o
⊢ nim (grundyValue G) ≈ nim o
[PROOFSTEP]
exact Equiv.trans (Equiv.symm (equiv_nim_grundyValue G)) h
[GOAL]
G : PGame
inst✝ : Impartial G
⊢ grundyValue G = 0 ↔ G ≈ 0
[PROOFSTEP]
rw [← grundyValue_eq_iff_equiv, grundyValue_zero]
[GOAL]
G : PGame
inst✝ : Impartial G
⊢ grundyValue (-G) = grundyValue G
[PROOFSTEP]
rw [grundyValue_eq_iff_equiv_nim, neg_equiv_iff, neg_nim, ← grundyValue_eq_iff_equiv_nim]
[GOAL]
l r : Type u
L : l → PGame
R : r → PGame
x✝ : Impartial (mk l r L R)
⊢ grundyValue (mk l r L R) = mex fun i => grundyValue (moveRight (mk l r L R) i)
[PROOFSTEP]
rw [← grundyValue_neg, grundyValue_eq_mex_left]
[GOAL]
l r : Type u
L : l → PGame
R : r → PGame
x✝ : Impartial (mk l r L R)
⊢ (mex fun i => grundyValue (moveLeft (-mk l r L R) i)) = mex fun i => grundyValue (moveRight (mk l r L R) i)
[PROOFSTEP]
congr
[GOAL]
case e_f
l r : Type u
L : l → PGame
R : r → PGame
x✝ : Impartial (mk l r L R)
⊢ (fun i => grundyValue (moveLeft (-mk l r L R) i)) = fun i => grundyValue (moveRight (mk l r L R) i)
[PROOFSTEP]
ext i
[GOAL]
case e_f.h
l r : Type u
L : l → PGame
R : r → PGame
x✝ : Impartial (mk l r L R)
i : LeftMoves (-mk l r L R)
⊢ grundyValue (moveLeft (-mk l r L R) i) = grundyValue (moveRight (mk l r L R) i)
[PROOFSTEP]
haveI : (R i).Impartial := @Impartial.moveRight_impartial ⟨l, r, L, R⟩ _ i
[GOAL]
case e_f.h
l r : Type u
L : l → PGame
R : r → PGame
x✝ : Impartial (mk l r L R)
i : LeftMoves (-mk l r L R)
this : Impartial (R i)
⊢ grundyValue (moveLeft (-mk l r L R) i) = grundyValue (moveRight (mk l r L R) i)
[PROOFSTEP]
apply grundyValue_neg
[GOAL]
n m : ℕ
⊢ grundyValue (nim ↑n + nim ↑m) = ↑(Nat.lxor' n m)
[PROOFSTEP]
induction' n using Nat.strong_induction_on with n hn generalizing m
[GOAL]
case h
m✝ n : ℕ
hn : ∀ (m : ℕ), m < n → ∀ (m_1 : ℕ), grundyValue (nim ↑m + nim ↑m_1) = ↑(Nat.lxor' m m_1)
m : ℕ
⊢ grundyValue (nim ↑n + nim ↑m) = ↑(Nat.lxor' n m)
[PROOFSTEP]
induction' m using Nat.strong_induction_on with m hm
[GOAL]
case h.h
m✝ n : ℕ
hn : ∀ (m : ℕ), m < n → ∀ (m_1 : ℕ), grundyValue (nim ↑m + nim ↑m_1) = ↑(Nat.lxor' m m_1)
m : ℕ
hm : ∀ (m_1 : ℕ), m_1 < m → grundyValue (nim ↑n + nim ↑m_1) = ↑(Nat.lxor' n m_1)
⊢ grundyValue (nim ↑n + nim ↑m) = ↑(Nat.lxor' n m)
[PROOFSTEP]
rw [grundyValue_eq_mex_left]
[GOAL]
case h.h
m✝ n : ℕ
hn : ∀ (m : ℕ), m < n → ∀ (m_1 : ℕ), grundyValue (nim ↑m + nim ↑m_1) = ↑(Nat.lxor' m m_1)
m : ℕ
hm : ∀ (m_1 : ℕ), m_1 < m → grundyValue (nim ↑n + nim ↑m_1) = ↑(Nat.lxor' n m_1)
⊢ (mex fun i => grundyValue (moveLeft (nim ↑n + nim ↑m) i)) = ↑(Nat.lxor' n m)
[PROOFSTEP]
refine
  (Ordinal.mex_le_of_ne.{u, u} fun i => ?_).antisymm
    (Ordinal.le_mex_of_forall fun ou hu => ?_)
      -- The Grundy value `Nat.lxor' n m` can't be reached by left moves.
[GOAL]
case h.h.refine_1
m✝ n : ℕ
hn : ∀ (m : ℕ), m < n → ∀ (m_1 : ℕ), grundyValue (nim ↑m + nim ↑m_1) = ↑(Nat.lxor' m m_1)
m : ℕ
hm : ∀ (m_1 : ℕ), m_1 < m → grundyValue (nim ↑n + nim ↑m_1) = ↑(Nat.lxor' n m_1)
i : LeftMoves (nim ↑n + nim ↑m)
⊢ grundyValue (moveLeft (nim ↑n + nim ↑m) i) ≠ ↑(Nat.lxor' n m)
[PROOFSTEP]
apply leftMoves_add_cases i
[GOAL]
case h.h.refine_1.hl
m✝ n : ℕ
hn : ∀ (m : ℕ), m < n → ∀ (m_1 : ℕ), grundyValue (nim ↑m + nim ↑m_1) = ↑(Nat.lxor' m m_1)
m : ℕ
hm : ∀ (m_1 : ℕ), m_1 < m → grundyValue (nim ↑n + nim ↑m_1) = ↑(Nat.lxor' n m_1)
i : LeftMoves (nim ↑n + nim ↑m)
⊢ ∀ (i : LeftMoves (nim ↑n)), grundyValue (moveLeft (nim ↑n + nim ↑m) (↑toLeftMovesAdd (Sum.inl i))) ≠ ↑(Nat.lxor' n m)
[PROOFSTEP]
refine' fun a => leftMovesNimRecOn a fun ok hk => _
[GOAL]
case h.h.refine_1.hl
m✝ n : ℕ
hn : ∀ (m : ℕ), m < n → ∀ (m_1 : ℕ), grundyValue (nim ↑m + nim ↑m_1) = ↑(Nat.lxor' m m_1)
m : ℕ
hm : ∀ (m_1 : ℕ), m_1 < m → grundyValue (nim ↑n + nim ↑m_1) = ↑(Nat.lxor' n m_1)
i : LeftMoves (nim ↑n + nim ↑m)
a : LeftMoves (nim ↑n)
ok : Ordinal.{u}
hk : ok < ↑n
⊢ grundyValue (moveLeft (nim ↑n + nim ↑m) (↑toLeftMovesAdd (Sum.inl (↑toLeftMovesNim { val := ok, property := hk })))) ≠
    ↑(Nat.lxor' n m)
[PROOFSTEP]
obtain ⟨k, rfl⟩ := Ordinal.lt_omega.1 (hk.trans (Ordinal.nat_lt_omega _))
[GOAL]
case h.h.refine_1.hl.intro
m✝ n : ℕ
hn : ∀ (m : ℕ), m < n → ∀ (m_1 : ℕ), grundyValue (nim ↑m + nim ↑m_1) = ↑(Nat.lxor' m m_1)
m : ℕ
hm : ∀ (m_1 : ℕ), m_1 < m → grundyValue (nim ↑n + nim ↑m_1) = ↑(Nat.lxor' n m_1)
i : LeftMoves (nim ↑n + nim ↑m)
a : LeftMoves (nim ↑n)
k : ℕ
hk : ↑k < ↑n
⊢ grundyValue (moveLeft (nim ↑n + nim ↑m) (↑toLeftMovesAdd (Sum.inl (↑toLeftMovesNim { val := ↑k, property := hk })))) ≠
    ↑(Nat.lxor' n m)
[PROOFSTEP]
simp only [add_moveLeft_inl, add_moveLeft_inr, moveLeft_nim', Equiv.symm_apply_apply]
  -- The inequality follows from injectivity.
[GOAL]
case h.h.refine_1.hl.intro
m✝ n : ℕ
hn : ∀ (m : ℕ), m < n → ∀ (m_1 : ℕ), grundyValue (nim ↑m + nim ↑m_1) = ↑(Nat.lxor' m m_1)
m : ℕ
hm : ∀ (m_1 : ℕ), m_1 < m → grundyValue (nim ↑n + nim ↑m_1) = ↑(Nat.lxor' n m_1)
i : LeftMoves (nim ↑n + nim ↑m)
a : LeftMoves (nim ↑n)
k : ℕ
hk : ↑k < ↑n
⊢ grundyValue (nim ↑k + nim ↑m) ≠ ↑(Nat.lxor' n m)
[PROOFSTEP]
rw [nat_cast_lt] at hk 
[GOAL]
case h.h.refine_1.hl.intro
m✝ n : ℕ
hn : ∀ (m : ℕ), m < n → ∀ (m_1 : ℕ), grundyValue (nim ↑m + nim ↑m_1) = ↑(Nat.lxor' m m_1)
m : ℕ
hm : ∀ (m_1 : ℕ), m_1 < m → grundyValue (nim ↑n + nim ↑m_1) = ↑(Nat.lxor' n m_1)
i : LeftMoves (nim ↑n + nim ↑m)
a : LeftMoves (nim ↑n)
k : ℕ
hk : k < n
⊢ grundyValue (nim ↑k + nim ↑m) ≠ ↑(Nat.lxor' n m)
[PROOFSTEP]
first
| rw [hn _ hk]
| rw [hm _ hk]
[GOAL]
case h.h.refine_1.hl.intro
m✝ n : ℕ
hn : ∀ (m : ℕ), m < n → ∀ (m_1 : ℕ), grundyValue (nim ↑m + nim ↑m_1) = ↑(Nat.lxor' m m_1)
m : ℕ
hm : ∀ (m_1 : ℕ), m_1 < m → grundyValue (nim ↑n + nim ↑m_1) = ↑(Nat.lxor' n m_1)
i : LeftMoves (nim ↑n + nim ↑m)
a : LeftMoves (nim ↑n)
k : ℕ
hk : k < n
⊢ grundyValue (nim ↑k + nim ↑m) ≠ ↑(Nat.lxor' n m)
[PROOFSTEP]
rw [hn _ hk]
[GOAL]
case h.h.refine_1.hl.intro
m✝ n : ℕ
hn : ∀ (m : ℕ), m < n → ∀ (m_1 : ℕ), grundyValue (nim ↑m + nim ↑m_1) = ↑(Nat.lxor' m m_1)
m : ℕ
hm : ∀ (m_1 : ℕ), m_1 < m → grundyValue (nim ↑n + nim ↑m_1) = ↑(Nat.lxor' n m_1)
i : LeftMoves (nim ↑n + nim ↑m)
a : LeftMoves (nim ↑n)
k : ℕ
hk : k < n
⊢ ↑(Nat.lxor' k m) ≠ ↑(Nat.lxor' n m)
[PROOFSTEP]
refine' fun h => hk.ne _
[GOAL]
case h.h.refine_1.hl.intro
m✝ n : ℕ
hn : ∀ (m : ℕ), m < n → ∀ (m_1 : ℕ), grundyValue (nim ↑m + nim ↑m_1) = ↑(Nat.lxor' m m_1)
m : ℕ
hm : ∀ (m_1 : ℕ), m_1 < m → grundyValue (nim ↑n + nim ↑m_1) = ↑(Nat.lxor' n m_1)
i : LeftMoves (nim ↑n + nim ↑m)
a : LeftMoves (nim ↑n)
k : ℕ
hk : k < n
h : ↑(Nat.lxor' k m) = ↑(Nat.lxor' n m)
⊢ k = n
[PROOFSTEP]
rw [Ordinal.nat_cast_inj] at h 
[GOAL]
case h.h.refine_1.hl.intro
m✝ n : ℕ
hn : ∀ (m : ℕ), m < n → ∀ (m_1 : ℕ), grundyValue (nim ↑m + nim ↑m_1) = ↑(Nat.lxor' m m_1)
m : ℕ
hm : ∀ (m_1 : ℕ), m_1 < m → grundyValue (nim ↑n + nim ↑m_1) = ↑(Nat.lxor' n m_1)
i : LeftMoves (nim ↑n + nim ↑m)
a : LeftMoves (nim ↑n)
k : ℕ
hk : k < n
h : Nat.lxor' k m = Nat.lxor' n m
⊢ k = n
[PROOFSTEP]
first
| rwa [Nat.lxor'_left_inj] at h 
| rwa [Nat.lxor'_right_inj] at h 
[GOAL]
case h.h.refine_1.hl.intro
m✝ n : ℕ
hn : ∀ (m : ℕ), m < n → ∀ (m_1 : ℕ), grundyValue (nim ↑m + nim ↑m_1) = ↑(Nat.lxor' m m_1)
m : ℕ
hm : ∀ (m_1 : ℕ), m_1 < m → grundyValue (nim ↑n + nim ↑m_1) = ↑(Nat.lxor' n m_1)
i : LeftMoves (nim ↑n + nim ↑m)
a : LeftMoves (nim ↑n)
k : ℕ
hk : k < n
h : Nat.lxor' k m = Nat.lxor' n m
⊢ k = n
[PROOFSTEP]
rwa [Nat.lxor'_left_inj] at h 
[GOAL]
case h.h.refine_1.hr
m✝ n : ℕ
hn : ∀ (m : ℕ), m < n → ∀ (m_1 : ℕ), grundyValue (nim ↑m + nim ↑m_1) = ↑(Nat.lxor' m m_1)
m : ℕ
hm : ∀ (m_1 : ℕ), m_1 < m → grundyValue (nim ↑n + nim ↑m_1) = ↑(Nat.lxor' n m_1)
i : LeftMoves (nim ↑n + nim ↑m)
⊢ ∀ (i : LeftMoves (nim ↑m)), grundyValue (moveLeft (nim ↑n + nim ↑m) (↑toLeftMovesAdd (Sum.inr i))) ≠ ↑(Nat.lxor' n m)
[PROOFSTEP]
refine' fun a => leftMovesNimRecOn a fun ok hk => _
[GOAL]
case h.h.refine_1.hr
m✝ n : ℕ
hn : ∀ (m : ℕ), m < n → ∀ (m_1 : ℕ), grundyValue (nim ↑m + nim ↑m_1) = ↑(Nat.lxor' m m_1)
m : ℕ
hm : ∀ (m_1 : ℕ), m_1 < m → grundyValue (nim ↑n + nim ↑m_1) = ↑(Nat.lxor' n m_1)
i : LeftMoves (nim ↑n + nim ↑m)
a : LeftMoves (nim ↑m)
ok : Ordinal.{u}
hk : ok < ↑m
⊢ grundyValue (moveLeft (nim ↑n + nim ↑m) (↑toLeftMovesAdd (Sum.inr (↑toLeftMovesNim { val := ok, property := hk })))) ≠
    ↑(Nat.lxor' n m)
[PROOFSTEP]
obtain ⟨k, rfl⟩ := Ordinal.lt_omega.1 (hk.trans (Ordinal.nat_lt_omega _))
[GOAL]
case h.h.refine_1.hr.intro
m✝ n : ℕ
hn : ∀ (m : ℕ), m < n → ∀ (m_1 : ℕ), grundyValue (nim ↑m + nim ↑m_1) = ↑(Nat.lxor' m m_1)
m : ℕ
hm : ∀ (m_1 : ℕ), m_1 < m → grundyValue (nim ↑n + nim ↑m_1) = ↑(Nat.lxor' n m_1)
i : LeftMoves (nim ↑n + nim ↑m)
a : LeftMoves (nim ↑m)
k : ℕ
hk : ↑k < ↑m
⊢ grundyValue (moveLeft (nim ↑n + nim ↑m) (↑toLeftMovesAdd (Sum.inr (↑toLeftMovesNim { val := ↑k, property := hk })))) ≠
    ↑(Nat.lxor' n m)
[PROOFSTEP]
simp only [add_moveLeft_inl, add_moveLeft_inr, moveLeft_nim', Equiv.symm_apply_apply]
  -- The inequality follows from injectivity.
[GOAL]
case h.h.refine_1.hr.intro
m✝ n : ℕ
hn : ∀ (m : ℕ), m < n → ∀ (m_1 : ℕ), grundyValue (nim ↑m + nim ↑m_1) = ↑(Nat.lxor' m m_1)
m : ℕ
hm : ∀ (m_1 : ℕ), m_1 < m → grundyValue (nim ↑n + nim ↑m_1) = ↑(Nat.lxor' n m_1)
i : LeftMoves (nim ↑n + nim ↑m)
a : LeftMoves (nim ↑m)
k : ℕ
hk : ↑k < ↑m
⊢ grundyValue (nim ↑n + nim ↑k) ≠ ↑(Nat.lxor' n m)
[PROOFSTEP]
rw [nat_cast_lt] at hk 
[GOAL]
case h.h.refine_1.hr.intro
m✝ n : ℕ
hn : ∀ (m : ℕ), m < n → ∀ (m_1 : ℕ), grundyValue (nim ↑m + nim ↑m_1) = ↑(Nat.lxor' m m_1)
m : ℕ
hm : ∀ (m_1 : ℕ), m_1 < m → grundyValue (nim ↑n + nim ↑m_1) = ↑(Nat.lxor' n m_1)
i : LeftMoves (nim ↑n + nim ↑m)
a : LeftMoves (nim ↑m)
k : ℕ
hk : k < m
⊢ grundyValue (nim ↑n + nim ↑k) ≠ ↑(Nat.lxor' n m)
[PROOFSTEP]
first
| rw [hn _ hk]
| rw [hm _ hk]
[GOAL]
case h.h.refine_1.hr.intro
m✝ n : ℕ
hn : ∀ (m : ℕ), m < n → ∀ (m_1 : ℕ), grundyValue (nim ↑m + nim ↑m_1) = ↑(Nat.lxor' m m_1)
m : ℕ
hm : ∀ (m_1 : ℕ), m_1 < m → grundyValue (nim ↑n + nim ↑m_1) = ↑(Nat.lxor' n m_1)
i : LeftMoves (nim ↑n + nim ↑m)
a : LeftMoves (nim ↑m)
k : ℕ
hk : k < m
⊢ grundyValue (nim ↑n + nim ↑k) ≠ ↑(Nat.lxor' n m)
[PROOFSTEP]
rw [hn _ hk]
[GOAL]
case h.h.refine_1.hr.intro
m✝ n : ℕ
hn : ∀ (m : ℕ), m < n → ∀ (m_1 : ℕ), grundyValue (nim ↑m + nim ↑m_1) = ↑(Nat.lxor' m m_1)
m : ℕ
hm : ∀ (m_1 : ℕ), m_1 < m → grundyValue (nim ↑n + nim ↑m_1) = ↑(Nat.lxor' n m_1)
i : LeftMoves (nim ↑n + nim ↑m)
a : LeftMoves (nim ↑m)
k : ℕ
hk : k < m
⊢ grundyValue (nim ↑n + nim ↑k) ≠ ↑(Nat.lxor' n m)
[PROOFSTEP]
rw [hm _ hk]
[GOAL]
case h.h.refine_1.hr.intro
m✝ n : ℕ
hn : ∀ (m : ℕ), m < n → ∀ (m_1 : ℕ), grundyValue (nim ↑m + nim ↑m_1) = ↑(Nat.lxor' m m_1)
m : ℕ
hm : ∀ (m_1 : ℕ), m_1 < m → grundyValue (nim ↑n + nim ↑m_1) = ↑(Nat.lxor' n m_1)
i : LeftMoves (nim ↑n + nim ↑m)
a : LeftMoves (nim ↑m)
k : ℕ
hk : k < m
⊢ ↑(Nat.lxor' n k) ≠ ↑(Nat.lxor' n m)
[PROOFSTEP]
refine' fun h => hk.ne _
[GOAL]
case h.h.refine_1.hr.intro
m✝ n : ℕ
hn : ∀ (m : ℕ), m < n → ∀ (m_1 : ℕ), grundyValue (nim ↑m + nim ↑m_1) = ↑(Nat.lxor' m m_1)
m : ℕ
hm : ∀ (m_1 : ℕ), m_1 < m → grundyValue (nim ↑n + nim ↑m_1) = ↑(Nat.lxor' n m_1)
i : LeftMoves (nim ↑n + nim ↑m)
a : LeftMoves (nim ↑m)
k : ℕ
hk : k < m
h : ↑(Nat.lxor' n k) = ↑(Nat.lxor' n m)
⊢ k = m
[PROOFSTEP]
rw [Ordinal.nat_cast_inj] at h 
[GOAL]
case h.h.refine_1.hr.intro
m✝ n : ℕ
hn : ∀ (m : ℕ), m < n → ∀ (m_1 : ℕ), grundyValue (nim ↑m + nim ↑m_1) = ↑(Nat.lxor' m m_1)
m : ℕ
hm : ∀ (m_1 : ℕ), m_1 < m → grundyValue (nim ↑n + nim ↑m_1) = ↑(Nat.lxor' n m_1)
i : LeftMoves (nim ↑n + nim ↑m)
a : LeftMoves (nim ↑m)
k : ℕ
hk : k < m
h : Nat.lxor' n k = Nat.lxor' n m
⊢ k = m
[PROOFSTEP]
first
| rwa [Nat.lxor'_left_inj] at h 
| rwa [Nat.lxor'_right_inj] at h 
[GOAL]
case h.h.refine_1.hr.intro
m✝ n : ℕ
hn : ∀ (m : ℕ), m < n → ∀ (m_1 : ℕ), grundyValue (nim ↑m + nim ↑m_1) = ↑(Nat.lxor' m m_1)
m : ℕ
hm : ∀ (m_1 : ℕ), m_1 < m → grundyValue (nim ↑n + nim ↑m_1) = ↑(Nat.lxor' n m_1)
i : LeftMoves (nim ↑n + nim ↑m)
a : LeftMoves (nim ↑m)
k : ℕ
hk : k < m
h : Nat.lxor' n k = Nat.lxor' n m
⊢ k = m
[PROOFSTEP]
rwa [Nat.lxor'_left_inj] at h 
[GOAL]
case h.h.refine_1.hr.intro
m✝ n : ℕ
hn : ∀ (m : ℕ), m < n → ∀ (m_1 : ℕ), grundyValue (nim ↑m + nim ↑m_1) = ↑(Nat.lxor' m m_1)
m : ℕ
hm : ∀ (m_1 : ℕ), m_1 < m → grundyValue (nim ↑n + nim ↑m_1) = ↑(Nat.lxor' n m_1)
i : LeftMoves (nim ↑n + nim ↑m)
a : LeftMoves (nim ↑m)
k : ℕ
hk : k < m
h : Nat.lxor' n k = Nat.lxor' n m
⊢ k = m
[PROOFSTEP]
rwa [Nat.lxor'_right_inj] at h 
[GOAL]
case h.h.refine_2
m✝ n : ℕ
hn : ∀ (m : ℕ), m < n → ∀ (m_1 : ℕ), grundyValue (nim ↑m + nim ↑m_1) = ↑(Nat.lxor' m m_1)
m : ℕ
hm : ∀ (m_1 : ℕ), m_1 < m → grundyValue (nim ↑n + nim ↑m_1) = ↑(Nat.lxor' n m_1)
ou : Ordinal.{u}
hu : ou < ↑(Nat.lxor' n m)
⊢ ∃ i, grundyValue (moveLeft (nim ↑n + nim ↑m) i) = ou
[PROOFSTEP]
obtain ⟨u, rfl⟩ := Ordinal.lt_omega.1 (hu.trans (Ordinal.nat_lt_omega _))
[GOAL]
case h.h.refine_2.intro
m✝ n : ℕ
hn : ∀ (m : ℕ), m < n → ∀ (m_1 : ℕ), grundyValue (nim ↑m + nim ↑m_1) = ↑(Nat.lxor' m m_1)
m : ℕ
hm : ∀ (m_1 : ℕ), m_1 < m → grundyValue (nim ↑n + nim ↑m_1) = ↑(Nat.lxor' n m_1)
u : ℕ
hu : ↑u < ↑(Nat.lxor' n m)
⊢ ∃ i, grundyValue (moveLeft (nim ↑n + nim ↑m) i) = ↑u
[PROOFSTEP]
replace hu := Ordinal.nat_cast_lt.1 hu
[GOAL]
case h.h.refine_2.intro
m✝ n : ℕ
hn : ∀ (m : ℕ), m < n → ∀ (m_1 : ℕ), grundyValue (nim ↑m + nim ↑m_1) = ↑(Nat.lxor' m m_1)
m : ℕ
hm : ∀ (m_1 : ℕ), m_1 < m → grundyValue (nim ↑n + nim ↑m_1) = ↑(Nat.lxor' n m_1)
u : ℕ
hu : u < Nat.lxor' n m
⊢ ∃ i, grundyValue (moveLeft (nim ↑n + nim ↑m) i) = ↑u
[PROOFSTEP]
cases' Nat.lt_lxor'_cases hu with h h
[GOAL]
case h.h.refine_2.intro.inl
m✝ n : ℕ
hn : ∀ (m : ℕ), m < n → ∀ (m_1 : ℕ), grundyValue (nim ↑m + nim ↑m_1) = ↑(Nat.lxor' m m_1)
m : ℕ
hm : ∀ (m_1 : ℕ), m_1 < m → grundyValue (nim ↑n + nim ↑m_1) = ↑(Nat.lxor' n m_1)
u : ℕ
hu : u < Nat.lxor' n m
h : Nat.lxor' u m < n
⊢ ∃ i, grundyValue (moveLeft (nim ↑n + nim ↑m) i) = ↑u
[PROOFSTEP]
refine' ⟨toLeftMovesAdd (Sum.inl <| toLeftMovesNim ⟨_, Ordinal.nat_cast_lt.2 h⟩), _⟩
[GOAL]
case h.h.refine_2.intro.inl
m✝ n : ℕ
hn : ∀ (m : ℕ), m < n → ∀ (m_1 : ℕ), grundyValue (nim ↑m + nim ↑m_1) = ↑(Nat.lxor' m m_1)
m : ℕ
hm : ∀ (m_1 : ℕ), m_1 < m → grundyValue (nim ↑n + nim ↑m_1) = ↑(Nat.lxor' n m_1)
u : ℕ
hu : u < Nat.lxor' n m
h : Nat.lxor' u m < n
⊢ grundyValue
      (moveLeft (nim ↑n + nim ↑m)
        (↑toLeftMovesAdd
          (Sum.inl (↑toLeftMovesNim { val := ↑(Nat.lxor' u m), property := (_ : ↑(Nat.lxor' u m) < ↑n) })))) =
    ↑u
[PROOFSTEP]
simp [Nat.lxor_cancel_right, hn _ h]
  -- In the second case, reducing the `n` pile to `Nat.lxor' u m` gives the desired Grundy value.
[GOAL]
case h.h.refine_2.intro.inr
m✝ n : ℕ
hn : ∀ (m : ℕ), m < n → ∀ (m_1 : ℕ), grundyValue (nim ↑m + nim ↑m_1) = ↑(Nat.lxor' m m_1)
m : ℕ
hm : ∀ (m_1 : ℕ), m_1 < m → grundyValue (nim ↑n + nim ↑m_1) = ↑(Nat.lxor' n m_1)
u : ℕ
hu : u < Nat.lxor' n m
h : Nat.lxor' u n < m
⊢ ∃ i, grundyValue (moveLeft (nim ↑n + nim ↑m) i) = ↑u
[PROOFSTEP]
refine' ⟨toLeftMovesAdd (Sum.inr <| toLeftMovesNim ⟨_, Ordinal.nat_cast_lt.2 h⟩), _⟩
[GOAL]
case h.h.refine_2.intro.inr
m✝ n : ℕ
hn : ∀ (m : ℕ), m < n → ∀ (m_1 : ℕ), grundyValue (nim ↑m + nim ↑m_1) = ↑(Nat.lxor' m m_1)
m : ℕ
hm : ∀ (m_1 : ℕ), m_1 < m → grundyValue (nim ↑n + nim ↑m_1) = ↑(Nat.lxor' n m_1)
u : ℕ
hu : u < Nat.lxor' n m
h : Nat.lxor' u n < m
⊢ grundyValue
      (moveLeft (nim ↑n + nim ↑m)
        (↑toLeftMovesAdd
          (Sum.inr (↑toLeftMovesNim { val := ↑(Nat.lxor' u n), property := (_ : ↑(Nat.lxor' u n) < ↑m) })))) =
    ↑u
[PROOFSTEP]
have : n.lxor' (u.lxor' n) = u
[GOAL]
case this
m✝ n : ℕ
hn : ∀ (m : ℕ), m < n → ∀ (m_1 : ℕ), grundyValue (nim ↑m + nim ↑m_1) = ↑(Nat.lxor' m m_1)
m : ℕ
hm : ∀ (m_1 : ℕ), m_1 < m → grundyValue (nim ↑n + nim ↑m_1) = ↑(Nat.lxor' n m_1)
u : ℕ
hu : u < Nat.lxor' n m
h : Nat.lxor' u n < m
⊢ Nat.lxor' n (Nat.lxor' u n) = u
case h.h.refine_2.intro.inr
m✝ n : ℕ
hn : ∀ (m : ℕ), m < n → ∀ (m_1 : ℕ), grundyValue (nim ↑m + nim ↑m_1) = ↑(Nat.lxor' m m_1)
m : ℕ
hm : ∀ (m_1 : ℕ), m_1 < m → grundyValue (nim ↑n + nim ↑m_1) = ↑(Nat.lxor' n m_1)
u : ℕ
hu : u < Nat.lxor' n m
h : Nat.lxor' u n < m
this : Nat.lxor' n (Nat.lxor' u n) = u
⊢ grundyValue
      (moveLeft (nim ↑n + nim ↑m)
        (↑toLeftMovesAdd
          (Sum.inr (↑toLeftMovesNim { val := ↑(Nat.lxor' u n), property := (_ : ↑(Nat.lxor' u n) < ↑m) })))) =
    ↑u
[PROOFSTEP]
rw [Nat.lxor'_comm u, Nat.lxor'_cancel_left]
[GOAL]
case h.h.refine_2.intro.inr
m✝ n : ℕ
hn : ∀ (m : ℕ), m < n → ∀ (m_1 : ℕ), grundyValue (nim ↑m + nim ↑m_1) = ↑(Nat.lxor' m m_1)
m : ℕ
hm : ∀ (m_1 : ℕ), m_1 < m → grundyValue (nim ↑n + nim ↑m_1) = ↑(Nat.lxor' n m_1)
u : ℕ
hu : u < Nat.lxor' n m
h : Nat.lxor' u n < m
this : Nat.lxor' n (Nat.lxor' u n) = u
⊢ grundyValue
      (moveLeft (nim ↑n + nim ↑m)
        (↑toLeftMovesAdd
          (Sum.inr (↑toLeftMovesNim { val := ↑(Nat.lxor' u n), property := (_ : ↑(Nat.lxor' u n) < ↑m) })))) =
    ↑u
[PROOFSTEP]
simpa [hm _ h] using this
[GOAL]
n m : ℕ
⊢ nim ↑n + nim ↑m ≈ nim ↑(Nat.lxor' n m)
[PROOFSTEP]
rw [← grundyValue_eq_iff_equiv_nim, grundyValue_nim_add_nim]
[GOAL]
G H : PGame
inst✝¹ : Impartial G
inst✝ : Impartial H
n m : ℕ
hG : grundyValue G = ↑n
hH : grundyValue H = ↑m
⊢ grundyValue (G + H) = ↑(Nat.lxor' n m)
[PROOFSTEP]
rw [← nim_grundyValue (Nat.lxor' n m), grundyValue_eq_iff_equiv]
[GOAL]
G H : PGame
inst✝¹ : Impartial G
inst✝ : Impartial H
n m : ℕ
hG : grundyValue G = ↑n
hH : grundyValue H = ↑m
⊢ G + H ≈ nim ↑(Nat.lxor' n m)
[PROOFSTEP]
refine' Equiv.trans _ nim_add_nim_equiv
[GOAL]
G H : PGame
inst✝¹ : Impartial G
inst✝ : Impartial H
n m : ℕ
hG : grundyValue G = ↑n
hH : grundyValue H = ↑m
⊢ G + H ≈ nim ↑n + nim ↑m
[PROOFSTEP]
convert add_congr (equiv_nim_grundyValue G) (equiv_nim_grundyValue H)
[GOAL]
case h.e'_4.h.e'_5.h.e'_1
G H : PGame
inst✝¹ : Impartial G
inst✝ : Impartial H
n m : ℕ
hG : grundyValue G = ↑n
hH : grundyValue H = ↑m
⊢ ↑n = grundyValue G
[PROOFSTEP]
simp only [hG, hH]
[GOAL]
case h.e'_4.h.e'_6.h.e'_1
G H : PGame
inst✝¹ : Impartial G
inst✝ : Impartial H
n m : ℕ
hG : grundyValue G = ↑n
hH : grundyValue H = ↑m
⊢ ↑m = grundyValue H
[PROOFSTEP]
simp only [hG, hH]
