Theorem: shuffleCancelable (Advent/List/Shuffles.lean)

State before:
n : Nat
i : Fin (n + 2)
⊢ shuffleIndex (shuffleIndex i) = i
Tactic:
cases i with | mk v lt => 
cases v with
| zero => simp [shuffleIndex] 
| succ v1 => cases v1 <;> simp [shuffleIndex]
State after:
no goals

State before:
case mk
n v : Nat
lt : v < n + 2
⊢ shuffleIndex (shuffleIndex { val := v, isLt := lt }) = { val := v, isLt := lt }
Tactic:
cases v with
| zero => simp [shuffleIndex] 
| succ v1 => cases v1 <;> simp [shuffleIndex]
State after:
no goals

State before:
case mk.zero
n : Nat
lt : Nat.zero < n + 2
⊢ shuffleIndex (shuffleIndex { val := Nat.zero, isLt := lt }) = { val := Nat.zero, isLt := lt }
Tactic:
simp [shuffleIndex]
State after:
no goals

State before:
case mk.succ
n v1 : Nat
lt : Nat.succ v1 < n + 2
⊢ shuffleIndex (shuffleIndex { val := Nat.succ v1, isLt := lt }) = { val := Nat.succ v1, isLt := lt }
Tactic:
cases v1 <;> simp [shuffleIndex]
State after:
no goals