no goals
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hp : 1 ≤ p
hf : ∀ (i : ι), i ∈ s → 0 ≤ f i
⊢ (∑ i in s, f i) ^ p ≤ ↑(card s) ^ (p - 1) * ∑ i in s, f i ^ p
convert rpow_sum_le_const_mul_sum_rpow s f hp using 2 <;> apply sum_congr rfl <;> intro i hi <;>
  simp only [abs_of_nonneg, hf i hi]