obtain ha | ha := Bool.eq_false_or_eq_true (p a)
α✝ : 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
h : (if p a = true then a :: filter p (b :: as) else filter p (b :: as)) ≠ []
⊢ (if p a = true then a :: filter p (b :: as) else filter p (b :: as)).getLast ⋯ = (b :: as).getLast ⋯
case inl
α✝ : 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
h : (if p a = true then a :: filter p (b :: as) else filter p (b :: as)) ≠ []
ha : p a = true
⊢ (if p a = true then a :: filter p (b :: as) else filter p (b :: as)).getLast ⋯ = (b :: as).getLast ⋯

case inr
α✝ : 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
h : (if p a = true then a :: filter p (b :: as) else filter p (b :: as)) ≠ []
ha : p a = false
⊢ (if p a = true then a :: filter p (b :: as) else filter p (b :: as)).getLast ⋯ = (b :: as).getLast ⋯