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