rw [ArithmeticFunction.pmul_apply, ArithmeticFunction.prodPrimeFactors_apply h]
case neg
s : Sieve
d : ℕ
h : ¬d = 0
⊢ (ν.pmul (ArithmeticFunction.prodPrimeFactors fun p => 1 / (1 - ν p))) d = ν d * ∏ p ∈ d.primeFactors, 1 / (1 - ν p)
no goals