rw [s.selbergWeights_diagonalisation l hl, ite_pow, zero_pow, mul_ite_zero]
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ 1 / g l * (∑ d ∈ P.divisors, if l ∣ d then ν d * s.selbergWeights d else 0) ^ 2 =
    if ↑l ^ 2 ≤ y then g l * S⁻¹ ^ 2 else 0
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ (if ↑l ^ 2 ≤ y then 1 / g l * (g l * ↑(μ l) * S⁻¹) ^ 2 else 0) = if ↑l ^ 2 ≤ y then g l * S⁻¹ ^ 2 else 0

s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ 2 ≠ 0