rw [←Aux.sum_intro]
s : SelbergSieve
d : ℕ
hdP : d ∣ P
l : ℕ
a✝ : l ∈ P.divisors
⊢ (if ↑l ^ 2 ≤ y then g l else 0) = ∑ x ∈ P.divisors, if x = d.gcd l then if ↑l ^ 2 ≤ y then g l else 0 else 0
case hd
s : SelbergSieve
d : ℕ
hdP : d ∣ P
l : ℕ
a✝ : l ∈ P.divisors
⊢ d.gcd l ∈ P.divisors