simp_rw [sum_filter, sum_product]
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
⊢ ∑ d ∈ range (N + 1), (f * ↑ζ) d = ∑ d ∈ filter (fun d => d.2 ∈ d.1.divisors) (range (N + 1) ×ˢ range (N + 1)), f d.2
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