apply Finset.sum_congr rfl
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hx : 0 < x
l1 : ∀ n ∉ Finset.Ico ⌈a * x⌉₊ ⌈b * x⌉₊, f n * (Ico a b).indicator 1 (↑n / x) = 0
⊢ ∑ b_1 ∈ Finset.Ico ⌈a * x⌉₊ ⌈b * x⌉₊, f b_1 * (Ico a b).indicator 1 (↑b_1 / x) =
    ∑ n ∈ Finset.Ico ⌈a * x⌉₊ ⌈b * x⌉₊, f n
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f✝ : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
f : ℕ → ℝ
hx : 0 < x
l1 : ∀ n ∉ Finset.Ico ⌈a * x⌉₊ ⌈b * x⌉₊, f n * (Ico a b).indicator 1 (↑n / x) = 0
⊢ ∀ x_1 ∈ Finset.Ico ⌈a * x⌉₊ ⌈b * x⌉₊, f x_1 * (Ico a b).indicator 1 (↑x_1 / x) = f x_1