simp only [mem_primeFactors] at hp
case hf
s : Sieve
d : ℕ
hdP : d ∣ P
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
p : ℕ
hp : p ∈ d.primeFactors
⊢ 0 < ν p
case hf
s : Sieve
d : ℕ
hdP : d ∣ P
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
p : ℕ
hp : p.Prime ∧ p ∣ d ∧ d ≠ 0
⊢ 0 < ν p