simp only [← sum_filter]
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N y : ℕ
x✝ : y ∈ range (N + 1)
⊢ (∑ x ∈ range (N + 1), if (x, y).2 ∈ (x, y).1.divisors then f (x, y).2 else 0) =
    ∑ _m ∈ filter (fun x => y ∈ x.divisors) (range (N + 1)), f y
no goals