rw [mem_primeFactors_of_ne_zero hd_sq.ne_zero] at hpd
case hfg
s : Sieve
d : ℕ
hdP : d ∣ P
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
p : ℕ
hpd : p ∈ d.primeFactors
⊢ ν p < 1
case hfg
s : Sieve
d : ℕ
hdP : d ∣ P
hd_ne_one : d ≠ 1
hd_sq : Squarefree d
p : ℕ
hpd : p.Prime ∧ p ∣ d
⊢ ν p < 1