no goals
α : Type u
β : Type v
a b : α
inst✝ : CommSemiring α
I : Ideal α
ι : Type u_1
s : Finset ι
f : ι → α
n : ℕ
⊢ (∑ i in s, f i) ^ (Finset.card s * n + 1) ∈ span ((fun i => f i ^ (n + 1)) '' ↑s)
simpa only [Multiset.card_map, Multiset.map_map, comp_apply, Multiset.toFinset_map,
  Finset.coe_image, Finset.val_toFinset] using pow_multiset_sum_mem_span_pow (s.1.map f) n