no goals
ι : Type u
s : Finset ι
f : ι → ℝ≥0
n : ℕ
⊢ ↑((∑ x in s, f x) ^ (n + 1)) / ↑(card s) ^ n ≤ ↑(∑ x in s, f x ^ (n + 1))
simpa only [← NNReal.coe_le_coe, NNReal.coe_sum, Nonneg.coe_div, NNReal.coe_pow] using
  @Real.pow_sum_div_card_le_sum_pow ι s (((↑) : ℝ≥0 → ℝ) ∘ f) n fun _ _ => NNReal.coe_nonneg _