[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
