case intro
α : Type u_2
β✝ : Type ?u.339127
γ : Type ?u.339130
β : Type u_1
i : β → α
hi : Injective i
f : α → ℝ≥0
hf : Summable fun i => ↑(f i)
⊢ tsum ((fun i => ↑(f i)) ∘ i) ≤ ∑' (i : α), ↑(f i)
α : Type u_2
β✝ : Type ?u.339127
γ : Type ?u.339130
β : Type u_1
f : α → ℝ
hf : Summable f
hn : ∀ (a : α), 0 ≤ f a
i : β → α
hi : Injective i
⊢ tsum (f ∘ i) ≤ tsum f
lift f to α → ℝ≥0 using hn
case intro
α : Type u_2
β✝ : Type ?u.339127
γ : Type ?u.339130
β : Type u_1
i : β → α
hi : Injective i
f : α → ℝ≥0
hf : Summable fun i => f i
⊢ tsum ((fun i => ↑(f i)) ∘ i) ≤ ∑' (i : α), ↑(f i)
case intro
α : Type u_2
β✝ : Type ?u.339127
γ : Type ?u.339130
β : Type u_1
i : β → α
hi : Injective i
f : α → ℝ≥0
hf : Summable fun i => ↑(f i)
⊢ tsum ((fun i => ↑(f i)) ∘ i) ≤ ∑' (i : α), ↑(f i)
rw [NNReal.summable_coe] at hf