α : Type u_1
p : α → Bool
a : α
l : List α
⊢ (match p a with
    | true => a :: filter p l
    | false => filter p l) <+
    a :: l
α : Type u_1
p : α → Bool
a : α
l : List α
⊢ filter p (a :: l) <+ a :: l
rw [filter]
no goals
α : Type u_1
p : α → Bool
a : α
l : List α
⊢ (match p a with
    | true => a :: filter p l
    | false => filter p l) <+
    a :: l
split <;> simp [Sublist.cons, Sublist.cons₂, filter_sublist l]