no goals
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hp : 1 ≤ p
hf : ∀ (i : ι), i ∈ s → 0 ≤ f i
hg : ∀ (i : ι), i ∈ s → 0 ≤ g i
⊢ (∑ i in s, (f i + g i) ^ p) ^ (1 / p) ≤ (∑ i in s, f i ^ p) ^ (1 / p) + (∑ i in s, g i ^ p) ^ (1 / p)
convert Lp_add_le s f g hp using 2 <;> [skip;congr 1;congr 1] <;> apply sum_congr rfl <;>
    intro i hi <;>
  simp only [abs_of_nonneg, hf i hi, hg i hi, add_nonneg]