simp only [one_div, mul_inv, inv_div, inv_inv, Finset.prod_congr, Finset.prod_inv_distrib]
s : Sieve
l : ℕ
hl : Squarefree l
hnu_nonzero : ν l ≠ 0
⊢ 1 / (ν l * ∏ p ∈ l.primeFactors, 1 / (1 - ν p)) = ∑ d ∈ l.divisors, ↑(μ (l / d)) * (ν d)⁻¹
s : Sieve
l : ℕ
hl : Squarefree l
hnu_nonzero : ν l ≠ 0
⊢ (ν l)⁻¹ * ∏ x ∈ l.primeFactors, (1 - ν x) = ∑ d ∈ l.divisors, ↑(μ (l / d)) * (ν d)⁻¹