[GOAL]
S : Type u
inst✝ : State S
s t : S
m : t ∈ l s
⊢ turnBound s ≠ 0
[PROOFSTEP]
intro h
[GOAL]
S : Type u
inst✝ : State S
s t : S
m : t ∈ l s
h : turnBound s = 0
⊢ False
[PROOFSTEP]
have t := left_bound m
[GOAL]
S : Type u
inst✝ : State S
s t✝ : S
m : t✝ ∈ l s
h : turnBound s = 0
t : turnBound t✝ < turnBound s
⊢ False
[PROOFSTEP]
rw [h] at t
[GOAL]
S : Type u
inst✝ : State S
s t✝ : S
m : t✝ ∈ l s
h : turnBound s = 0
t : turnBound t✝ < 0
⊢ False
[PROOFSTEP]
exact Nat.not_succ_le_zero _ t
[GOAL]
S : Type u
inst✝ : State S
s t : S
m : t ∈ r s
⊢ turnBound s ≠ 0
[PROOFSTEP]
intro h
[GOAL]
S : Type u
inst✝ : State S
s t : S
m : t ∈ r s
h : turnBound s = 0
⊢ False
[PROOFSTEP]
have t := right_bound m
[GOAL]
S : Type u
inst✝ : State S
s t✝ : S
m : t✝ ∈ r s
h : turnBound s = 0
t : turnBound t✝ < turnBound s
⊢ False
[PROOFSTEP]
rw [h] at t
[GOAL]
S : Type u
inst✝ : State S
s t✝ : S
m : t✝ ∈ r s
h : turnBound s = 0
t : turnBound t✝ < 0
⊢ False
[PROOFSTEP]
exact Nat.not_succ_le_zero _ t
[GOAL]
S : Type u
inst✝ : State S
s : S
h : turnBound s ≤ 0
t : { t // t ∈ l s }
⊢ PGame
[PROOFSTEP]
exfalso
[GOAL]
case h
S : Type u
inst✝ : State S
s : S
h : turnBound s ≤ 0
t : { t // t ∈ l s }
⊢ False
[PROOFSTEP]
exact turnBound_ne_zero_of_left_move t.2 (nonpos_iff_eq_zero.mp h)
[GOAL]
S : Type u
inst✝ : State S
s : S
h : turnBound s ≤ 0
t : { t // t ∈ r s }
⊢ PGame
[PROOFSTEP]
exfalso
[GOAL]
case h
S : Type u
inst✝ : State S
s : S
h : turnBound s ≤ 0
t : { t // t ∈ r s }
⊢ False
[PROOFSTEP]
exact turnBound_ne_zero_of_right_move t.2 (nonpos_iff_eq_zero.mp h)
[GOAL]
S : Type u
inst✝ : State S
s : S
hn hm : turnBound s ≤ 0
⊢ ofStateAux 0 s hn ≡r ofStateAux 0 s hm
[PROOFSTEP]
dsimp [PGame.ofStateAux]
[GOAL]
S : Type u
inst✝ : State S
s : S
hn hm : turnBound s ≤ 0
⊢ (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False)) ≡r
    mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False)
[PROOFSTEP]
fconstructor
[GOAL]
case L
S : Type u
inst✝ : State S
s : S
hn hm : turnBound s ≤ 0
⊢ LeftMoves (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False)) ≃
    LeftMoves (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False))
case R
S : Type u
inst✝ : State S
s : S
hn hm : turnBound s ≤ 0
⊢ RightMoves (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False)) ≃
    RightMoves (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False))
case a
S : Type u
inst✝ : State S
s : S
hn hm : turnBound s ≤ 0
⊢ (i :
      LeftMoves
        (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False))) →
    moveLeft (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False))
        i ≡r
      moveLeft (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False))
        (↑?L i)
case a
S : Type u
inst✝ : State S
s : S
hn hm : turnBound s ≤ 0
⊢ (j :
      RightMoves
        (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False))) →
    moveRight (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False))
        j ≡r
      moveRight (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False))
        (↑?R j)
[PROOFSTEP]
rfl
[GOAL]
case R
S : Type u
inst✝ : State S
s : S
hn hm : turnBound s ≤ 0
⊢ RightMoves (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False)) ≃
    RightMoves (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False))
case a
S : Type u
inst✝ : State S
s : S
hn hm : turnBound s ≤ 0
⊢ (i :
      LeftMoves
        (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False))) →
    moveLeft (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False))
        i ≡r
      moveLeft (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False))
        (↑(Equiv.refl
              (LeftMoves
                (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t =>
                  False.elim (_ : False))))
          i)
case a
S : Type u
inst✝ : State S
s : S
hn hm : turnBound s ≤ 0
⊢ (j :
      RightMoves
        (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False))) →
    moveRight (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False))
        j ≡r
      moveRight (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False))
        (↑?R j)
[PROOFSTEP]
rfl
[GOAL]
case a
S : Type u
inst✝ : State S
s : S
hn hm : turnBound s ≤ 0
⊢ (i :
      LeftMoves
        (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False))) →
    moveLeft (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False))
        i ≡r
      moveLeft (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False))
        (↑(Equiv.refl
              (LeftMoves
                (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t =>
                  False.elim (_ : False))))
          i)
[PROOFSTEP]
intro i
[GOAL]
case a
S : Type u
inst✝ : State S
s : S
hn hm : turnBound s ≤ 0
i : LeftMoves (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False))
⊢ moveLeft (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False)) i ≡r
    moveLeft (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False))
      (↑(Equiv.refl
            (LeftMoves
              (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False))))
        i)
[PROOFSTEP]
dsimp at i
[GOAL]
case a
S : Type u
inst✝ : State S
s : S
hn hm : turnBound s ≤ 0
i : { t // t ∈ l s }
⊢ moveLeft (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False)) i ≡r
    moveLeft (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False))
      (↑(Equiv.refl
            (LeftMoves
              (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False))))
        i)
[PROOFSTEP]
exfalso
[GOAL]
case a.h
S : Type u
inst✝ : State S
s : S
hn hm : turnBound s ≤ 0
i : { t // t ∈ l s }
⊢ False
[PROOFSTEP]
exact turnBound_ne_zero_of_left_move i.2 (nonpos_iff_eq_zero.mp hn)
[GOAL]
case a
S : Type u
inst✝ : State S
s : S
hn hm : turnBound s ≤ 0
⊢ (j :
      RightMoves
        (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False))) →
    moveRight (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False))
        j ≡r
      moveRight (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False))
        (↑(Equiv.refl
              (RightMoves
                (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t =>
                  False.elim (_ : False))))
          j)
[PROOFSTEP]
intro j
[GOAL]
case a
S : Type u
inst✝ : State S
s : S
hn hm : turnBound s ≤ 0
j : RightMoves (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False))
⊢ moveRight (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False))
      j ≡r
    moveRight (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False))
      (↑(Equiv.refl
            (RightMoves
              (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False))))
        j)
[PROOFSTEP]
dsimp at j
[GOAL]
case a
S : Type u
inst✝ : State S
s : S
hn hm : turnBound s ≤ 0
j : { t // t ∈ r s }
⊢ moveRight (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False))
      j ≡r
    moveRight (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False))
      (↑(Equiv.refl
            (RightMoves
              (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False))))
        j)
[PROOFSTEP]
exfalso
[GOAL]
case a.h
S : Type u
inst✝ : State S
s : S
hn hm : turnBound s ≤ 0
j : { t // t ∈ r s }
⊢ False
[PROOFSTEP]
exact turnBound_ne_zero_of_right_move j.2 (nonpos_iff_eq_zero.mp hm)
[GOAL]
S : Type u
inst✝ : State S
s : S
m : ℕ
hn : turnBound s ≤ 0
hm : turnBound s ≤ m + 1
⊢ ofStateAux 0 s hn ≡r ofStateAux (m + 1) s hm
[PROOFSTEP]
dsimp [PGame.ofStateAux]
[GOAL]
S : Type u
inst✝ : State S
s : S
m : ℕ
hn : turnBound s ≤ 0
hm : turnBound s ≤ m + 1
⊢ (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False)) ≡r
    mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux m ↑t (_ : turnBound ↑t ≤ m)) fun t =>
      ofStateAux m ↑t (_ : turnBound ↑t ≤ m)
[PROOFSTEP]
fconstructor
[GOAL]
case L
S : Type u
inst✝ : State S
s : S
m : ℕ
hn : turnBound s ≤ 0
hm : turnBound s ≤ m + 1
⊢ LeftMoves (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False)) ≃
    LeftMoves
      (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux m ↑t (_ : turnBound ↑t ≤ m)) fun t =>
        ofStateAux m ↑t (_ : turnBound ↑t ≤ m))
case R
S : Type u
inst✝ : State S
s : S
m : ℕ
hn : turnBound s ≤ 0
hm : turnBound s ≤ m + 1
⊢ RightMoves (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False)) ≃
    RightMoves
      (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux m ↑t (_ : turnBound ↑t ≤ m)) fun t =>
        ofStateAux m ↑t (_ : turnBound ↑t ≤ m))
case a
S : Type u
inst✝ : State S
s : S
m : ℕ
hn : turnBound s ≤ 0
hm : turnBound s ≤ m + 1
⊢ (i :
      LeftMoves
        (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False))) →
    moveLeft (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False))
        i ≡r
      moveLeft
        (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux m ↑t (_ : turnBound ↑t ≤ m)) fun t =>
          ofStateAux m ↑t (_ : turnBound ↑t ≤ m))
        (↑?L i)
case a
S : Type u
inst✝ : State S
s : S
m : ℕ
hn : turnBound s ≤ 0
hm : turnBound s ≤ m + 1
⊢ (j :
      RightMoves
        (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False))) →
    moveRight (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False))
        j ≡r
      moveRight
        (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux m ↑t (_ : turnBound ↑t ≤ m)) fun t =>
          ofStateAux m ↑t (_ : turnBound ↑t ≤ m))
        (↑?R j)
[PROOFSTEP]
rfl
[GOAL]
case R
S : Type u
inst✝ : State S
s : S
m : ℕ
hn : turnBound s ≤ 0
hm : turnBound s ≤ m + 1
⊢ RightMoves (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False)) ≃
    RightMoves
      (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux m ↑t (_ : turnBound ↑t ≤ m)) fun t =>
        ofStateAux m ↑t (_ : turnBound ↑t ≤ m))
case a
S : Type u
inst✝ : State S
s : S
m : ℕ
hn : turnBound s ≤ 0
hm : turnBound s ≤ m + 1
⊢ (i :
      LeftMoves
        (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False))) →
    moveLeft (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False))
        i ≡r
      moveLeft
        (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux m ↑t (_ : turnBound ↑t ≤ m)) fun t =>
          ofStateAux m ↑t (_ : turnBound ↑t ≤ m))
        (↑(Equiv.refl
              (LeftMoves
                (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t =>
                  False.elim (_ : False))))
          i)
case a
S : Type u
inst✝ : State S
s : S
m : ℕ
hn : turnBound s ≤ 0
hm : turnBound s ≤ m + 1
⊢ (j :
      RightMoves
        (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False))) →
    moveRight (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False))
        j ≡r
      moveRight
        (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux m ↑t (_ : turnBound ↑t ≤ m)) fun t =>
          ofStateAux m ↑t (_ : turnBound ↑t ≤ m))
        (↑?R j)
[PROOFSTEP]
rfl
[GOAL]
case a
S : Type u
inst✝ : State S
s : S
m : ℕ
hn : turnBound s ≤ 0
hm : turnBound s ≤ m + 1
⊢ (i :
      LeftMoves
        (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False))) →
    moveLeft (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False))
        i ≡r
      moveLeft
        (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux m ↑t (_ : turnBound ↑t ≤ m)) fun t =>
          ofStateAux m ↑t (_ : turnBound ↑t ≤ m))
        (↑(Equiv.refl
              (LeftMoves
                (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t =>
                  False.elim (_ : False))))
          i)
[PROOFSTEP]
intro i
[GOAL]
case a
S : Type u
inst✝ : State S
s : S
m : ℕ
hn : turnBound s ≤ 0
hm : turnBound s ≤ m + 1
i : LeftMoves (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False))
⊢ moveLeft (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False)) i ≡r
    moveLeft
      (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux m ↑t (_ : turnBound ↑t ≤ m)) fun t =>
        ofStateAux m ↑t (_ : turnBound ↑t ≤ m))
      (↑(Equiv.refl
            (LeftMoves
              (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False))))
        i)
[PROOFSTEP]
dsimp at i
[GOAL]
case a
S : Type u
inst✝ : State S
s : S
m : ℕ
hn : turnBound s ≤ 0
hm : turnBound s ≤ m + 1
i : { t // t ∈ l s }
⊢ moveLeft (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False)) i ≡r
    moveLeft
      (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux m ↑t (_ : turnBound ↑t ≤ m)) fun t =>
        ofStateAux m ↑t (_ : turnBound ↑t ≤ m))
      (↑(Equiv.refl
            (LeftMoves
              (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False))))
        i)
[PROOFSTEP]
exfalso
[GOAL]
case a.h
S : Type u
inst✝ : State S
s : S
m : ℕ
hn : turnBound s ≤ 0
hm : turnBound s ≤ m + 1
i : { t // t ∈ l s }
⊢ False
[PROOFSTEP]
exact turnBound_ne_zero_of_left_move i.2 (nonpos_iff_eq_zero.mp hn)
[GOAL]
case a
S : Type u
inst✝ : State S
s : S
m : ℕ
hn : turnBound s ≤ 0
hm : turnBound s ≤ m + 1
⊢ (j :
      RightMoves
        (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False))) →
    moveRight (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False))
        j ≡r
      moveRight
        (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux m ↑t (_ : turnBound ↑t ≤ m)) fun t =>
          ofStateAux m ↑t (_ : turnBound ↑t ≤ m))
        (↑(Equiv.refl
              (RightMoves
                (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t =>
                  False.elim (_ : False))))
          j)
[PROOFSTEP]
intro j
[GOAL]
case a
S : Type u
inst✝ : State S
s : S
m : ℕ
hn : turnBound s ≤ 0
hm : turnBound s ≤ m + 1
j : RightMoves (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False))
⊢ moveRight (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False))
      j ≡r
    moveRight
      (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux m ↑t (_ : turnBound ↑t ≤ m)) fun t =>
        ofStateAux m ↑t (_ : turnBound ↑t ≤ m))
      (↑(Equiv.refl
            (RightMoves
              (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False))))
        j)
[PROOFSTEP]
dsimp at j
[GOAL]
case a
S : Type u
inst✝ : State S
s : S
m : ℕ
hn : turnBound s ≤ 0
hm : turnBound s ≤ m + 1
j : { t // t ∈ r s }
⊢ moveRight (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False))
      j ≡r
    moveRight
      (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux m ↑t (_ : turnBound ↑t ≤ m)) fun t =>
        ofStateAux m ↑t (_ : turnBound ↑t ≤ m))
      (↑(Equiv.refl
            (RightMoves
              (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False))))
        j)
[PROOFSTEP]
exfalso
[GOAL]
case a.h
S : Type u
inst✝ : State S
s : S
m : ℕ
hn : turnBound s ≤ 0
hm : turnBound s ≤ m + 1
j : { t // t ∈ r s }
⊢ False
[PROOFSTEP]
exact turnBound_ne_zero_of_right_move j.2 (nonpos_iff_eq_zero.mp hn)
[GOAL]
S : Type u
inst✝ : State S
s : S
n : ℕ
hn : turnBound s ≤ n + 1
hm : turnBound s ≤ 0
⊢ ofStateAux (n + 1) s hn ≡r ofStateAux 0 s hm
[PROOFSTEP]
dsimp [PGame.ofStateAux]
[GOAL]
S : Type u
inst✝ : State S
s : S
n : ℕ
hn : turnBound s ≤ n + 1
hm : turnBound s ≤ 0
⊢ (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux n ↑t (_ : turnBound ↑t ≤ n)) fun t =>
      ofStateAux n ↑t (_ : turnBound ↑t ≤ n)) ≡r
    mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False)
[PROOFSTEP]
fconstructor
[GOAL]
case L
S : Type u
inst✝ : State S
s : S
n : ℕ
hn : turnBound s ≤ n + 1
hm : turnBound s ≤ 0
⊢ LeftMoves
      (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux n ↑t (_ : turnBound ↑t ≤ n)) fun t =>
        ofStateAux n ↑t (_ : turnBound ↑t ≤ n)) ≃
    LeftMoves (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False))
case R
S : Type u
inst✝ : State S
s : S
n : ℕ
hn : turnBound s ≤ n + 1
hm : turnBound s ≤ 0
⊢ RightMoves
      (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux n ↑t (_ : turnBound ↑t ≤ n)) fun t =>
        ofStateAux n ↑t (_ : turnBound ↑t ≤ n)) ≃
    RightMoves (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False))
case a
S : Type u
inst✝ : State S
s : S
n : ℕ
hn : turnBound s ≤ n + 1
hm : turnBound s ≤ 0
⊢ (i :
      LeftMoves
        (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux n ↑t (_ : turnBound ↑t ≤ n)) fun t =>
          ofStateAux n ↑t (_ : turnBound ↑t ≤ n))) →
    moveLeft
        (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux n ↑t (_ : turnBound ↑t ≤ n)) fun t =>
          ofStateAux n ↑t (_ : turnBound ↑t ≤ n))
        i ≡r
      moveLeft (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False))
        (↑?L i)
case a
S : Type u
inst✝ : State S
s : S
n : ℕ
hn : turnBound s ≤ n + 1
hm : turnBound s ≤ 0
⊢ (j :
      RightMoves
        (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux n ↑t (_ : turnBound ↑t ≤ n)) fun t =>
          ofStateAux n ↑t (_ : turnBound ↑t ≤ n))) →
    moveRight
        (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux n ↑t (_ : turnBound ↑t ≤ n)) fun t =>
          ofStateAux n ↑t (_ : turnBound ↑t ≤ n))
        j ≡r
      moveRight (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False))
        (↑?R j)
[PROOFSTEP]
rfl
[GOAL]
case R
S : Type u
inst✝ : State S
s : S
n : ℕ
hn : turnBound s ≤ n + 1
hm : turnBound s ≤ 0
⊢ RightMoves
      (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux n ↑t (_ : turnBound ↑t ≤ n)) fun t =>
        ofStateAux n ↑t (_ : turnBound ↑t ≤ n)) ≃
    RightMoves (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False))
case a
S : Type u
inst✝ : State S
s : S
n : ℕ
hn : turnBound s ≤ n + 1
hm : turnBound s ≤ 0
⊢ (i :
      LeftMoves
        (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux n ↑t (_ : turnBound ↑t ≤ n)) fun t =>
          ofStateAux n ↑t (_ : turnBound ↑t ≤ n))) →
    moveLeft
        (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux n ↑t (_ : turnBound ↑t ≤ n)) fun t =>
          ofStateAux n ↑t (_ : turnBound ↑t ≤ n))
        i ≡r
      moveLeft (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False))
        (↑(Equiv.refl
              (LeftMoves
                (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux n ↑t (_ : turnBound ↑t ≤ n)) fun t =>
                  ofStateAux n ↑t (_ : turnBound ↑t ≤ n))))
          i)
case a
S : Type u
inst✝ : State S
s : S
n : ℕ
hn : turnBound s ≤ n + 1
hm : turnBound s ≤ 0
⊢ (j :
      RightMoves
        (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux n ↑t (_ : turnBound ↑t ≤ n)) fun t =>
          ofStateAux n ↑t (_ : turnBound ↑t ≤ n))) →
    moveRight
        (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux n ↑t (_ : turnBound ↑t ≤ n)) fun t =>
          ofStateAux n ↑t (_ : turnBound ↑t ≤ n))
        j ≡r
      moveRight (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False))
        (↑?R j)
[PROOFSTEP]
rfl
[GOAL]
case a
S : Type u
inst✝ : State S
s : S
n : ℕ
hn : turnBound s ≤ n + 1
hm : turnBound s ≤ 0
⊢ (i :
      LeftMoves
        (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux n ↑t (_ : turnBound ↑t ≤ n)) fun t =>
          ofStateAux n ↑t (_ : turnBound ↑t ≤ n))) →
    moveLeft
        (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux n ↑t (_ : turnBound ↑t ≤ n)) fun t =>
          ofStateAux n ↑t (_ : turnBound ↑t ≤ n))
        i ≡r
      moveLeft (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False))
        (↑(Equiv.refl
              (LeftMoves
                (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux n ↑t (_ : turnBound ↑t ≤ n)) fun t =>
                  ofStateAux n ↑t (_ : turnBound ↑t ≤ n))))
          i)
[PROOFSTEP]
intro i
[GOAL]
case a
S : Type u
inst✝ : State S
s : S
n : ℕ
hn : turnBound s ≤ n + 1
hm : turnBound s ≤ 0
i :
  LeftMoves
    (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux n ↑t (_ : turnBound ↑t ≤ n)) fun t =>
      ofStateAux n ↑t (_ : turnBound ↑t ≤ n))
⊢ moveLeft
      (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux n ↑t (_ : turnBound ↑t ≤ n)) fun t =>
        ofStateAux n ↑t (_ : turnBound ↑t ≤ n))
      i ≡r
    moveLeft (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False))
      (↑(Equiv.refl
            (LeftMoves
              (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux n ↑t (_ : turnBound ↑t ≤ n)) fun t =>
                ofStateAux n ↑t (_ : turnBound ↑t ≤ n))))
        i)
[PROOFSTEP]
dsimp at i
[GOAL]
case a
S : Type u
inst✝ : State S
s : S
n : ℕ
hn : turnBound s ≤ n + 1
hm : turnBound s ≤ 0
i : { t // t ∈ l s }
⊢ moveLeft
      (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux n ↑t (_ : turnBound ↑t ≤ n)) fun t =>
        ofStateAux n ↑t (_ : turnBound ↑t ≤ n))
      i ≡r
    moveLeft (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False))
      (↑(Equiv.refl
            (LeftMoves
              (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux n ↑t (_ : turnBound ↑t ≤ n)) fun t =>
                ofStateAux n ↑t (_ : turnBound ↑t ≤ n))))
        i)
[PROOFSTEP]
exfalso
[GOAL]
case a.h
S : Type u
inst✝ : State S
s : S
n : ℕ
hn : turnBound s ≤ n + 1
hm : turnBound s ≤ 0
i : { t // t ∈ l s }
⊢ False
[PROOFSTEP]
exact turnBound_ne_zero_of_left_move i.2 (nonpos_iff_eq_zero.mp hm)
[GOAL]
case a
S : Type u
inst✝ : State S
s : S
n : ℕ
hn : turnBound s ≤ n + 1
hm : turnBound s ≤ 0
⊢ (j :
      RightMoves
        (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux n ↑t (_ : turnBound ↑t ≤ n)) fun t =>
          ofStateAux n ↑t (_ : turnBound ↑t ≤ n))) →
    moveRight
        (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux n ↑t (_ : turnBound ↑t ≤ n)) fun t =>
          ofStateAux n ↑t (_ : turnBound ↑t ≤ n))
        j ≡r
      moveRight (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False))
        (↑(Equiv.refl
              (RightMoves
                (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux n ↑t (_ : turnBound ↑t ≤ n)) fun t =>
                  ofStateAux n ↑t (_ : turnBound ↑t ≤ n))))
          j)
[PROOFSTEP]
intro j
[GOAL]
case a
S : Type u
inst✝ : State S
s : S
n : ℕ
hn : turnBound s ≤ n + 1
hm : turnBound s ≤ 0
j :
  RightMoves
    (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux n ↑t (_ : turnBound ↑t ≤ n)) fun t =>
      ofStateAux n ↑t (_ : turnBound ↑t ≤ n))
⊢ moveRight
      (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux n ↑t (_ : turnBound ↑t ≤ n)) fun t =>
        ofStateAux n ↑t (_ : turnBound ↑t ≤ n))
      j ≡r
    moveRight (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False))
      (↑(Equiv.refl
            (RightMoves
              (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux n ↑t (_ : turnBound ↑t ≤ n)) fun t =>
                ofStateAux n ↑t (_ : turnBound ↑t ≤ n))))
        j)
[PROOFSTEP]
dsimp at j
[GOAL]
case a
S : Type u
inst✝ : State S
s : S
n : ℕ
hn : turnBound s ≤ n + 1
hm : turnBound s ≤ 0
j : { t // t ∈ r s }
⊢ moveRight
      (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux n ↑t (_ : turnBound ↑t ≤ n)) fun t =>
        ofStateAux n ↑t (_ : turnBound ↑t ≤ n))
      j ≡r
    moveRight (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => False.elim (_ : False)) fun t => False.elim (_ : False))
      (↑(Equiv.refl
            (RightMoves
              (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux n ↑t (_ : turnBound ↑t ≤ n)) fun t =>
                ofStateAux n ↑t (_ : turnBound ↑t ≤ n))))
        j)
[PROOFSTEP]
exfalso
[GOAL]
case a.h
S : Type u
inst✝ : State S
s : S
n : ℕ
hn : turnBound s ≤ n + 1
hm : turnBound s ≤ 0
j : { t // t ∈ r s }
⊢ False
[PROOFSTEP]
exact turnBound_ne_zero_of_right_move j.2 (nonpos_iff_eq_zero.mp hm)
[GOAL]
S : Type u
inst✝ : State S
s : S
n m : ℕ
hn : turnBound s ≤ n + 1
hm : turnBound s ≤ m + 1
⊢ ofStateAux (n + 1) s hn ≡r ofStateAux (m + 1) s hm
[PROOFSTEP]
dsimp [PGame.ofStateAux]
[GOAL]
S : Type u
inst✝ : State S
s : S
n m : ℕ
hn : turnBound s ≤ n + 1
hm : turnBound s ≤ m + 1
⊢ (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux n ↑t (_ : turnBound ↑t ≤ n)) fun t =>
      ofStateAux n ↑t (_ : turnBound ↑t ≤ n)) ≡r
    mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux m ↑t (_ : turnBound ↑t ≤ m)) fun t =>
      ofStateAux m ↑t (_ : turnBound ↑t ≤ m)
[PROOFSTEP]
fconstructor
[GOAL]
case L
S : Type u
inst✝ : State S
s : S
n m : ℕ
hn : turnBound s ≤ n + 1
hm : turnBound s ≤ m + 1
⊢ LeftMoves
      (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux n ↑t (_ : turnBound ↑t ≤ n)) fun t =>
        ofStateAux n ↑t (_ : turnBound ↑t ≤ n)) ≃
    LeftMoves
      (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux m ↑t (_ : turnBound ↑t ≤ m)) fun t =>
        ofStateAux m ↑t (_ : turnBound ↑t ≤ m))
case R
S : Type u
inst✝ : State S
s : S
n m : ℕ
hn : turnBound s ≤ n + 1
hm : turnBound s ≤ m + 1
⊢ RightMoves
      (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux n ↑t (_ : turnBound ↑t ≤ n)) fun t =>
        ofStateAux n ↑t (_ : turnBound ↑t ≤ n)) ≃
    RightMoves
      (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux m ↑t (_ : turnBound ↑t ≤ m)) fun t =>
        ofStateAux m ↑t (_ : turnBound ↑t ≤ m))
case a
S : Type u
inst✝ : State S
s : S
n m : ℕ
hn : turnBound s ≤ n + 1
hm : turnBound s ≤ m + 1
⊢ (i :
      LeftMoves
        (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux n ↑t (_ : turnBound ↑t ≤ n)) fun t =>
          ofStateAux n ↑t (_ : turnBound ↑t ≤ n))) →
    moveLeft
        (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux n ↑t (_ : turnBound ↑t ≤ n)) fun t =>
          ofStateAux n ↑t (_ : turnBound ↑t ≤ n))
        i ≡r
      moveLeft
        (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux m ↑t (_ : turnBound ↑t ≤ m)) fun t =>
          ofStateAux m ↑t (_ : turnBound ↑t ≤ m))
        (↑?L i)
case a
S : Type u
inst✝ : State S
s : S
n m : ℕ
hn : turnBound s ≤ n + 1
hm : turnBound s ≤ m + 1
⊢ (j :
      RightMoves
        (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux n ↑t (_ : turnBound ↑t ≤ n)) fun t =>
          ofStateAux n ↑t (_ : turnBound ↑t ≤ n))) →
    moveRight
        (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux n ↑t (_ : turnBound ↑t ≤ n)) fun t =>
          ofStateAux n ↑t (_ : turnBound ↑t ≤ n))
        j ≡r
      moveRight
        (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux m ↑t (_ : turnBound ↑t ≤ m)) fun t =>
          ofStateAux m ↑t (_ : turnBound ↑t ≤ m))
        (↑?R j)
[PROOFSTEP]
rfl
[GOAL]
case R
S : Type u
inst✝ : State S
s : S
n m : ℕ
hn : turnBound s ≤ n + 1
hm : turnBound s ≤ m + 1
⊢ RightMoves
      (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux n ↑t (_ : turnBound ↑t ≤ n)) fun t =>
        ofStateAux n ↑t (_ : turnBound ↑t ≤ n)) ≃
    RightMoves
      (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux m ↑t (_ : turnBound ↑t ≤ m)) fun t =>
        ofStateAux m ↑t (_ : turnBound ↑t ≤ m))
case a
S : Type u
inst✝ : State S
s : S
n m : ℕ
hn : turnBound s ≤ n + 1
hm : turnBound s ≤ m + 1
⊢ (i :
      LeftMoves
        (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux n ↑t (_ : turnBound ↑t ≤ n)) fun t =>
          ofStateAux n ↑t (_ : turnBound ↑t ≤ n))) →
    moveLeft
        (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux n ↑t (_ : turnBound ↑t ≤ n)) fun t =>
          ofStateAux n ↑t (_ : turnBound ↑t ≤ n))
        i ≡r
      moveLeft
        (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux m ↑t (_ : turnBound ↑t ≤ m)) fun t =>
          ofStateAux m ↑t (_ : turnBound ↑t ≤ m))
        (↑(Equiv.refl
              (LeftMoves
                (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux n ↑t (_ : turnBound ↑t ≤ n)) fun t =>
                  ofStateAux n ↑t (_ : turnBound ↑t ≤ n))))
          i)
case a
S : Type u
inst✝ : State S
s : S
n m : ℕ
hn : turnBound s ≤ n + 1
hm : turnBound s ≤ m + 1
⊢ (j :
      RightMoves
        (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux n ↑t (_ : turnBound ↑t ≤ n)) fun t =>
          ofStateAux n ↑t (_ : turnBound ↑t ≤ n))) →
    moveRight
        (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux n ↑t (_ : turnBound ↑t ≤ n)) fun t =>
          ofStateAux n ↑t (_ : turnBound ↑t ≤ n))
        j ≡r
      moveRight
        (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux m ↑t (_ : turnBound ↑t ≤ m)) fun t =>
          ofStateAux m ↑t (_ : turnBound ↑t ≤ m))
        (↑?R j)
[PROOFSTEP]
rfl
[GOAL]
case a
S : Type u
inst✝ : State S
s : S
n m : ℕ
hn : turnBound s ≤ n + 1
hm : turnBound s ≤ m + 1
⊢ (i :
      LeftMoves
        (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux n ↑t (_ : turnBound ↑t ≤ n)) fun t =>
          ofStateAux n ↑t (_ : turnBound ↑t ≤ n))) →
    moveLeft
        (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux n ↑t (_ : turnBound ↑t ≤ n)) fun t =>
          ofStateAux n ↑t (_ : turnBound ↑t ≤ n))
        i ≡r
      moveLeft
        (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux m ↑t (_ : turnBound ↑t ≤ m)) fun t =>
          ofStateAux m ↑t (_ : turnBound ↑t ≤ m))
        (↑(Equiv.refl
              (LeftMoves
                (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux n ↑t (_ : turnBound ↑t ≤ n)) fun t =>
                  ofStateAux n ↑t (_ : turnBound ↑t ≤ n))))
          i)
[PROOFSTEP]
intro i
[GOAL]
case a
S : Type u
inst✝ : State S
s : S
n m : ℕ
hn : turnBound s ≤ n + 1
hm : turnBound s ≤ m + 1
i :
  LeftMoves
    (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux n ↑t (_ : turnBound ↑t ≤ n)) fun t =>
      ofStateAux n ↑t (_ : turnBound ↑t ≤ n))
⊢ moveLeft
      (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux n ↑t (_ : turnBound ↑t ≤ n)) fun t =>
        ofStateAux n ↑t (_ : turnBound ↑t ≤ n))
      i ≡r
    moveLeft
      (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux m ↑t (_ : turnBound ↑t ≤ m)) fun t =>
        ofStateAux m ↑t (_ : turnBound ↑t ≤ m))
      (↑(Equiv.refl
            (LeftMoves
              (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux n ↑t (_ : turnBound ↑t ≤ n)) fun t =>
                ofStateAux n ↑t (_ : turnBound ↑t ≤ n))))
        i)
[PROOFSTEP]
apply ofStateAuxRelabelling
[GOAL]
case a
S : Type u
inst✝ : State S
s : S
n m : ℕ
hn : turnBound s ≤ n + 1
hm : turnBound s ≤ m + 1
⊢ (j :
      RightMoves
        (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux n ↑t (_ : turnBound ↑t ≤ n)) fun t =>
          ofStateAux n ↑t (_ : turnBound ↑t ≤ n))) →
    moveRight
        (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux n ↑t (_ : turnBound ↑t ≤ n)) fun t =>
          ofStateAux n ↑t (_ : turnBound ↑t ≤ n))
        j ≡r
      moveRight
        (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux m ↑t (_ : turnBound ↑t ≤ m)) fun t =>
          ofStateAux m ↑t (_ : turnBound ↑t ≤ m))
        (↑(Equiv.refl
              (RightMoves
                (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux n ↑t (_ : turnBound ↑t ≤ n)) fun t =>
                  ofStateAux n ↑t (_ : turnBound ↑t ≤ n))))
          j)
[PROOFSTEP]
intro j
[GOAL]
case a
S : Type u
inst✝ : State S
s : S
n m : ℕ
hn : turnBound s ≤ n + 1
hm : turnBound s ≤ m + 1
j :
  RightMoves
    (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux n ↑t (_ : turnBound ↑t ≤ n)) fun t =>
      ofStateAux n ↑t (_ : turnBound ↑t ≤ n))
⊢ moveRight
      (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux n ↑t (_ : turnBound ↑t ≤ n)) fun t =>
        ofStateAux n ↑t (_ : turnBound ↑t ≤ n))
      j ≡r
    moveRight
      (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux m ↑t (_ : turnBound ↑t ≤ m)) fun t =>
        ofStateAux m ↑t (_ : turnBound ↑t ≤ m))
      (↑(Equiv.refl
            (RightMoves
              (mk { t // t ∈ l s } { t // t ∈ r s } (fun t => ofStateAux n ↑t (_ : turnBound ↑t ≤ n)) fun t =>
                ofStateAux n ↑t (_ : turnBound ↑t ≤ n))))
        j)
[PROOFSTEP]
apply ofStateAuxRelabelling
[GOAL]
S : Type u
inst✝ : State S
n : ℕ
s : S
h : turnBound s ≤ n
⊢ LeftMoves (ofStateAux n s h) ≃ { t // t ∈ l s }
[PROOFSTEP]
induction n
[GOAL]
case zero
S : Type u
inst✝ : State S
s : S
h : turnBound s ≤ Nat.zero
⊢ LeftMoves (ofStateAux Nat.zero s h) ≃ { t // t ∈ l s }
[PROOFSTEP]
rfl
[GOAL]
case succ
S : Type u
inst✝ : State S
s : S
n✝ : ℕ
n_ih✝ : (h : turnBound s ≤ n✝) → LeftMoves (ofStateAux n✝ s h) ≃ { t // t ∈ l s }
h : turnBound s ≤ Nat.succ n✝
⊢ LeftMoves (ofStateAux (Nat.succ n✝) s h) ≃ { t // t ∈ l s }
[PROOFSTEP]
rfl
[GOAL]
S : Type u
inst✝ : State S
n : ℕ
s : S
h : turnBound s ≤ n
⊢ RightMoves (ofStateAux n s h) ≃ { t // t ∈ r s }
[PROOFSTEP]
induction n
[GOAL]
case zero
S : Type u
inst✝ : State S
s : S
h : turnBound s ≤ Nat.zero
⊢ RightMoves (ofStateAux Nat.zero s h) ≃ { t // t ∈ r s }
[PROOFSTEP]
rfl
[GOAL]
case succ
S : Type u
inst✝ : State S
s : S
n✝ : ℕ
n_ih✝ : (h : turnBound s ≤ n✝) → RightMoves (ofStateAux n✝ s h) ≃ { t // t ∈ r s }
h : turnBound s ≤ Nat.succ n✝
⊢ RightMoves (ofStateAux (Nat.succ n✝) s h) ≃ { t // t ∈ r s }
[PROOFSTEP]
rfl
[GOAL]
S : Type u
inst✝ : State S
n : ℕ
s : S
h : turnBound s ≤ n
t : LeftMoves (ofStateAux n s h)
⊢ moveLeft (ofStateAux n s h) t ≡r
    ofStateAux (n - 1) ↑(↑(leftMovesOfStateAux n h) t) (_ : turnBound ↑(↑(leftMovesOfStateAux n h) t) ≤ n - 1)
[PROOFSTEP]
induction n
[GOAL]
case zero
S : Type u
inst✝ : State S
s : S
h : turnBound s ≤ Nat.zero
t : LeftMoves (ofStateAux Nat.zero s h)
⊢ moveLeft (ofStateAux Nat.zero s h) t ≡r
    ofStateAux (Nat.zero - 1) ↑(↑(leftMovesOfStateAux Nat.zero h) t)
      (_ : turnBound ↑(↑(leftMovesOfStateAux Nat.zero h) t) ≤ Nat.zero - 1)
[PROOFSTEP]
have t' := (leftMovesOfStateAux 0 h) t
[GOAL]
case zero
S : Type u
inst✝ : State S
s : S
h : turnBound s ≤ Nat.zero
t : LeftMoves (ofStateAux Nat.zero s h)
t' : (fun x => { t // t ∈ l s }) t
⊢ moveLeft (ofStateAux Nat.zero s h) t ≡r
    ofStateAux (Nat.zero - 1) ↑(↑(leftMovesOfStateAux Nat.zero h) t)
      (_ : turnBound ↑(↑(leftMovesOfStateAux Nat.zero h) t) ≤ Nat.zero - 1)
[PROOFSTEP]
exfalso
[GOAL]
case zero.h
S : Type u
inst✝ : State S
s : S
h : turnBound s ≤ Nat.zero
t : LeftMoves (ofStateAux Nat.zero s h)
t' : (fun x => { t // t ∈ l s }) t
⊢ False
[PROOFSTEP]
exact turnBound_ne_zero_of_left_move t'.2 (nonpos_iff_eq_zero.mp h)
[GOAL]
case succ
S : Type u
inst✝ : State S
s : S
n✝ : ℕ
n_ih✝ :
  (h : turnBound s ≤ n✝) →
    (t : LeftMoves (ofStateAux n✝ s h)) →
      moveLeft (ofStateAux n✝ s h) t ≡r
        ofStateAux (n✝ - 1) ↑(↑(leftMovesOfStateAux n✝ h) t) (_ : turnBound ↑(↑(leftMovesOfStateAux n✝ h) t) ≤ n✝ - 1)
h : turnBound s ≤ Nat.succ n✝
t : LeftMoves (ofStateAux (Nat.succ n✝) s h)
⊢ moveLeft (ofStateAux (Nat.succ n✝) s h) t ≡r
    ofStateAux (Nat.succ n✝ - 1) ↑(↑(leftMovesOfStateAux (Nat.succ n✝) h) t)
      (_ : turnBound ↑(↑(leftMovesOfStateAux (Nat.succ n✝) h) t) ≤ Nat.succ n✝ - 1)
[PROOFSTEP]
rfl
[GOAL]
S : Type u
inst✝ : State S
s : S
t : LeftMoves (ofState s)
⊢ moveLeft (ofState s) t ≡r ofState ↑(Equiv.toFun (leftMovesOfState s) t)
[PROOFSTEP]
trans
[GOAL]
S : Type u
inst✝ : State S
s : S
t : LeftMoves (ofState s)
⊢ moveLeft (ofState s) t ≡r ?m.9328
S : Type u
inst✝ : State S
s : S
t : LeftMoves (ofState s)
⊢ ?m.9328 ≡r ofState ↑(Equiv.toFun (leftMovesOfState s) t)
S : Type u inst✝ : State S s : S t : LeftMoves (ofState s) ⊢ PGame
[PROOFSTEP]
apply relabellingMoveLeftAux
[GOAL]
S : Type u
inst✝ : State S
s : S
t : LeftMoves (ofState s)
⊢ ofStateAux (turnBound s - 1) ↑(↑(leftMovesOfStateAux (turnBound s) (_ : turnBound s ≤ turnBound s)) t)
      (_ : turnBound ↑(↑(leftMovesOfStateAux (turnBound s) (_ : turnBound s ≤ turnBound s)) t) ≤ turnBound s - 1) ≡r
    ofState ↑(Equiv.toFun (leftMovesOfState s) t)
[PROOFSTEP]
apply ofStateAuxRelabelling
[GOAL]
S : Type u
inst✝ : State S
n : ℕ
s : S
h : turnBound s ≤ n
t : RightMoves (ofStateAux n s h)
⊢ moveRight (ofStateAux n s h) t ≡r
    ofStateAux (n - 1) ↑(↑(rightMovesOfStateAux n h) t) (_ : turnBound ↑(↑(rightMovesOfStateAux n h) t) ≤ n - 1)
[PROOFSTEP]
induction n
[GOAL]
case zero
S : Type u
inst✝ : State S
s : S
h : turnBound s ≤ Nat.zero
t : RightMoves (ofStateAux Nat.zero s h)
⊢ moveRight (ofStateAux Nat.zero s h) t ≡r
    ofStateAux (Nat.zero - 1) ↑(↑(rightMovesOfStateAux Nat.zero h) t)
      (_ : turnBound ↑(↑(rightMovesOfStateAux Nat.zero h) t) ≤ Nat.zero - 1)
[PROOFSTEP]
have t' := (rightMovesOfStateAux 0 h) t
[GOAL]
case zero
S : Type u
inst✝ : State S
s : S
h : turnBound s ≤ Nat.zero
t : RightMoves (ofStateAux Nat.zero s h)
t' : (fun x => { t // t ∈ r s }) t
⊢ moveRight (ofStateAux Nat.zero s h) t ≡r
    ofStateAux (Nat.zero - 1) ↑(↑(rightMovesOfStateAux Nat.zero h) t)
      (_ : turnBound ↑(↑(rightMovesOfStateAux Nat.zero h) t) ≤ Nat.zero - 1)
[PROOFSTEP]
exfalso
[GOAL]
case zero.h
S : Type u
inst✝ : State S
s : S
h : turnBound s ≤ Nat.zero
t : RightMoves (ofStateAux Nat.zero s h)
t' : (fun x => { t // t ∈ r s }) t
⊢ False
[PROOFSTEP]
exact turnBound_ne_zero_of_right_move t'.2 (nonpos_iff_eq_zero.mp h)
[GOAL]
case succ
S : Type u
inst✝ : State S
s : S
n✝ : ℕ
n_ih✝ :
  (h : turnBound s ≤ n✝) →
    (t : RightMoves (ofStateAux n✝ s h)) →
      moveRight (ofStateAux n✝ s h) t ≡r
        ofStateAux (n✝ - 1) ↑(↑(rightMovesOfStateAux n✝ h) t) (_ : turnBound ↑(↑(rightMovesOfStateAux n✝ h) t) ≤ n✝ - 1)
h : turnBound s ≤ Nat.succ n✝
t : RightMoves (ofStateAux (Nat.succ n✝) s h)
⊢ moveRight (ofStateAux (Nat.succ n✝) s h) t ≡r
    ofStateAux (Nat.succ n✝ - 1) ↑(↑(rightMovesOfStateAux (Nat.succ n✝) h) t)
      (_ : turnBound ↑(↑(rightMovesOfStateAux (Nat.succ n✝) h) t) ≤ Nat.succ n✝ - 1)
[PROOFSTEP]
rfl
[GOAL]
S : Type u
inst✝ : State S
s : S
t : RightMoves (ofState s)
⊢ moveRight (ofState s) t ≡r ofState ↑(Equiv.toFun (rightMovesOfState s) t)
[PROOFSTEP]
trans
[GOAL]
S : Type u
inst✝ : State S
s : S
t : RightMoves (ofState s)
⊢ moveRight (ofState s) t ≡r ?m.11225
S : Type u
inst✝ : State S
s : S
t : RightMoves (ofState s)
⊢ ?m.11225 ≡r ofState ↑(Equiv.toFun (rightMovesOfState s) t)
S : Type u inst✝ : State S s : S t : RightMoves (ofState s) ⊢ PGame
[PROOFSTEP]
apply relabellingMoveRightAux
[GOAL]
S : Type u
inst✝ : State S
s : S
t : RightMoves (ofState s)
⊢ ofStateAux (turnBound s - 1) ↑(↑(rightMovesOfStateAux (turnBound s) (_ : turnBound s ≤ turnBound s)) t)
      (_ : turnBound ↑(↑(rightMovesOfStateAux (turnBound s) (_ : turnBound s ≤ turnBound s)) t) ≤ turnBound s - 1) ≡r
    ofState ↑(Equiv.toFun (rightMovesOfState s) t)
[PROOFSTEP]
apply ofStateAuxRelabelling
[GOAL]
S : Type u
inst✝ : State S
n : ℕ
s : S
h : turnBound s ≤ n
⊢ Fintype (LeftMoves (ofStateAux n s h))
[PROOFSTEP]
apply Fintype.ofEquiv _ (leftMovesOfStateAux _ _).symm
[GOAL]
S : Type u
inst✝ : State S
n : ℕ
s : S
h : turnBound s ≤ n
⊢ Fintype (RightMoves (ofStateAux n s h))
[PROOFSTEP]
apply Fintype.ofEquiv _ (rightMovesOfStateAux _ _).symm
[GOAL]
S : Type u
inst✝ : State S
s : S
h : turnBound s ≤ 0
i : LeftMoves (ofStateAux 0 s h)
⊢ Short (moveLeft (ofStateAux 0 s h) i)
[PROOFSTEP]
have i := (leftMovesOfStateAux _ _).toFun i
[GOAL]
S : Type u
inst✝ : State S
s : S
h : turnBound s ≤ 0
i✝ : LeftMoves (ofStateAux 0 s h)
i : { t // t ∈ l s }
⊢ Short (moveLeft (ofStateAux 0 s h) i✝)
[PROOFSTEP]
exfalso
[GOAL]
case h
S : Type u
inst✝ : State S
s : S
h : turnBound s ≤ 0
i✝ : LeftMoves (ofStateAux 0 s h)
i : { t // t ∈ l s }
⊢ False
[PROOFSTEP]
exact turnBound_ne_zero_of_left_move i.2 (nonpos_iff_eq_zero.mp h)
[GOAL]
S : Type u
inst✝ : State S
s : S
h : turnBound s ≤ 0
j : RightMoves (ofStateAux 0 s h)
⊢ Short (moveRight (ofStateAux 0 s h) j)
[PROOFSTEP]
have j := (rightMovesOfStateAux _ _).toFun j
[GOAL]
S : Type u
inst✝ : State S
s : S
h : turnBound s ≤ 0
j✝ : RightMoves (ofStateAux 0 s h)
j : { t // t ∈ r s }
⊢ Short (moveRight (ofStateAux 0 s h) j✝)
[PROOFSTEP]
exfalso
[GOAL]
case h
S : Type u
inst✝ : State S
s : S
h : turnBound s ≤ 0
j✝ : RightMoves (ofStateAux 0 s h)
j : { t // t ∈ r s }
⊢ False
[PROOFSTEP]
exact turnBound_ne_zero_of_right_move j.2 (nonpos_iff_eq_zero.mp h)
[GOAL]
S : Type u
inst✝ : State S
s : S
⊢ Short (ofState s)
[PROOFSTEP]
dsimp [PGame.ofState]
[GOAL]
S : Type u
inst✝ : State S
s : S
⊢ Short (ofStateAux (turnBound s) s (_ : turnBound s ≤ turnBound s))
[PROOFSTEP]
infer_instance


[GOAL]
a✝ : PGame
G : PGame := a✝
i : LeftMoves G
⊢ (invImage (fun a => a) instWellFoundedRelationPGame).1 (moveLeft G i) a✝
[PROOFSTEP]
pgame_wf_tac
[GOAL]
a✝ : PGame
G : PGame := a✝
j : RightMoves G
⊢ (invImage (fun a => a) instWellFoundedRelationPGame).1 (moveRight G j) a✝
[PROOFSTEP]
pgame_wf_tac
[GOAL]
G : PGame
⊢ ImpartialAux G ↔
    G ≈ -G ∧ (∀ (i : LeftMoves G), ImpartialAux (moveLeft G i)) ∧ ∀ (j : RightMoves G), ImpartialAux (moveRight G j)
[PROOFSTEP]
rw [ImpartialAux]
[GOAL]
G : PGame
⊢ Impartial G ↔
    G ≈ -G ∧ (∀ (i : LeftMoves G), Impartial (moveLeft G i)) ∧ ∀ (j : RightMoves G), Impartial (moveRight G j)
[PROOFSTEP]
simpa only [impartial_iff_aux] using impartialAux_def
[GOAL]
⊢ Impartial 0
[PROOFSTEP]
rw [impartial_def]
[GOAL]
⊢ 0 ≈ -0 ∧ (∀ (i : LeftMoves 0), Impartial (moveLeft 0 i)) ∧ ∀ (j : RightMoves 0), Impartial (moveRight 0 j)
[PROOFSTEP]
dsimp
[GOAL]
⊢ 0 ≈ -0 ∧ (∀ (i : PEmpty), Impartial (moveLeft 0 i)) ∧ ∀ (j : PEmpty), Impartial (moveRight 0 j)
[PROOFSTEP]
simp
[GOAL]
⊢ Impartial star
[PROOFSTEP]
rw [impartial_def]
[GOAL]
⊢ star ≈ -star ∧
    (∀ (i : LeftMoves star), Impartial (moveLeft star i)) ∧ ∀ (j : RightMoves star), Impartial (moveRight star j)
[PROOFSTEP]
simpa using Impartial.impartial_zero
[GOAL]
G H : PGame
e : G ≡r H
⊢ ∀ [inst : Impartial G], Impartial H
[PROOFSTEP]
intro h
[GOAL]
G H : PGame
e : G ≡r H
h : Impartial G
⊢ Impartial H
[PROOFSTEP]
exact
  impartial_def.2
    ⟨Equiv.trans e.symm.equiv (Equiv.trans (neg_equiv_self G) (neg_equiv_neg_iff.2 e.equiv)), fun i =>
      impartial_congr (e.moveLeftSymm i), fun j => impartial_congr (e.moveRightSymm j)⟩
[GOAL]
G H : PGame
x✝ :
  ∀ (y : (_ : PGame) ×' PGame),
    (invImage (fun a => PSigma.casesOn a fun G snd => (G, snd)) Prod.instWellFoundedRelationProd).1 y
        { fst := G, snd := H } →
      y.1 ≡r y.2 → ∀ [inst : Impartial y.1], Impartial y.2
e : G ≡r H
h : Impartial G
i : LeftMoves H
⊢ (invImage (fun a => PSigma.casesOn a fun G snd => (G, snd)) Prod.instWellFoundedRelationProd).1
    { fst := moveLeft G (↑(Relabelling.leftMovesEquiv e).symm i), snd := moveLeft H i } { fst := G, snd := H }
[PROOFSTEP]
pgame_wf_tac
[GOAL]
G H : PGame
x✝ :
  ∀ (y : (_ : PGame) ×' PGame),
    (invImage (fun a => PSigma.casesOn a fun G snd => (G, snd)) Prod.instWellFoundedRelationProd).1 y
        { fst := G, snd := H } →
      y.1 ≡r y.2 → ∀ [inst : Impartial y.1], Impartial y.2
e : G ≡r H
h : Impartial G
j : RightMoves H
⊢ (invImage (fun a => PSigma.casesOn a fun G snd => (G, snd)) Prod.instWellFoundedRelationProd).1
    { fst := moveRight G (↑(Relabelling.rightMovesEquiv e).symm j), snd := moveRight H j } { fst := G, snd := H }
[PROOFSTEP]
pgame_wf_tac
[GOAL]
G H : PGame
x✝¹ : Impartial G
x✝ : Impartial H
⊢ Impartial (G + H)
[PROOFSTEP]
rw [impartial_def]
[GOAL]
G H : PGame
x✝¹ : Impartial G
x✝ : Impartial H
⊢ G + H ≈ -(G + H) ∧
    (∀ (i : LeftMoves (G + H)), Impartial (moveLeft (G + H) i)) ∧
      ∀ (j : RightMoves (G + H)), Impartial (moveRight (G + H) j)
[PROOFSTEP]
refine'
  ⟨Equiv.trans (add_congr (neg_equiv_self G) (neg_equiv_self _)) (Equiv.symm (negAddRelabelling _ _).equiv), fun k => _,
    fun k => _⟩
[GOAL]
case refine'_1
G H : PGame
x✝¹ : Impartial G
x✝ : Impartial H
k : LeftMoves (G + H)
⊢ Impartial (moveLeft (G + H) k)
[PROOFSTEP]
apply leftMoves_add_cases k
[GOAL]
case refine'_1.hl
G H : PGame
x✝¹ : Impartial G
x✝ : Impartial H
k : LeftMoves (G + H)
⊢ ∀ (i : LeftMoves G), Impartial (moveLeft (G + H) (↑toLeftMovesAdd (Sum.inl i)))
case refine'_1.hr
G H : PGame
x✝¹ : Impartial G
x✝ : Impartial H
k : LeftMoves (G + H)
⊢ ∀ (i : LeftMoves H), Impartial (moveLeft (G + H) (↑toLeftMovesAdd (Sum.inr i)))
[PROOFSTEP]
all_goals
  intro i; simp only [add_moveLeft_inl, add_moveLeft_inr]
  apply impartial_add
[GOAL]
case refine'_1.hl
G H : PGame
x✝¹ : Impartial G
x✝ : Impartial H
k : LeftMoves (G + H)
⊢ ∀ (i : LeftMoves G), Impartial (moveLeft (G + H) (↑toLeftMovesAdd (Sum.inl i)))
[PROOFSTEP]
intro i
[GOAL]
case refine'_1.hl
G H : PGame
x✝¹ : Impartial G
x✝ : Impartial H
k : LeftMoves (G + H)
i : LeftMoves G
⊢ Impartial (moveLeft (G + H) (↑toLeftMovesAdd (Sum.inl i)))
[PROOFSTEP]
simp only [add_moveLeft_inl, add_moveLeft_inr]
[GOAL]
case refine'_1.hl
G H : PGame
x✝¹ : Impartial G
x✝ : Impartial H
k : LeftMoves (G + H)
i : LeftMoves G
⊢ Impartial (moveLeft G i + H)
[PROOFSTEP]
apply impartial_add
[GOAL]
case refine'_1.hr
G H : PGame
x✝¹ : Impartial G
x✝ : Impartial H
k : LeftMoves (G + H)
⊢ ∀ (i : LeftMoves H), Impartial (moveLeft (G + H) (↑toLeftMovesAdd (Sum.inr i)))
[PROOFSTEP]
intro i
[GOAL]
case refine'_1.hr
G H : PGame
x✝¹ : Impartial G
x✝ : Impartial H
k : LeftMoves (G + H)
i : LeftMoves H
⊢ Impartial (moveLeft (G + H) (↑toLeftMovesAdd (Sum.inr i)))
[PROOFSTEP]
simp only [add_moveLeft_inl, add_moveLeft_inr]
[GOAL]
case refine'_1.hr
G H : PGame
x✝¹ : Impartial G
x✝ : Impartial H
k : LeftMoves (G + H)
i : LeftMoves H
⊢ Impartial (G + moveLeft H i)
[PROOFSTEP]
apply impartial_add
[GOAL]
case refine'_2
G H : PGame
x✝¹ : Impartial G
x✝ : Impartial H
k : RightMoves (G + H)
⊢ Impartial (moveRight (G + H) k)
[PROOFSTEP]
apply rightMoves_add_cases k
[GOAL]
case refine'_2.hl
G H : PGame
x✝¹ : Impartial G
x✝ : Impartial H
k : RightMoves (G + H)
⊢ ∀ (j : RightMoves G), Impartial (moveRight (G + H) (↑toRightMovesAdd (Sum.inl j)))
case refine'_2.hr
G H : PGame
x✝¹ : Impartial G
x✝ : Impartial H
k : RightMoves (G + H)
⊢ ∀ (j : RightMoves H), Impartial (moveRight (G + H) (↑toRightMovesAdd (Sum.inr j)))
[PROOFSTEP]
all_goals
  intro i; simp only [add_moveRight_inl, add_moveRight_inr]
  apply impartial_add
[GOAL]
case refine'_2.hl
G H : PGame
x✝¹ : Impartial G
x✝ : Impartial H
k : RightMoves (G + H)
⊢ ∀ (j : RightMoves G), Impartial (moveRight (G + H) (↑toRightMovesAdd (Sum.inl j)))
[PROOFSTEP]
intro i
[GOAL]
case refine'_2.hl
G H : PGame
x✝¹ : Impartial G
x✝ : Impartial H
k : RightMoves (G + H)
i : RightMoves G
⊢ Impartial (moveRight (G + H) (↑toRightMovesAdd (Sum.inl i)))
[PROOFSTEP]
simp only [add_moveRight_inl, add_moveRight_inr]
[GOAL]
case refine'_2.hl
G H : PGame
x✝¹ : Impartial G
x✝ : Impartial H
k : RightMoves (G + H)
i : RightMoves G
⊢ Impartial (moveRight G i + H)
[PROOFSTEP]
apply impartial_add
[GOAL]
case refine'_2.hr
G H : PGame
x✝¹ : Impartial G
x✝ : Impartial H
k : RightMoves (G + H)
⊢ ∀ (j : RightMoves H), Impartial (moveRight (G + H) (↑toRightMovesAdd (Sum.inr j)))
[PROOFSTEP]
intro i
[GOAL]
case refine'_2.hr
G H : PGame
x✝¹ : Impartial G
x✝ : Impartial H
k : RightMoves (G + H)
i : RightMoves H
⊢ Impartial (moveRight (G + H) (↑toRightMovesAdd (Sum.inr i)))
[PROOFSTEP]
simp only [add_moveRight_inl, add_moveRight_inr]
[GOAL]
case refine'_2.hr
G H : PGame
x✝¹ : Impartial G
x✝ : Impartial H
k : RightMoves (G + H)
i : RightMoves H
⊢ Impartial (G + moveRight H i)
[PROOFSTEP]
apply impartial_add
[GOAL]
G H : PGame
x✝² : Impartial G
x✝¹ : Impartial H
x✝ :
  ∀ (y : (x : PGame) ×' (x_1 : PGame) ×' (_ : Impartial x) ×' Impartial x_1),
    (invImage
            (fun a =>
              PSigma.casesOn a fun G snd => PSigma.casesOn snd fun H snd => PSigma.casesOn snd fun x snd => (G, H))
            Prod.instWellFoundedRelationProd).1
        y { fst := G, snd := { fst := H, snd := { fst := x✝², snd := x✝¹ } } } →
      Impartial (y.1 + y.2.1)
i : LeftMoves G
⊢ (invImage
        (fun a => PSigma.casesOn a fun G snd => PSigma.casesOn snd fun H snd => PSigma.casesOn snd fun x snd => (G, H))
        Prod.instWellFoundedRelationProd).1
    { fst := moveLeft G i, snd := { fst := H, snd := { fst := (_ : Impartial (moveLeft G i)), snd := x✝¹ } } }
    { fst := G, snd := { fst := H, snd := { fst := x✝², snd := x✝¹ } } }
[PROOFSTEP]
pgame_wf_tac
[GOAL]
G H : PGame
x✝² : Impartial G
x✝¹ : Impartial H
x✝ :
  ∀ (y : (x : PGame) ×' (x_1 : PGame) ×' (_ : Impartial x) ×' Impartial x_1),
    (invImage
            (fun a =>
              PSigma.casesOn a fun G snd => PSigma.casesOn snd fun H snd => PSigma.casesOn snd fun x snd => (G, H))
            Prod.instWellFoundedRelationProd).1
        y { fst := G, snd := { fst := H, snd := { fst := x✝², snd := x✝¹ } } } →
      Impartial (y.1 + y.2.1)
i : LeftMoves H
⊢ (invImage
        (fun a => PSigma.casesOn a fun G snd => PSigma.casesOn snd fun H snd => PSigma.casesOn snd fun x snd => (G, H))
        Prod.instWellFoundedRelationProd).1
    { fst := G, snd := { fst := moveLeft H i, snd := { fst := x✝², snd := (_ : Impartial (moveLeft H i)) } } }
    { fst := G, snd := { fst := H, snd := { fst := x✝², snd := x✝¹ } } }
[PROOFSTEP]
pgame_wf_tac
[GOAL]
G H : PGame
x✝² : Impartial G
x✝¹ : Impartial H
x✝ :
  ∀ (y : (x : PGame) ×' (x_1 : PGame) ×' (_ : Impartial x) ×' Impartial x_1),
    (invImage
            (fun a =>
              PSigma.casesOn a fun G snd => PSigma.casesOn snd fun H snd => PSigma.casesOn snd fun x snd => (G, H))
            Prod.instWellFoundedRelationProd).1
        y { fst := G, snd := { fst := H, snd := { fst := x✝², snd := x✝¹ } } } →
      Impartial (y.1 + y.2.1)
i : RightMoves G
⊢ (invImage
        (fun a => PSigma.casesOn a fun G snd => PSigma.casesOn snd fun H snd => PSigma.casesOn snd fun x snd => (G, H))
        Prod.instWellFoundedRelationProd).1
    { fst := moveRight G i, snd := { fst := H, snd := { fst := (_ : Impartial (moveRight G i)), snd := x✝¹ } } }
    { fst := G, snd := { fst := H, snd := { fst := x✝², snd := x✝¹ } } }
[PROOFSTEP]
pgame_wf_tac
[GOAL]
G H : PGame
x✝² : Impartial G
x✝¹ : Impartial H
x✝ :
  ∀ (y : (x : PGame) ×' (x_1 : PGame) ×' (_ : Impartial x) ×' Impartial x_1),
    (invImage
            (fun a =>
              PSigma.casesOn a fun G snd => PSigma.casesOn snd fun H snd => PSigma.casesOn snd fun x snd => (G, H))
            Prod.instWellFoundedRelationProd).1
        y { fst := G, snd := { fst := H, snd := { fst := x✝², snd := x✝¹ } } } →
      Impartial (y.1 + y.2.1)
i : RightMoves H
⊢ (invImage
        (fun a => PSigma.casesOn a fun G snd => PSigma.casesOn snd fun H snd => PSigma.casesOn snd fun x snd => (G, H))
        Prod.instWellFoundedRelationProd).1
    { fst := G, snd := { fst := moveRight H i, snd := { fst := x✝², snd := (_ : Impartial (moveRight H i)) } } }
    { fst := G, snd := { fst := H, snd := { fst := x✝², snd := x✝¹ } } }
[PROOFSTEP]
pgame_wf_tac
[GOAL]
G : PGame
x✝ : Impartial G
⊢ Impartial (-G)
[PROOFSTEP]
rw [impartial_def]
[GOAL]
G : PGame
x✝ : Impartial G
⊢ -G ≈ - -G ∧
    (∀ (i : LeftMoves (-G)), Impartial (moveLeft (-G) i)) ∧ ∀ (j : RightMoves (-G)), Impartial (moveRight (-G) j)
[PROOFSTEP]
refine' ⟨_, fun i => _, fun i => _⟩
[GOAL]
case refine'_1
G : PGame
x✝ : Impartial G
⊢ -G ≈ - -G
[PROOFSTEP]
rw [neg_neg]
[GOAL]
case refine'_1
G : PGame
x✝ : Impartial G
⊢ -G ≈ G
[PROOFSTEP]
exact Equiv.symm (neg_equiv_self G)
[GOAL]
case refine'_2
G : PGame
x✝ : Impartial G
i : LeftMoves (-G)
⊢ Impartial (moveLeft (-G) i)
[PROOFSTEP]
rw [moveLeft_neg']
[GOAL]
case refine'_2
G : PGame
x✝ : Impartial G
i : LeftMoves (-G)
⊢ Impartial (-moveRight G (↑toLeftMovesNeg.symm i))
[PROOFSTEP]
apply impartial_neg
[GOAL]
case refine'_3
G : PGame
x✝ : Impartial G
i : RightMoves (-G)
⊢ Impartial (moveRight (-G) i)
[PROOFSTEP]
rw [moveRight_neg']
[GOAL]
case refine'_3
G : PGame
x✝ : Impartial G
i : RightMoves (-G)
⊢ Impartial (-moveLeft G (↑toRightMovesNeg.symm i))
[PROOFSTEP]
apply impartial_neg
[GOAL]
G : PGame
x✝¹ : Impartial G
x✝ :
  ∀ (y : (x : PGame) ×' Impartial x),
    (invImage (fun a => PSigma.casesOn a fun G snd => G) instWellFoundedRelationPGame).1 y { fst := G, snd := x✝¹ } →
      Impartial (-y.1)
i : LeftMoves (-G)
⊢ (invImage (fun a => PSigma.casesOn a fun G snd => G) instWellFoundedRelationPGame).1
    { fst := moveRight G (↑toLeftMovesNeg.symm i), snd := (_ : Impartial (moveRight G (↑toLeftMovesNeg.symm i))) }
    { fst := G, snd := x✝¹ }
[PROOFSTEP]
pgame_wf_tac
[GOAL]
G : PGame
x✝¹ : Impartial G
x✝ :
  ∀ (y : (x : PGame) ×' Impartial x),
    (invImage (fun a => PSigma.casesOn a fun G snd => G) instWellFoundedRelationPGame).1 y { fst := G, snd := x✝¹ } →
      Impartial (-y.1)
i : RightMoves (-G)
⊢ (invImage (fun a => PSigma.casesOn a fun G snd => G) instWellFoundedRelationPGame).1
    { fst := moveLeft G (↑toRightMovesNeg.symm i), snd := (_ : Impartial (moveLeft G (↑toRightMovesNeg.symm i))) }
    { fst := G, snd := x✝¹ }
[PROOFSTEP]
pgame_wf_tac
[GOAL]
G : PGame
inst✝ : Impartial G
h : 0 < G
⊢ False
[PROOFSTEP]
have h' := neg_lt_neg_iff.2 h
[GOAL]
G : PGame
inst✝ : Impartial G
h : 0 < G
h' : -G < -0
⊢ False
[PROOFSTEP]
rw [neg_zero, lt_congr_left (Equiv.symm (neg_equiv_self G))] at h'
[GOAL]
G : PGame
inst✝ : Impartial G
h : 0 < G
h' : G < 0
⊢ False
[PROOFSTEP]
exact (h.trans h').false
[GOAL]
G : PGame
inst✝ : Impartial G
h : G < 0
⊢ False
[PROOFSTEP]
have h' := neg_lt_neg_iff.2 h
[GOAL]
G : PGame
inst✝ : Impartial G
h : G < 0
h' : -0 < -G
⊢ False
[PROOFSTEP]
rw [neg_zero, lt_congr_right (Equiv.symm (neg_equiv_self G))] at h'
[GOAL]
G : PGame
inst✝ : Impartial G
h : G < 0
h' : 0 < G
⊢ False
[PROOFSTEP]
exact (h.trans h').false
[GOAL]
G : PGame
inst✝ : Impartial G
⊢ G ≈ 0 ∨ G ‖ 0
[PROOFSTEP]
rcases lt_or_equiv_or_gt_or_fuzzy G 0 with (h | h | h | h)
[GOAL]
case inl
G : PGame
inst✝ : Impartial G
h : G < 0
⊢ G ≈ 0 ∨ G ‖ 0
[PROOFSTEP]
exact ((nonneg G) h).elim
[GOAL]
case inr.inl
G : PGame
inst✝ : Impartial G
h : G ≈ 0
⊢ G ≈ 0 ∨ G ‖ 0
[PROOFSTEP]
exact Or.inl h
[GOAL]
case inr.inr.inl
G : PGame
inst✝ : Impartial G
h : 0 < G
⊢ G ≈ 0 ∨ G ‖ 0
[PROOFSTEP]
exact ((nonpos G) h).elim
[GOAL]
case inr.inr.inr
G : PGame
inst✝ : Impartial G
h : G ‖ 0
⊢ G ≈ 0 ∨ G ‖ 0
[PROOFSTEP]
exact Or.inr h
[GOAL]
G : PGame
inst✝ : Impartial G
H : PGame
⊢ H ≈ G ↔ H + G ≈ 0
[PROOFSTEP]
rw [Game.PGame.equiv_iff_game_eq, ← @add_right_cancel_iff _ _ _ ⟦G⟧, mk'_add_self, ← quot_add,
  Game.PGame.equiv_iff_game_eq]
[GOAL]
G : PGame
inst✝ : Impartial G
H : PGame
⊢ Quotient.mk setoid (H + G) = 0 ↔ Quotient.mk setoid (H + G) = Quotient.mk setoid 0
[PROOFSTEP]
rfl
[GOAL]
G : PGame
inst✝ : Impartial G
H : PGame
⊢ G ≈ H ↔ G + H ≈ 0
[PROOFSTEP]
rw [Game.PGame.equiv_iff_game_eq, ← @add_left_cancel_iff _ _ _ ⟦G⟧, mk'_add_self, ← quot_add,
  Game.PGame.equiv_iff_game_eq]
[GOAL]
G : PGame
inst✝ : Impartial G
H : PGame
⊢ 0 = Quotient.mk setoid (G + H) ↔ Quotient.mk setoid (G + H) = Quotient.mk setoid 0
[PROOFSTEP]
exact ⟨Eq.symm, Eq.symm⟩
[GOAL]
G✝ : PGame
inst✝¹ : Impartial G✝
G : PGame
inst✝ : Impartial G
⊢ G ≤ 0 ↔ 0 ≤ G
[PROOFSTEP]
rw [← zero_le_neg_iff, le_congr_right (neg_equiv_self G)]
[GOAL]
G✝ : PGame
inst✝¹ : Impartial G✝
G : PGame
inst✝ : Impartial G
⊢ G ⧏ 0 ↔ 0 ⧏ G
[PROOFSTEP]
rw [← zero_lf_neg_iff, lf_congr_right (neg_equiv_self G)]
[GOAL]
G : PGame
inst✝ : Impartial G
⊢ (∀ (i : LeftMoves G), moveLeft G i ‖ 0) ↔ G ≈ 0
[PROOFSTEP]
refine' ⟨fun hb => _, fun hp i => _⟩
[GOAL]
case refine'_1
G : PGame
inst✝ : Impartial G
hb : ∀ (i : LeftMoves G), moveLeft G i ‖ 0
⊢ G ≈ 0
[PROOFSTEP]
rw [equiv_zero_iff_le G, le_zero_lf]
[GOAL]
case refine'_1
G : PGame
inst✝ : Impartial G
hb : ∀ (i : LeftMoves G), moveLeft G i ‖ 0
⊢ ∀ (i : LeftMoves G), moveLeft G i ⧏ 0
[PROOFSTEP]
exact fun i => (hb i).1
[GOAL]
case refine'_2
G : PGame
inst✝ : Impartial G
hp : G ≈ 0
i : LeftMoves G
⊢ moveLeft G i ‖ 0
[PROOFSTEP]
rw [fuzzy_zero_iff_lf]
[GOAL]
case refine'_2
G : PGame
inst✝ : Impartial G
hp : G ≈ 0
i : LeftMoves G
⊢ moveLeft G i ⧏ 0
[PROOFSTEP]
exact hp.1.moveLeft_lf i
[GOAL]
G : PGame
inst✝ : Impartial G
⊢ (∀ (j : RightMoves G), moveRight G j ‖ 0) ↔ G ≈ 0
[PROOFSTEP]
refine' ⟨fun hb => _, fun hp i => _⟩
[GOAL]
case refine'_1
G : PGame
inst✝ : Impartial G
hb : ∀ (j : RightMoves G), moveRight G j ‖ 0
⊢ G ≈ 0
[PROOFSTEP]
rw [equiv_zero_iff_ge G, zero_le_lf]
[GOAL]
case refine'_1
G : PGame
inst✝ : Impartial G
hb : ∀ (j : RightMoves G), moveRight G j ‖ 0
⊢ ∀ (j : RightMoves G), 0 ⧏ moveRight G j
[PROOFSTEP]
exact fun i => (hb i).2
[GOAL]
case refine'_2
G : PGame
inst✝ : Impartial G
hp : G ≈ 0
i : RightMoves G
⊢ moveRight G i ‖ 0
[PROOFSTEP]
rw [fuzzy_zero_iff_gf]
[GOAL]
case refine'_2
G : PGame
inst✝ : Impartial G
hp : G ≈ 0
i : RightMoves G
⊢ 0 ⧏ moveRight G i
[PROOFSTEP]
exact hp.2.lf_moveRight i
[GOAL]
G : PGame
inst✝ : Impartial G
⊢ (∃ i, moveLeft G i ≈ 0) ↔ G ‖ 0
[PROOFSTEP]
refine' ⟨fun ⟨i, hi⟩ => (fuzzy_zero_iff_gf G).2 (lf_of_le_moveLeft hi.2), fun hn => _⟩
[GOAL]
G : PGame
inst✝ : Impartial G
hn : G ‖ 0
⊢ ∃ i, moveLeft G i ≈ 0
[PROOFSTEP]
rw [fuzzy_zero_iff_gf G, zero_lf_le] at hn
[GOAL]
G : PGame
inst✝ : Impartial G
hn : ∃ i, 0 ≤ moveLeft G i
⊢ ∃ i, moveLeft G i ≈ 0
[PROOFSTEP]
cases' hn with i hi
[GOAL]
case intro
G : PGame
inst✝ : Impartial G
i : LeftMoves G
hi : 0 ≤ moveLeft G i
⊢ ∃ i, moveLeft G i ≈ 0
[PROOFSTEP]
exact ⟨i, (equiv_zero_iff_ge _).2 hi⟩
[GOAL]
G : PGame
inst✝ : Impartial G
⊢ (∃ j, moveRight G j ≈ 0) ↔ G ‖ 0
[PROOFSTEP]
refine' ⟨fun ⟨i, hi⟩ => (fuzzy_zero_iff_lf G).2 (lf_of_moveRight_le hi.1), fun hn => _⟩
[GOAL]
G : PGame
inst✝ : Impartial G
hn : G ‖ 0
⊢ ∃ j, moveRight G j ≈ 0
[PROOFSTEP]
rw [fuzzy_zero_iff_lf G, lf_zero_le] at hn
[GOAL]
G : PGame
inst✝ : Impartial G
hn : ∃ j, moveRight G j ≤ 0
⊢ ∃ j, moveRight G j ≈ 0
[PROOFSTEP]
cases' hn with i hi
[GOAL]
case intro
G : PGame
inst✝ : Impartial G
i : RightMoves G
hi : moveRight G i ≤ 0
⊢ ∃ j, moveRight G j ≈ 0
[PROOFSTEP]
exact ⟨i, (equiv_zero_iff_le _).2 hi⟩