rw [List.getLast_cons_cons] at h' ⊢
α✝ : Type u_1
l l' l₀ l₁ l₂ : List α✝
a✝ b✝ : α✝
m n : ℕ
α : Type u_2
p : α → Bool
a b : α
as : List α
h : filter p (a :: b :: as) ≠ []
h' : p ((a :: b :: as).getLast ⋯) = true
⊢ (filter p (a :: b :: as)).getLast h = (a :: b :: as).getLast ⋯
α✝ : Type u_1
l l' l₀ l₁ l₂ : List α✝
a✝ b✝ : α✝
m n : ℕ
α : Type u_2
p : α → Bool
a b : α
as : List α
h : filter p (a :: b :: as) ≠ []
h' : p ((b :: as).getLast ⋯) = true
⊢ (filter p (a :: b :: as)).getLast h = (b :: as).getLast ⋯