rw [mem_divisors] at hl
case neg
s : SelbergSieve
d : ℕ
h_dvd : ¬d ∣ P
l : ℕ
hl : l ∈ P.divisors
⊢ (if d ∣ l ∧ ↑l ^ 2 ≤ y then g l else 0) = 0
case neg
s : SelbergSieve
d : ℕ
h_dvd : ¬d ∣ P
l : ℕ
hl : l ∣ P ∧ P ≠ 0
⊢ (if d ∣ l ∧ ↑l ^ 2 ≤ y then g l else 0) = 0