Theorem: Aux.sum_over_dvd_ite (PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/AuxResults.lean)

State before:
α : 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
Tactic:
rw [←Finset.sum_filter, Nat.divisors_filter_dvd_of_dvd hP hn]
State after:
no goals