apply sum_congr rfl (fun x hx ↦ ?_)
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
⊢ ∑ d ∈ range (N + 1), (f * ↑ζ) d = ∑ x ∈ range (N + 1), ∑ x_1 ∈ range (N + 1), if x_1 ∈ x.divisors then f x_1 else 0
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N x : ℕ
hx : x ∈ range (N + 1)
⊢ (f * ↑ζ) x = ∑ x_1 ∈ range (N + 1), if x_1 ∈ x.divisors then f x_1 else 0