rw [(s.nu_mult).prodPrimeFactors_one_sub_of_squarefree _ hl]
s : Sieve
l : ℕ
hl : Squarefree l
hnu_nonzero : ν l ≠ 0
⊢ (ν l)⁻¹ * ∏ x ∈ l.primeFactors, (1 - ν x) = ∑ d ∈ l.divisors, ↑(μ (l / d)) * (ν d)⁻¹
s : Sieve
l : ℕ
hl : Squarefree l
hnu_nonzero : ν l ≠ 0
⊢ (ν l)⁻¹ * ∑ d ∈ l.divisors, ↑(μ d) * ν d = ∑ d ∈ l.divisors, ↑(μ (l / d)) * (ν d)⁻¹