case intro
α : Type u_1
f : α → ℝ
hf₀ : ∀ (n : α), 0 ≤ f n
y : ℝ≥0
hy : HasSum f ↑y
⊢ HasSum (fun x => Real.toNNReal (f x)) (Real.toNNReal ↑y)
α : Type u_1
f : α → ℝ
y : ℝ
hf₀ : ∀ (n : α), 0 ≤ f n
hy : HasSum f y
⊢ HasSum (fun x => Real.toNNReal (f x)) (Real.toNNReal y)
lift y to ℝ≥0 using hy.nonneg hf₀
case intro.intro
α : Type u_1
y : ℝ≥0
f : α → ℝ≥0
hy : HasSum (fun i => ↑(f i)) ↑y
⊢ HasSum (fun x => Real.toNNReal ((fun i => ↑(f i)) x)) (Real.toNNReal ↑y)
case intro
α : Type u_1
f : α → ℝ
hf₀ : ∀ (n : α), 0 ≤ f n
y : ℝ≥0
hy : HasSum f ↑y
⊢ HasSum (fun x => Real.toNNReal (f x)) (Real.toNNReal ↑y)
lift f to α → ℝ≥0 using hf₀
no goals
case intro.intro
α : Type u_1
y : ℝ≥0
f : α → ℝ≥0
hy : HasSum (fun i => ↑(f i)) ↑y
⊢ HasSum (fun x => Real.toNNReal ((fun i => ↑(f i)) x)) (Real.toNNReal ↑y)
simpa [hasSum_coe] using hy