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