-- Mathlib/MeasureTheory/Integral/MeanInequalities.lean
theorem lintegral_rpow_add_le_add_eLpNorm_mul_lintegral_rpow_add {p q : ℝ}
    (hpq : p.IsConjExponent q) {f g : α → ℝ≥0∞} (hf : AEMeasurable f μ)
    (hf_top : (∫⁻ a, f a ^ p ∂μ) ≠ ⊤) (hg : AEMeasurable g μ) (hg_top : (∫⁻ a, g a ^ p ∂μ) ≠ ⊤) :
    (∫⁻ a, (f + g) a ^ p ∂μ) ≤
      ((∫⁻ a, f a ^ p ∂μ) ^ (1 / p) + (∫⁻ a, g a ^ p ∂μ) ^ (1 / p)) *
        (∫⁻ a, (f a + g a) ^ p ∂μ) ^ (1 / q)

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.IsConjExponent q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤
hg : AEMeasurable g μ
hg_top : ∫⁻ (a : α), g a ^ p ∂μ ≠ ⊤
h_add_m : AEMeasurable (fun a => (f + g) a ^ (p - 1)) μ
h_add_apply : ∫⁻ (a : α), (f + g) a * (f + g) a ^ (p - 1) ∂μ = ∫⁻ (a : α), (f a + g a) * (f + g) a ^ (p - 1) ∂μ
⊢ ∫⁻ (a : α), (f + g) a * (f + g) a ^ (p - 1) ∂μ =
    ∫⁻ (a : α), f a * (f + g) a ^ (p - 1) ∂μ + ∫⁻ (a : α), g a * (f + g) a ^ (p - 1) ∂μ

Tactic:
simp_rw [h_add_apply, add_mul]

Result:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.IsConjExponent q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤
hg : AEMeasurable g μ
hg_top : ∫⁻ (a : α), g a ^ p ∂μ ≠ ⊤
h_add_m : AEMeasurable (fun a => (f + g) a ^ (p - 1)) μ
h_add_apply : ∫⁻ (a : α), (f + g) a * (f + g) a ^ (p - 1) ∂μ = ∫⁻ (a : α), (f a + g a) * (f + g) a ^ (p - 1) ∂μ
⊢ ∫⁻ (a : α), f a * (f + g) a ^ (p - 1) + g a * (f + g) a ^ (p - 1) ∂μ =
    ∫⁻ (a : α), f a * (f + g) a ^ (p - 1) ∂μ + ∫⁻ (a : α), g a * (f + g) a ^ (p - 1) ∂μ

Proof state:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.IsConjExponent q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤
hg : AEMeasurable g μ
hg_top : ∫⁻ (a : α), g a ^ p ∂μ ≠ ⊤
a : α
h_zero : (f + g) a = 0
⊢ (f + g) a ^ p ≤ (f + g) a * (f + g) a ^ (p - 1)

Tactic:
rw [h_zero, ENNReal.zero_rpow_of_pos hpq.pos]

Result:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.IsConjExponent q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤
hg : AEMeasurable g μ
hg_top : ∫⁻ (a : α), g a ^ p ∂μ ≠ ⊤
a : α
h_zero : (f + g) a = 0
⊢ 0 ≤ 0 * 0 ^ (p - 1)

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.IsConjExponent q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤
hg : AEMeasurable g μ
hg_top : ∫⁻ (a : α), g a ^ p ∂μ ≠ ⊤
⊢ ∫⁻ (a : α), f a * (f + g) a ^ (p - 1) ∂μ + ∫⁻ (a : α), g a * (f + g) a ^ (p - 1) ∂μ ≤
    ((∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) + (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p)) *
      (∫⁻ (a : α), (f a + g a) ^ p ∂μ) ^ (1 / q)

Tactic:
rw [add_mul]

Result:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.IsConjExponent q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤
hg : AEMeasurable g μ
hg_top : ∫⁻ (a : α), g a ^ p ∂μ ≠ ⊤
⊢ ∫⁻ (a : α), f a * (f + g) a ^ (p - 1) ∂μ + ∫⁻ (a : α), g a * (f + g) a ^ (p - 1) ∂μ ≤
    (∫⁻ (a : α), f a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), (f a + g a) ^ p ∂μ) ^ (1 / q) +
      (∫⁻ (a : α), g a ^ p ∂μ) ^ (1 / p) * (∫⁻ (a : α), (f a + g a) ^ p ∂μ) ^ (1 / q)

Proof state:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.IsConjExponent q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤
hg : AEMeasurable g μ
hg_top : ∫⁻ (a : α), g a ^ p ∂μ ≠ ⊤
a : α
h_zero : (f + g) a = 0
⊢ 0 ≤ 0 * 0 ^ (p - 1)

Tactic:
exact zero_le _

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.IsConjExponent q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤
hg : AEMeasurable g μ
hg_top : ∫⁻ (a : α), g a ^ p ∂μ ≠ ⊤
h_add_m : AEMeasurable (fun a => (f + g) a ^ (p - 1)) μ
h_add_apply : ∫⁻ (a : α), (f + g) a * (f + g) a ^ (p - 1) ∂μ = ∫⁻ (a : α), (f a + g a) * (f + g) a ^ (p - 1) ∂μ
⊢ ∫⁻ (a : α), f a * (f + g) a ^ (p - 1) + g a * (f + g) a ^ (p - 1) ∂μ =
    ∫⁻ (a : α), f a * (f + g) a ^ (p - 1) ∂μ + ∫⁻ (a : α), g a * (f + g) a ^ (p - 1) ∂μ

Tactic:
rw [lintegral_add_left' (hf.mul h_add_m)]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.IsConjExponent q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤
hg : AEMeasurable g μ
hg_top : ∫⁻ (a : α), g a ^ p ∂μ ≠ ⊤
⊢ ∫⁻ (a : α), (f + g) a * (f + g) a ^ (p - 1) ∂μ =
    ∫⁻ (a : α), f a * (f + g) a ^ (p - 1) ∂μ + ∫⁻ (a : α), g a * (f + g) a ^ (p - 1) ∂μ

Tactic:
have h_add_m : AEMeasurable (fun a : α => (f + g) a ^ (p - 1 : ℝ)) μ :=
  (hf.add hg).pow_const _

Result:
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.IsConjExponent q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤
hg : AEMeasurable g μ
hg_top : ∫⁻ (a : α), g a ^ p ∂μ ≠ ⊤
h_add_m : AEMeasurable (fun a => (f + g) a ^ (p - 1)) μ
⊢ ∫⁻ (a : α), (f + g) a * (f + g) a ^ (p - 1) ∂μ =
    ∫⁻ (a : α), f a * (f + g) a ^ (p - 1) ∂μ + ∫⁻ (a : α), g a * (f + g) a ^ (p - 1) ∂μ

Proof state:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.IsConjExponent q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤
hg : AEMeasurable g μ
hg_top : ∫⁻ (a : α), g a ^ p ∂μ ≠ ⊤
a : α
h_zero : ¬(f + g) a = 0
h_top : (f + g) a = ⊤
⊢ (f + g) a ^ p ≤ (f + g) a * (f + g) a ^ (p - 1)

Tactic:
rw [h_top, ENNReal.top_rpow_of_pos hpq.sub_one_pos, ENNReal.top_mul_top]

Result:
case pos
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.IsConjExponent q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤
hg : AEMeasurable g μ
hg_top : ∫⁻ (a : α), g a ^ p ∂μ ≠ ⊤
a : α
h_zero : ¬(f + g) a = 0
h_top : (f + g) a = ⊤
⊢ ⊤ ^ p ≤ ⊤

Proof state:
case neg
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.IsConjExponent q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤
hg : AEMeasurable g μ
hg_top : ∫⁻ (a : α), g a ^ p ∂μ ≠ ⊤
a : α
h_zero : ¬(f + g) a = 0
h_top : ¬(f + g) a = ⊤
⊢ (f + g) a ^ p = (f + g) a * (f + g) a ^ (p - 1)

Tactic:
nth_rw 2 [← ENNReal.rpow_one ((f + g) a)]

Result:
case neg
α : Type u_1
inst✝ : MeasurableSpace α
μ : Measure α
p q : ℝ
hpq : p.IsConjExponent q
f g : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_top : ∫⁻ (a : α), f a ^ p ∂μ ≠ ⊤
hg : AEMeasurable g μ
hg_top : ∫⁻ (a : α), g a ^ p ∂μ ≠ ⊤
a : α
h_zero : ¬(f + g) a = 0
h_top : ¬(f + g) a = ⊤
⊢ (f + g) a ^ p = (f + g) a ^ 1 * (f + g) a ^ (p - 1)