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