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