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