refine Finset.sum_le_sum (fun i _ => ?_) |>.trans (hf n)
n✝ : ℕ
A a b c d u x✝ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hf : chebyWith C f
x : ℝ
hx : 1 ≤ x
f0 : ℕ → ℂ := fun i => if i = 0 then 0 else f i
n : ℕ
⊢ cumsum (fun x => ‖f0 x‖) n ≤ C * ↑n
n✝ : ℕ
A a b c d u x✝¹ y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
C : ℝ
hf : chebyWith C f
x : ℝ
hx : 1 ≤ x
f0 : ℕ → ℂ := fun i => if i = 0 then 0 else f i
n i : ℕ
x✝ : i ∈ Finset.range n
⊢ (fun x => ‖f0 x‖) i ≤ (fun x => ‖f x‖) i