apply prod_lt_prod_of_nonempty
s : Sieve
d : ℕ
hdP : d ∣ P
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
⊢ ∏ p ∈ d.primeFactors, ν p < ∏ p ∈ d.primeFactors, 1
case hf
s : Sieve
d : ℕ
hdP : d ∣ P
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
⊢ ∀ i ∈ d.primeFactors, 0 < ν i

case hfg
s : Sieve
d : ℕ
hdP : d ∣ P
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
⊢ ∀ i ∈ d.primeFactors, ν i < 1

case h_ne
s : Sieve
d : ℕ
hdP : d ∣ P
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
⊢ d.primeFactors.Nonempty