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

State before:
α : Type u_1
x y : α
xs : List α
i : Fin (List.length xs + 2)
⊢ List.get (x :: y :: xs) i = List.get (y :: x :: xs) (shuffleIndex i)
Tactic:
cases i with | mk v vlt => 
cases v 
. simp [List.get]
. case succ v1 => cases v1 <;> simp [List.get]
State after:
no goals

State before:
case mk
α : Type u_1
x y : α
xs : List α
v : Nat
vlt : v < List.length xs + 2
⊢ List.get (x :: y :: xs) { val := v, isLt := vlt } = List.get (y :: x :: xs) (shuffleIndex { val := v, isLt := vlt })
Tactic:
cases v
State after:
case mk.zero
α : Type u_1
x y : α
xs : List α
vlt : Nat.zero < List.length xs + 2
⊢ List.get (x :: y :: xs) { val := Nat.zero, isLt := vlt } =
    List.get (y :: x :: xs) (shuffleIndex { val := Nat.zero, isLt := vlt })

case mk.succ
α : Type u_1
x y : α
xs : List α
n✝ : Nat
vlt : Nat.succ n✝ < List.length xs + 2
⊢ List.get (x :: y :: xs) { val := Nat.succ n✝, isLt := vlt } =
    List.get (y :: x :: xs) (shuffleIndex { val := Nat.succ n✝, isLt := vlt })

State before:
case mk.zero
α : Type u_1
x y : α
xs : List α
vlt : Nat.zero < List.length xs + 2
⊢ List.get (x :: y :: xs) { val := Nat.zero, isLt := vlt } =
    List.get (y :: x :: xs) (shuffleIndex { val := Nat.zero, isLt := vlt })

case mk.succ
α : Type u_1
x y : α
xs : List α
n✝ : Nat
vlt : Nat.succ n✝ < List.length xs + 2
⊢ List.get (x :: y :: xs) { val := Nat.succ n✝, isLt := vlt } =
    List.get (y :: x :: xs) (shuffleIndex { val := Nat.succ n✝, isLt := vlt })
Tactic:
. simp [List.get]
State after:
case mk.succ
α : Type u_1
x y : α
xs : List α
n✝ : Nat
vlt : Nat.succ n✝ < List.length xs + 2
⊢ List.get (x :: y :: xs) { val := Nat.succ n✝, isLt := vlt } =
    List.get (y :: x :: xs) (shuffleIndex { val := Nat.succ n✝, isLt := vlt })

State before:
case mk.succ
α : Type u_1
x y : α
xs : List α
n✝ : Nat
vlt : Nat.succ n✝ < List.length xs + 2
⊢ List.get (x :: y :: xs) { val := Nat.succ n✝, isLt := vlt } =
    List.get (y :: x :: xs) (shuffleIndex { val := Nat.succ n✝, isLt := vlt })
Tactic:
. case succ v1 => cases v1 <;> simp [List.get]
State after:
no goals

State before:
α : Type u_1
x y : α
xs : List α
v1 : Nat
vlt : Nat.succ v1 < List.length xs + 2
⊢ List.get (x :: y :: xs) { val := Nat.succ v1, isLt := vlt } =
    List.get (y :: x :: xs) (shuffleIndex { val := Nat.succ v1, isLt := vlt })
Tactic:
cases v1 <;> simp [List.get]
State after:
no goals