next hd tl ih =>
split
next hHd =>
  simp [hHd] at h
  simp [_sizeOf_1]
  apply Nat.add_lt_add_left
  apply ih
  assumption
next hHd =>
  clear h hHd
  apply Nat.lt_of_le_of_lt (sizeOf_filter _ _)
  rw [Nat.add_comm, Nat.add_comm 1, Nat.add_one, Nat.add_succ]
  apply Nat.succ_le_succ
  apply Nat.le_add_right
case cons
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
head✝ : α
tail✝ : List α
tail_ih✝ : ¬filter f tail✝ = tail✝ → sizeOf (filter f tail✝) < sizeOf tail✝
h :
  ¬(match f head✝ with
      | true => head✝ :: filter f tail✝
      | false => filter f tail✝) =
      head✝ :: tail✝
⊢ sizeOf
      (match f head✝ with
      | true => head✝ :: filter f tail✝
      | false => filter f tail✝) <
    1 + sizeOf head✝ + sizeOf tail✝
no goals