no goals
ι : Type ?u.32017
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a : α
x✝ : [a] ≠ []
⊢ getLast [a] x✝ ∈ [a]
simp only [getLast, mem_singleton]
ι : Type ?u.32017
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a b : α
l : List α
h : a :: b :: l ≠ []
⊢ getLast (b :: l) (_ : b :: l ≠ []) ∈ b :: l
ι : Type ?u.32017
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a b : α
l : List α
h : a :: b :: l ≠ []
⊢ getLast (a :: b :: l) h ∈ b :: l
rw [getLast_cons_cons]
no goals
ι : Type ?u.32017
α : Type u
β : Type v
γ : Type w
δ : Type x
l₁ l₂ : List α
a b : α
l : List α
h : a :: b :: l ≠ []
⊢ getLast (b :: l) (_ : b :: l ≠ []) ∈ b :: l
exact getLast_mem (cons_ne_nil b l)