have hd_dvd : d ∣ l := dvd_of_mem_divisors hd
case a
s : Sieve
l : ℕ
hl : Squarefree l
hnu_nonzero : ν l ≠ 0
d : ℕ
hd : d ∈ l.divisors
⊢ ↑(μ d) * (ν (l / d))⁻¹ = (ν l)⁻¹ * (↑(μ d) * ν d)
case a
s : Sieve
l : ℕ
hl : Squarefree l
hnu_nonzero : ν l ≠ 0
d : ℕ
hd : d ∈ l.divisors
hd_dvd : d ∣ l
⊢ ↑(μ d) * (ν (l / d))⁻¹ = (ν l)⁻¹ * (↑(μ d) * ν d)