-- Module: Mathlib.MeasureTheory.Integral.MeanInequalities
Goal:
α : Type u_1
inst : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.HolderConjugate q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hg : AEMeasurable g μ
h_add_zero : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ 0
h_add_top : ∫⁻ (a : α), (f + g) a ^ p ∂μ ≠ ∞
h0_rpow : (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≠ 0
h :
  1 ≤
    (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (-(1 / p)) *
      ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p))
rwa :
  ∀
    (h :
      (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) * 1 ≤
        (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) *
          ((∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (-(1 / p)) *
            ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)))),
    (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
rwa₁ :
  ∀
    (h :
      (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) * 1 ≤
        (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (-(1 / p)) *
          ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p))),
    (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
rwa₂ :
  ∀
    (h :
      (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) * 1 ≤
        (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p + -(1 / p)) *
          ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p))),
    (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
rwa₃ :
  ∀
    (h :
      (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) * 1 ≤
        (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p - 1 / p) *
          ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p))),
    (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
rwa₄ :
  ∀
    (h :
      (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) * 1 ≤
        HPow.hPow (β := ℝ) (∫⁻ (a : α), (f + g) a ^ p ∂μ) 0 *
          ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p))),
    (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
rwa₅ :
  ∀
    (h :
      (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) * 1 ≤
        1 * ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p))),
    (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
rwa₆ :
  ∀
    (h :
      (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) * 1 ≤
        (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)),
    (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
rwa₇ rwa₈ rwa₉ rwa₁₀ :
  ∀
    (h :
      (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤
        (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)),
    (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)
⊢ (∫⁻ (a : α), (f + g) a ^ p ∂μ) ^ (1 / p) ≤ (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)

Tactic:
rwa [← ENNReal.mul_le_mul_iff_right h0_rpow (by finiteness),
      ← mul_assoc, ← rpow_add _ _ h_add_zero h_add_top, ←
      sub_eq_add_neg, _root_.sub_self, rpow_zero, one_mul, mul_one] at h

Premises used: ENNReal.rpow_add, sub_self, mul_assoc, sub_eq_add_neg, ENNReal.rpow_zero, ENNReal.mul_le_mul_iff_right, mul_one, one_mul