rw [inv_mul_cancel]
s : SelbergSieve
⊢ ((∑ l ∈ P.divisors, if ↑l ^ 2 ≤ y then g l else 0)⁻¹ * ∑ l ∈ P.divisors, if ↑l ^ 2 ≤ y then g l else 0) = 1
s : SelbergSieve
⊢ (∑ l ∈ P.divisors, if ↑l ^ 2 ≤ y then g l else 0) ≠ 0