-- Mathlib/Analysis/MeanInequalities.lean
theorem Lp_add_le_hasSum {f g : ι → ℝ≥0} {A B : ℝ≥0} {p : ℝ} (hp : 1 ≤ p)
    (hf : HasSum (fun i => f i ^ p) (A ^ p)) (hg : HasSum (fun i => g i ^ p) (B ^ p)) :
    ∃ C, C ≤ A + B ∧ HasSum (fun i => (f i + g i) ^ p) (C ^ p)

Proof state:
ι : Type u
f g : ι → ℝ≥0
A B : ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : HasSum (fun i => f i ^ p) (A ^ p)
hg : HasSum (fun i => g i ^ p) (B ^ p)
⊢ ∃ C ≤ A + B, HasSum (fun i => (f i + g i) ^ p) (C ^ p)

Tactic:
have hp' : p ≠ 0 := (lt_of_lt_of_le zero_lt_one hp).ne'

Result:
ι : Type u
f g : ι → ℝ≥0
A B : ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : HasSum (fun i => f i ^ p) (A ^ p)
hg : HasSum (fun i => g i ^ p) (B ^ p)
hp' : p ≠ 0
⊢ ∃ C ≤ A + B, HasSum (fun i => (f i + g i) ^ p) (C ^ p)

Proof state:
case intro
ι : Type u
f g : ι → ℝ≥0
A B : ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : HasSum (fun i => f i ^ p) (A ^ p)
hg : HasSum (fun i => g i ^ p) (B ^ p)
hp' : p ≠ 0
H₁ : Summable fun i => (f i + g i) ^ p
H₂ : (∑' (i : ι), (f i + g i) ^ p) ^ (1 / p) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)
⊢ ∃ C ≤ A + B, HasSum (fun i => (f i + g i) ^ p) (C ^ p)

Tactic:
have hA : A = (∑' i : ι, f i ^ p) ^ (1 / p) := by rw [hf.tsum_eq, rpow_inv_rpow_self hp']

Result:
case intro
ι : Type u
f g : ι → ℝ≥0
A B : ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : HasSum (fun i => f i ^ p) (A ^ p)
hg : HasSum (fun i => g i ^ p) (B ^ p)
hp' : p ≠ 0
H₁ : Summable fun i => (f i + g i) ^ p
H₂ : (∑' (i : ι), (f i + g i) ^ p) ^ (1 / p) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)
hA : A = (∑' (i : ι), f i ^ p) ^ (1 / p)
⊢ ∃ C ≤ A + B, HasSum (fun i => (f i + g i) ^ p) (C ^ p)

Proof state:
case intro.refine_2
ι : Type u
f g : ι → ℝ≥0
A B : ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : HasSum (fun i => f i ^ p) (A ^ p)
hg : HasSum (fun i => g i ^ p) (B ^ p)
hp' : p ≠ 0
H₁ : Summable fun i => (f i + g i) ^ p
H₂ : (∑' (i : ι), (f i + g i) ^ p) ^ (1 / p) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)
hA : A = (∑' (i : ι), f i ^ p) ^ (1 / p)
hB : B = (∑' (i : ι), g i ^ p) ^ (1 / p)
⊢ HasSum (fun i => (f i + g i) ^ p) (((∑' (i : ι), (f i + g i) ^ p) ^ (1 / p)) ^ p)

Tactic:
simpa only [rpow_self_rpow_inv hp'] using H₁.hasSum

Result:
no goals

Proof state:
ι : Type u
f g : ι → ℝ≥0
A B : ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : HasSum (fun i => f i ^ p) (A ^ p)
hg : HasSum (fun i => g i ^ p) (B ^ p)
hp' : p ≠ 0
H₁ : Summable fun i => (f i + g i) ^ p
H₂ : (∑' (i : ι), (f i + g i) ^ p) ^ (1 / p) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)
hA : A = (∑' (i : ι), f i ^ p) ^ (1 / p)
⊢ B = (∑' (i : ι), g i ^ p) ^ (1 / p)

Tactic:
rw [hg.tsum_eq, rpow_inv_rpow_self hp']

Result:
no goals

Proof state:
case intro.refine_1
ι : Type u
f g : ι → ℝ≥0
A B : ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : HasSum (fun i => f i ^ p) (A ^ p)
hg : HasSum (fun i => g i ^ p) (B ^ p)
hp' : p ≠ 0
H₁ : Summable fun i => (f i + g i) ^ p
H₂ : (∑' (i : ι), (f i + g i) ^ p) ^ (1 / p) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)
hA : A = (∑' (i : ι), f i ^ p) ^ (1 / p)
hB : B = (∑' (i : ι), g i ^ p) ^ (1 / p)
⊢ (∑' (i : ι), (f i + g i) ^ p) ^ (1 / p) ≤ A + B

Tactic:
simpa [hA, hB] using H₂

Result:
no goals

Proof state:
ι : Type u
f g : ι → ℝ≥0
A B : ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : HasSum (fun i => f i ^ p) (A ^ p)
hg : HasSum (fun i => g i ^ p) (B ^ p)
hp' : p ≠ 0
H₁ : Summable fun i => (f i + g i) ^ p
H₂ : (∑' (i : ι), (f i + g i) ^ p) ^ (1 / p) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)
⊢ A = (∑' (i : ι), f i ^ p) ^ (1 / p)

Tactic:
rw [hf.tsum_eq, rpow_inv_rpow_self hp']

Result:
no goals

Proof state:
case intro
ι : Type u
f g : ι → ℝ≥0
A B : ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : HasSum (fun i => f i ^ p) (A ^ p)
hg : HasSum (fun i => g i ^ p) (B ^ p)
hp' : p ≠ 0
H₁ : Summable fun i => (f i + g i) ^ p
H₂ : (∑' (i : ι), (f i + g i) ^ p) ^ (1 / p) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)
hA : A = (∑' (i : ι), f i ^ p) ^ (1 / p)
⊢ ∃ C ≤ A + B, HasSum (fun i => (f i + g i) ^ p) (C ^ p)

Tactic:
have hB : B = (∑' i : ι, g i ^ p) ^ (1 / p) := by rw [hg.tsum_eq, rpow_inv_rpow_self hp']

Result:
case intro
ι : Type u
f g : ι → ℝ≥0
A B : ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : HasSum (fun i => f i ^ p) (A ^ p)
hg : HasSum (fun i => g i ^ p) (B ^ p)
hp' : p ≠ 0
H₁ : Summable fun i => (f i + g i) ^ p
H₂ : (∑' (i : ι), (f i + g i) ^ p) ^ (1 / p) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)
hA : A = (∑' (i : ι), f i ^ p) ^ (1 / p)
hB : B = (∑' (i : ι), g i ^ p) ^ (1 / p)
⊢ ∃ C ≤ A + B, HasSum (fun i => (f i + g i) ^ p) (C ^ p)

Proof state:
ι : Type u
f g : ι → ℝ≥0
A B : ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : HasSum (fun i => f i ^ p) (A ^ p)
hg : HasSum (fun i => g i ^ p) (B ^ p)
hp' : p ≠ 0
⊢ ∃ C ≤ A + B, HasSum (fun i => (f i + g i) ^ p) (C ^ p)

Tactic:
obtain ⟨H₁, H₂⟩ := Lp_add_le_tsum hp hf.summable hg.summable

Result:
case intro
ι : Type u
f g : ι → ℝ≥0
A B : ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : HasSum (fun i => f i ^ p) (A ^ p)
hg : HasSum (fun i => g i ^ p) (B ^ p)
hp' : p ≠ 0
H₁ : Summable fun i => (f i + g i) ^ p
H₂ : (∑' (i : ι), (f i + g i) ^ p) ^ (1 / p) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)
⊢ ∃ C ≤ A + B, HasSum (fun i => (f i + g i) ^ p) (C ^ p)

Proof state:
case intro
ι : Type u
f g : ι → ℝ≥0
A B : ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : HasSum (fun i => f i ^ p) (A ^ p)
hg : HasSum (fun i => g i ^ p) (B ^ p)
hp' : p ≠ 0
H₁ : Summable fun i => (f i + g i) ^ p
H₂ : (∑' (i : ι), (f i + g i) ^ p) ^ (1 / p) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)
hA : A = (∑' (i : ι), f i ^ p) ^ (1 / p)
hB : B = (∑' (i : ι), g i ^ p) ^ (1 / p)
⊢ ∃ C ≤ A + B, HasSum (fun i => (f i + g i) ^ p) (C ^ p)

Tactic:
refine ⟨(∑' i, (f i + g i) ^ p) ^ (1 / p), ?_, ?_⟩

Result:
case intro.refine_1
ι : Type u
f g : ι → ℝ≥0
A B : ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : HasSum (fun i => f i ^ p) (A ^ p)
hg : HasSum (fun i => g i ^ p) (B ^ p)
hp' : p ≠ 0
H₁ : Summable fun i => (f i + g i) ^ p
H₂ : (∑' (i : ι), (f i + g i) ^ p) ^ (1 / p) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)
hA : A = (∑' (i : ι), f i ^ p) ^ (1 / p)
hB : B = (∑' (i : ι), g i ^ p) ^ (1 / p)
⊢ (∑' (i : ι), (f i + g i) ^ p) ^ (1 / p) ≤ A + B

case intro.refine_2
ι : Type u
f g : ι → ℝ≥0
A B : ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : HasSum (fun i => f i ^ p) (A ^ p)
hg : HasSum (fun i => g i ^ p) (B ^ p)
hp' : p ≠ 0
H₁ : Summable fun i => (f i + g i) ^ p
H₂ : (∑' (i : ι), (f i + g i) ^ p) ^ (1 / p) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)
hA : A = (∑' (i : ι), f i ^ p) ^ (1 / p)
hB : B = (∑' (i : ι), g i ^ p) ^ (1 / p)
⊢ HasSum (fun i => (f i + g i) ^ p) (((∑' (i : ι), (f i + g i) ^ p) ^ (1 / p)) ^ p)