Theorem: Sieve.nu_ne_zero (PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/Basic.lean)

State before:
s : Sieve
d : ℕ
hd : d ∣ P
⊢ ν d ≠ 0
Tactic:
apply _root_.ne_of_gt
State after:
case h
s : Sieve
d : ℕ
hd : d ∣ P
⊢ 0 < ν d

State before:
case h
s : Sieve
d : ℕ
hd : d ∣ P
⊢ 0 < ν d
Tactic:
exact nu_pos_of_dvd_prodPrimes s hd
State after:
no goals