rw [← sum_filter, sum_congr (s₂ := divisors x) ?_ fun _ _ ↦ rfl, coe_mul_zeta_apply]
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
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N x : ℕ
hx : x ∈ range (N + 1)
⊢ filter (fun x_1 => x_1 ∈ x.divisors) (range (N + 1)) = x.divisors