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

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

State before:
case h
s : Sieve
d : ℕ
hd : d ∈ P.divisors
⊢ 0 < ν d
Tactic:
rw [mem_divisors] at hd
State after:
case h
s : Sieve
d : ℕ
hd : d ∣ P ∧ P ≠ 0
⊢ 0 < ν d

State before:
case h
s : Sieve
d : ℕ
hd : d ∣ P ∧ P ≠ 0
⊢ 0 < ν d
Tactic:
apply s.nu_pos_of_dvd_prodPrimes hd.left
State after:
no goals