Theorem: List.get?_cons (One.lean)

State before:
α : Type u_1
h : α
tail : List α
n : ℕ
hn : n > 0
⊢ get? (h :: tail) n = get? tail (n - 1)
Tactic:
conv => left; unfold List.get?
State after:
α : Type u_1
h : α
tail : List α
n : ℕ
hn : n > 0
⊢ (match h :: tail, n with
    | a :: tail, 0 => some a
    | head :: as, Nat.succ n => get? as n
    | x, x_1 => none) =
    get? tail (n - 1)

State before:
α : Type u_1
h : α
tail : List α
n : ℕ
hn : n > 0
⊢ (match h :: tail, n with
    | a :: tail, 0 => some a
    | head :: as, Nat.succ n => get? as n
    | x, x_1 => none) =
    get? tail (n - 1)
Tactic:
cases n with
| zero => simp only at hn
| succ n => simp only [ge_iff_le, Nat.succ_sub_succ_eq_sub, nonpos_iff_eq_zero, tsub_zero]
State after:
no goals

State before:
case zero
α : Type u_1
h : α
tail : List α
hn : Nat.zero > 0
⊢ (match h :: tail, Nat.zero with
    | a :: tail, 0 => some a
    | head :: as, Nat.succ n => get? as n
    | x, x_1 => none) =
    get? tail (Nat.zero - 1)
Tactic:
simp only at hn
State after:
no goals

State before:
case succ
α : Type u_1
h : α
tail : List α
n : ℕ
hn : Nat.succ n > 0
⊢ (match h :: tail, Nat.succ n with
    | a :: tail, 0 => some a
    | head :: as, Nat.succ n => get? as n
    | x, x_1 => none) =
    get? tail (Nat.succ n - 1)
Tactic:
simp only [ge_iff_le, Nat.succ_sub_succ_eq_sub, nonpos_iff_eq_zero, tsub_zero]
State after:
no goals