dsimp only [selbergBoundingSum]
s : SelbergSieve
⊢ ∑ i ∈ P.divisors, (if ↑i ^ 2 ≤ y then g i else 0) * S⁻¹ ^ 2 = S⁻¹
s : SelbergSieve
⊢ ∑ i ∈ P.divisors, (if ↑i ^ 2 ≤ y then g i else 0) * (∑ l ∈ P.divisors, if ↑l ^ 2 ≤ y then g l else 0)⁻¹ ^ 2 =
    (∑ l ∈ P.divisors, if ↑l ^ 2 ≤ y then g l else 0)⁻¹