-- Mathlib/Analysis/MeanInequalities.lean
theorem Lp_add_le_hasSum_of_nonneg (hp : 1 ≤ p) (hf : ∀ i, 0 ≤ f i) (hg : ∀ i, 0 ≤ g i) {A B : ℝ}
    (hA : 0 ≤ A) (hB : 0 ≤ B) (hfA : HasSum (fun i => f i ^ p) (A ^ p))
    (hgB : HasSum (fun i => g i ^ p) (B ^ p)) :
    ∃ C, 0 ≤ C ∧ C ≤ A + B ∧ HasSum (fun i => (f i + g i) ^ p) (C ^ p)

Proof state:
case h
ι : Type u
p : ℝ
hp : 1 ≤ p
f g : ι → ℝ≥0
A B : ℝ≥0
hfA : HasSum (fun a => f a ^ p) (A ^ p)
hgB : HasSum (fun a => g a ^ p) (B ^ p)
C : ℝ≥0
hC₁ : C ≤ A + B
hC₂ : HasSum (fun i => (f i + g i) ^ p) (C ^ p)
⊢ 0 ≤ C ∧ C ≤ A + B ∧ HasSum (fun a => (f a + g a) ^ p) (C ^ p)

Tactic:
exact ⟨zero_le _, hC₁, hC₂⟩

Result:
no goals

Proof state:
case intro
ι : Type u
g : ι → ℝ
p : ℝ
hp : 1 ≤ p
hg : ∀ (i : ι), 0 ≤ g i
A B : ℝ
hA : 0 ≤ A
hB : 0 ≤ B
hgB : HasSum (fun i => g i ^ p) (B ^ p)
f : ι → ℝ≥0
hfA : HasSum (fun i => (fun i => ↑(f i)) i ^ p) (A ^ p)
⊢ ∃ C, 0 ≤ C ∧ C ≤ A + B ∧ HasSum (fun i => ((fun i => ↑(f i)) i + g i) ^ p) (C ^ p)

Tactic:
lift g to ι → ℝ≥0 using hg

Result:
case intro.intro
ι : Type u
p : ℝ
hp : 1 ≤ p
A B : ℝ
hA : 0 ≤ A
hB : 0 ≤ B
f : ι → ℝ≥0
hfA : HasSum (fun i => (fun i => ↑(f i)) i ^ p) (A ^ p)
g : ι → ℝ≥0
hgB : HasSum (fun i => (fun i => ↑(g i)) i ^ p) (B ^ p)
⊢ ∃ C, 0 ≤ C ∧ C ≤ A + B ∧ HasSum (fun i => ((fun i => ↑(f i)) i + (fun i => ↑(g i)) i) ^ p) (C ^ p)

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

Tactic:
lift f to ι → ℝ≥0 using hf

Result:
case intro
ι : Type u
g : ι → ℝ
p : ℝ
hp : 1 ≤ p
hg : ∀ (i : ι), 0 ≤ g i
A B : ℝ
hA : 0 ≤ A
hB : 0 ≤ B
hgB : HasSum (fun i => g i ^ p) (B ^ p)
f : ι → ℝ≥0
hfA : HasSum (fun i => (fun i => ↑(f i)) i ^ p) (A ^ p)
⊢ ∃ C, 0 ≤ C ∧ C ≤ A + B ∧ HasSum (fun i => ((fun i => ↑(f i)) i + g i) ^ p) (C ^ p)

Proof state:
case h
ι : Type u
p : ℝ
hp : 1 ≤ p
f g : ι → ℝ≥0
A B : ℝ≥0
hfA : HasSum (fun a => f a ^ p) (A ^ p)
hgB : HasSum (fun a => g a ^ p) (B ^ p)
C : ℝ≥0
hC₁ : C ≤ A + B
hC₂ : HasSum (fun i => (f i + g i) ^ p) (C ^ p)
⊢ 0 ≤ ↑C ∧ ↑C ≤ ↑A + ↑B ∧ HasSum (fun i => (↑(f i) + ↑(g i)) ^ p) (↑C ^ p)

Tactic:
norm_cast

Result:
case h
ι : Type u
p : ℝ
hp : 1 ≤ p
f g : ι → ℝ≥0
A B : ℝ≥0
hfA : HasSum (fun a => f a ^ p) (A ^ p)
hgB : HasSum (fun a => g a ^ p) (B ^ p)
C : ℝ≥0
hC₁ : C ≤ A + B
hC₂ : HasSum (fun i => (f i + g i) ^ p) (C ^ p)
⊢ 0 ≤ C ∧ C ≤ A + B ∧ HasSum (fun a => (f a + g a) ^ p) (C ^ p)

Proof state:
case h
ι : Type u
p : ℝ
hp : 1 ≤ p
f g : ι → ℝ≥0
A B : ℝ≥0
hfA : HasSum (fun a => f a ^ p) (A ^ p)
hgB : HasSum (fun a => g a ^ p) (B ^ p)
C : ℝ≥0
hC₁ : C ≤ A + B
hC₂ : HasSum (fun i => (f i + g i) ^ p) (C ^ p)
⊢ 0 ≤ ↑C ∧ ↑C ≤ ↑A + ↑B ∧ HasSum (fun i => ((fun i => ↑(f i)) i + (fun i => ↑(g i)) i) ^ p) (↑C ^ p)

Tactic:
beta_reduce

Result:
case h
ι : Type u
p : ℝ
hp : 1 ≤ p
f g : ι → ℝ≥0
A B : ℝ≥0
hfA : HasSum (fun a => f a ^ p) (A ^ p)
hgB : HasSum (fun a => g a ^ p) (B ^ p)
C : ℝ≥0
hC₁ : C ≤ A + B
hC₂ : HasSum (fun i => (f i + g i) ^ p) (C ^ p)
⊢ 0 ≤ ↑C ∧ ↑C ≤ ↑A + ↑B ∧ HasSum (fun i => (↑(f i) + ↑(g i)) ^ p) (↑C ^ p)

Proof state:
case intro.intro.intro.intro.intro.intro
ι : Type u
p : ℝ
hp : 1 ≤ p
f g : ι → ℝ≥0
A B : ℝ≥0
hfA : HasSum (fun a => f a ^ p) (A ^ p)
hgB : HasSum (fun a => g a ^ p) (B ^ p)
C : ℝ≥0
hC₁ : C ≤ A + B
hC₂ : HasSum (fun i => (f i + g i) ^ p) (C ^ p)
⊢ ∃ C, 0 ≤ C ∧ C ≤ ↑A + ↑B ∧ HasSum (fun i => ((fun i => ↑(f i)) i + (fun i => ↑(g i)) i) ^ p) (C ^ p)

Tactic:
use C

Result:
case h
ι : Type u
p : ℝ
hp : 1 ≤ p
f g : ι → ℝ≥0
A B : ℝ≥0
hfA : HasSum (fun a => f a ^ p) (A ^ p)
hgB : HasSum (fun a => g a ^ p) (B ^ p)
C : ℝ≥0
hC₁ : C ≤ A + B
hC₂ : HasSum (fun i => (f i + g i) ^ p) (C ^ p)
⊢ 0 ≤ ↑C ∧ ↑C ≤ ↑A + ↑B ∧ HasSum (fun i => ((fun i => ↑(f i)) i + (fun i => ↑(g i)) i) ^ p) (↑C ^ p)

Proof state:
case intro.intro.intro.intro
ι : Type u
p : ℝ
hp : 1 ≤ p
f g : ι → ℝ≥0
A B : ℝ≥0
hfA : HasSum (fun a => f a ^ p) (A ^ p)
hgB : HasSum (fun a => g a ^ p) (B ^ p)
⊢ ∃ C, 0 ≤ C ∧ C ≤ ↑A + ↑B ∧ HasSum (fun i => ((fun i => ↑(f i)) i + (fun i => ↑(g i)) i) ^ p) (C ^ p)

Tactic:
obtain ⟨C, hC₁, hC₂⟩ := NNReal.Lp_add_le_hasSum hp hfA hgB

Result:
case intro.intro.intro.intro.intro.intro
ι : Type u
p : ℝ
hp : 1 ≤ p
f g : ι → ℝ≥0
A B : ℝ≥0
hfA : HasSum (fun a => f a ^ p) (A ^ p)
hgB : HasSum (fun a => g a ^ p) (B ^ p)
C : ℝ≥0
hC₁ : C ≤ A + B
hC₂ : HasSum (fun i => (f i + g i) ^ p) (C ^ p)
⊢ ∃ C, 0 ≤ C ∧ C ≤ ↑A + ↑B ∧ HasSum (fun i => ((fun i => ↑(f i)) i + (fun i => ↑(g i)) i) ^ p) (C ^ p)

Proof state:
case intro.intro.intro.intro
ι : Type u
p : ℝ
hp : 1 ≤ p
f g : ι → ℝ≥0
A : ℝ≥0
hfA : HasSum (fun i => (fun i => ↑(f i)) i ^ p) (↑A ^ p)
B : ℝ≥0
hgB : HasSum (fun i => (fun i => ↑(g i)) i ^ p) (↑B ^ p)
⊢ ∃ C, 0 ≤ C ∧ C ≤ ↑A + ↑B ∧ HasSum (fun i => ((fun i => ↑(f i)) i + (fun i => ↑(g i)) i) ^ p) (C ^ p)

Tactic:
beta_reduce at hfA hgB

Result:
case intro.intro.intro.intro
ι : Type u
p : ℝ
hp : 1 ≤ p
f g : ι → ℝ≥0
A : ℝ≥0
hfA : HasSum (fun i => ↑(f i) ^ p) (↑A ^ p)
B : ℝ≥0
hgB : HasSum (fun i => ↑(g i) ^ p) (↑B ^ p)
⊢ ∃ C, 0 ≤ C ∧ C ≤ ↑A + ↑B ∧ HasSum (fun i => ((fun i => ↑(f i)) i + (fun i => ↑(g i)) i) ^ p) (C ^ p)

Proof state:
case intro.intro.intro
ι : Type u
p : ℝ
hp : 1 ≤ p
B : ℝ
hB : 0 ≤ B
f g : ι → ℝ≥0
hgB : HasSum (fun i => (fun i => ↑(g i)) i ^ p) (B ^ p)
A : ℝ≥0
hfA : HasSum (fun i => (fun i => ↑(f i)) i ^ p) (↑A ^ p)
⊢ ∃ C, 0 ≤ C ∧ C ≤ ↑A + B ∧ HasSum (fun i => ((fun i => ↑(f i)) i + (fun i => ↑(g i)) i) ^ p) (C ^ p)

Tactic:
lift B to ℝ≥0 using hB

Result:
case intro.intro.intro.intro
ι : Type u
p : ℝ
hp : 1 ≤ p
f g : ι → ℝ≥0
A : ℝ≥0
hfA : HasSum (fun i => (fun i => ↑(f i)) i ^ p) (↑A ^ p)
B : ℝ≥0
hgB : HasSum (fun i => (fun i => ↑(g i)) i ^ p) (↑B ^ p)
⊢ ∃ C, 0 ≤ C ∧ C ≤ ↑A + ↑B ∧ HasSum (fun i => ((fun i => ↑(f i)) i + (fun i => ↑(g i)) i) ^ p) (C ^ p)

Proof state:
case intro.intro
ι : Type u
p : ℝ
hp : 1 ≤ p
A B : ℝ
hA : 0 ≤ A
hB : 0 ≤ B
f : ι → ℝ≥0
hfA : HasSum (fun i => (fun i => ↑(f i)) i ^ p) (A ^ p)
g : ι → ℝ≥0
hgB : HasSum (fun i => (fun i => ↑(g i)) i ^ p) (B ^ p)
⊢ ∃ C, 0 ≤ C ∧ C ≤ A + B ∧ HasSum (fun i => ((fun i => ↑(f i)) i + (fun i => ↑(g i)) i) ^ p) (C ^ p)

Tactic:
lift A to ℝ≥0 using hA

Result:
case intro.intro.intro
ι : Type u
p : ℝ
hp : 1 ≤ p
B : ℝ
hB : 0 ≤ B
f g : ι → ℝ≥0
hgB : HasSum (fun i => (fun i => ↑(g i)) i ^ p) (B ^ p)
A : ℝ≥0
hfA : HasSum (fun i => (fun i => ↑(f i)) i ^ p) (↑A ^ p)
⊢ ∃ C, 0 ≤ C ∧ C ≤ ↑A + B ∧ HasSum (fun i => ((fun i => ↑(f i)) i + (fun i => ↑(g i)) i) ^ p) (C ^ p)

Proof state:
case intro.intro.intro.intro
ι : Type u
p : ℝ
hp : 1 ≤ p
f g : ι → ℝ≥0
A : ℝ≥0
hfA : HasSum (fun i => ↑(f i) ^ p) (↑A ^ p)
B : ℝ≥0
hgB : HasSum (fun i => ↑(g i) ^ p) (↑B ^ p)
⊢ ∃ C, 0 ≤ C ∧ C ≤ ↑A + ↑B ∧ HasSum (fun i => ((fun i => ↑(f i)) i + (fun i => ↑(g i)) i) ^ p) (C ^ p)

Tactic:
norm_cast at hfA hgB

Result:
case intro.intro.intro.intro
ι : Type u
p : ℝ
hp : 1 ≤ p
f g : ι → ℝ≥0
A B : ℝ≥0
hfA : HasSum (fun a => f a ^ p) (A ^ p)
hgB : HasSum (fun a => g a ^ p) (B ^ p)
⊢ ∃ C, 0 ≤ C ∧ C ≤ ↑A + ↑B ∧ HasSum (fun i => ((fun i => ↑(f i)) i + (fun i => ↑(g i)) i) ^ p) (C ^ p)