induction xs with
| nil => simp [filter, filterSpec]
| cons x xs ih =>
  simp only [filter, filterSpec]
  cases p x with
  | true => simp only [ite_true, ih]
  | false => simp only [ite_false, ih]
α✝ : Type u_1
p : α✝ → Bool
xs : List α✝
⊢ filter p xs = filterSpec p xs
no goals