rw [Nat.add_comm, Nat.add_comm 1, Nat.add_one, Nat.add_succ]
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
hd : α
tl : List α
ih : ¬filter f tl = tl → sizeOf (filter f tl) < sizeOf tl
x✝ : Bool
⊢ sizeOf tl < 1 + sizeOf hd + sizeOf tl
α : Type u_1
inst✝ : SizeOf α
f : α → Bool
hd : α
tl : List α
ih : ¬filter f tl = tl → sizeOf (filter f tl) < sizeOf tl
x✝ : Bool
⊢ sizeOf tl < Nat.succ (sizeOf tl + sizeOf hd)