rw [sum_congr rfl fun y _ ↦ ?_]
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N : ℕ
⊢ ∑ d ∈ range (N + 1), ∑ _m ∈ filter (fun x => d ∈ x.divisors) (range (N + 1)), f d = ∑ d ∈ range (N + 1), (N / d) • f d
R : Type u_1
inst✝ : Semiring R
f : ArithmeticFunction R
N y : ℕ
x✝ : y ∈ range (N + 1)
⊢ ∑ _m ∈ filter (fun x => y ∈ x.divisors) (range (N + 1)), f y = (N / y) • f y