rw [←Finset.sum_filter, Nat.divisors_filter_dvd_of_dvd hP hn]
α : Type u_1
inst✝ : Ring α
P : ℕ
hP : P ≠ 0
n : ℕ
hn : n ∣ P
f : ℕ → α
⊢ ∑ d ∈ n.divisors, f d = ∑ d ∈ P.divisors, if d ∣ n then f d else 0
no goals