rw [Real.norm_eq_abs, abs_eq_self.mpr (l1 n)]
case intro
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
l1 : 0 ≤ cumsum fun x => ‖f x‖
C : ℝ
hC : chebyWith C f
n : ℕ
⊢ ‖cumsum (fun x => ‖f x‖) n‖ ≤ C * ‖↑n‖
case intro
n✝ : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
l1 : 0 ≤ cumsum fun x => ‖f x‖
C : ℝ
hC : chebyWith C f
n : ℕ
⊢ cumsum (fun x => ‖f x‖) n ≤ C * ‖↑n‖