no goals
α : Type u_1
a : α
h : [a] ≠ []
⊢ getLast [a] h = get [a] { val := length [a] - 1, isLt := (_ : length [a] - 1 < length [a]) }
rw [getLast_singleton, get_singleton]
α : Type u_1
a b : α
l : List α
h : a :: b :: l ≠ []
⊢ get (b :: l) { val := length (b :: l) - 1, isLt := (_ : length (b :: l) - 1 < length (b :: l)) } =
    get (a :: b :: l) { val := length (a :: b :: l) - 1, isLt := (_ : length (a :: b :: l) - 1 < length (a :: b :: l)) }

α : Type u_1
a b : α
l : List α
h : a :: b :: l ≠ []
⊢ b :: l ≠ []
α : Type u_1
a b : α
l : List α
h : a :: b :: l ≠ []
⊢ getLast (a :: b :: l) h =
    get (a :: b :: l) { val := length (a :: b :: l) - 1, isLt := (_ : length (a :: b :: l) - 1 < length (a :: b :: l)) }
rw [getLast_cons', getLast_eq_get (b :: l)]
α : Type u_1
a b : α
l : List α
h : a :: b :: l ≠ []
⊢ b :: l ≠ []
α : Type u_1
a b : α
l : List α
h : a :: b :: l ≠ []
⊢ get (b :: l) { val := length (b :: l) - 1, isLt := (_ : length (b :: l) - 1 < length (b :: l)) } =
    get (a :: b :: l) { val := length (a :: b :: l) - 1, isLt := (_ : length (a :: b :: l) - 1 < length (a :: b :: l)) }

α : Type u_1
a b : α
l : List α
h : a :: b :: l ≠ []
⊢ b :: l ≠ []
{rfl}
no goals
α : Type u_1
a b : α
l : List α
h : a :: b :: l ≠ []
⊢ b :: l ≠ []
exact cons_ne_nil b l