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 h_2
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
hd : α
tl : List α
ih : ¬filter f tl = tl → sizeOf (filter f tl) < sizeOf tl
h :
  ¬(match f hd with
      | true => hd :: filter f tl
      | false => filter f tl) =
      hd :: tl
x✝ : Bool
heq✝ : f hd = false
⊢ sizeOf (filter f tl) < 1 + sizeOf hd + sizeOf tl
no goals