no goals
R : Type u
ι : Type w
s : Finset ι
S : Type u_1
inst✝ : Semiring S
f : ι → S[X]
⊢ natDegree (∑ i in s, f i) ≤ Finset.fold max 0 (natDegree ∘ f) s
simpa using natDegree_multiset_sum_le (s.val.map f)