have r2 : Disjoint (Finset.range ⌈ε * N⌉₊) (Finset.Ico ⌈ε * N⌉₊ N) := by
  rw [Finset.range_eq_Ico] ; apply Finset.Ico_disjoint_Ico_consecutive
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → 𝕜
ε : ℝ
N : ℕ
hε : ε ≤ 1
r1 : Finset.range N = Finset.range ⌈ε * ↑N⌉₊ ∪ Finset.Ico ⌈ε * ↑N⌉₊ N
⊢ S f 0 N - S f ε N = cumsum f ⌈ε * ↑N⌉₊ / ↑N
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → 𝕜
ε : ℝ
N : ℕ
hε : ε ≤ 1
r1 : Finset.range N = Finset.range ⌈ε * ↑N⌉₊ ∪ Finset.Ico ⌈ε * ↑N⌉₊ N
r2 : Disjoint (Finset.range ⌈ε * ↑N⌉₊) (Finset.Ico ⌈ε * ↑N⌉₊ N)
⊢ S f 0 N - S f ε N = cumsum f ⌈ε * ↑N⌉₊ / ↑N