simp_rw [ENNReal.tsum_coe_ne_top_iff_summable_coe, ← norm_toNNReal]
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hσ : 1 < σ'
⊢ ∑' (i : ℕ), ↑‖term f (↑σ') i‖₊ ≠ ⊤
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
hf : ∀ (σ' : ℝ), 1 < σ' → Summable (nterm f σ')
hσ : 1 < σ'
⊢ Summable fun a => ↑‖term f (↑σ') a‖.toNNReal