rw [moebius_sq_eq_one_of_squarefree $ s.squarefree_of_mem_divisors_prodPrimes hl]
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ 1 / g l * g l * g l * ↑(μ l ^ 2) * S⁻¹ ^ 2 = g l * S⁻¹ ^ 2

s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ 2 ≠ 0
s : SelbergSieve
l : ℕ
hl : l ∈ P.divisors
⊢ 1 / g l * g l * g l * ↑1 * S⁻¹ ^ 2 = g l * S⁻¹ ^ 2

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