simp only [Complex.norm_eq_abs, abs_ofReal, abs_eq_self.mpr (hpos _), abs_div,
  abs_eq_self.mpr r2, Nat.abs_cast, ge_iff_le] at r1 ⊢
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
δ : ℝ
hδ : δ > 0
C : ℝ
hC : chebyWith C fun n => ↑(f n)
l1 : ∀ᶠ (p : ℝ × ℕ) in 𝓝[>] 0 ×ˢ atTop, C * ↑⌈p.1 * ↑p.2⌉₊ / ↑p.2 < δ
this : Ioc 0 1 ∈ 𝓝[>] 0
ε : ℝ
N : ℕ
h1 : C * ↑⌈(ε, N).1 * ↑(ε, N).2⌉₊ / ↑(ε, N).2 < δ
h2 : 0 < (ε, N).1 ∧ (ε, N).1 ≤ 1
r1 : cumsum (fun x => ‖(fun n => ↑(f n)) x‖) ⌈ε * ↑N⌉₊ ≤ C * ↑⌈ε * ↑N⌉₊
r2 : 0 ≤ cumsum f ⌈ε * ↑N⌉₊
⊢ |cumsum f ⌈ε * ↑N⌉₊ / ↑N| ≤ C * ↑⌈ε * ↑N⌉₊ / ↑N
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hpos : 0 ≤ f
δ : ℝ
hδ : δ > 0
C : ℝ
hC : chebyWith C fun n => ↑(f n)
l1 : ∀ᶠ (p : ℝ × ℕ) in 𝓝[>] 0 ×ˢ atTop, C * ↑⌈p.1 * ↑p.2⌉₊ / ↑p.2 < δ
this : Ioc 0 1 ∈ 𝓝[>] 0
ε : ℝ
N : ℕ
h1 : C * ↑⌈(ε, N).1 * ↑(ε, N).2⌉₊ / ↑(ε, N).2 < δ
h2 : 0 < (ε, N).1 ∧ (ε, N).1 ≤ 1
r2 : 0 ≤ cumsum f ⌈ε * ↑N⌉₊
r1 : cumsum (fun x => f x) ⌈ε * ↑N⌉₊ ≤ C * ↑⌈ε * ↑N⌉₊
⊢ cumsum f ⌈ε * ↑N⌉₊ / ↑N ≤ C * ↑⌈ε * ↑N⌉₊ / ↑N