induction xs with
| nil => simp [length]
| cons x xs ih =>
   simp only [filter]
   cases (g x) with
   | true =>
     simp only
     apply Nat.succ_le_succ
     exact ih
   | false =>
     simp only
     apply Nat.le.step
     exact ih
α : Type u_1
g : α → Bool
xs : List α
⊢ length (filter g xs) ≤ length xs
no goals