no goals
α : Type ?u.87760
x : α
xs : List α
n : Nat
h : n = length xs
⊢ n < length (x :: xs)
simp [h]
α : Type u_1
x : α
xs : List α
n : Nat
h : n = length xs
⊢ get (x :: xs) { val := n, isLt := (_ : n < succ (length xs)) } =
    get (x :: xs) { val := length (x :: xs) - 1, isLt := (_ : length (x :: xs) - 1 < length (x :: xs)) }
α : Type u_1
x : α
xs : List α
n : Nat
h : n = length xs
⊢ get (x :: xs) { val := n, isLt := (_ : n < succ (length xs)) } = getLast (x :: xs) (_ : x :: xs ≠ [])
rw [getLast_eq_get]
case refl
α : Type u_1
x : α
xs : List α
⊢ get (x :: xs) { val := length xs, isLt := (_ : length xs < succ (length xs)) } =
    get (x :: xs) { val := length (x :: xs) - 1, isLt := (_ : length (x :: xs) - 1 < length (x :: xs)) }
α : Type u_1
x : α
xs : List α
n : Nat
h : n = length xs
⊢ get (x :: xs) { val := n, isLt := (_ : n < succ (length xs)) } =
    get (x :: xs) { val := length (x :: xs) - 1, isLt := (_ : length (x :: xs) - 1 < length (x :: xs)) }
cases h
no goals
case refl
α : Type u_1
x : α
xs : List α
⊢ get (x :: xs) { val := length xs, isLt := (_ : length xs < succ (length xs)) } =
    get (x :: xs) { val := length (x :: xs) - 1, isLt := (_ : length (x :: xs) - 1 < length (x :: xs)) }
rfl