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

State before:
s : Sieve
d : ℕ
hd : d ∣ P
⊢ 0 < ν d
Tactic:
calc
  0 < ∏ p in d.primeFactors, ν p := by
    apply prod_pos
    intro p hpd
    have hp_prime : p.Prime := prime_of_mem_primeFactors hpd
    have hp_dvd : p ∣ P := (dvd_of_mem_primeFactors hpd).trans hd
    exact s.nu_pos_of_prime p hp_prime hp_dvd
  _ = ν d := s.nu_mult.prod_factors_of_mult ν (Squarefree.squarefree_of_dvd hd s.prodPrimes_squarefree)
State after:
no goals

State before:
s : Sieve
d : ℕ
hd : d ∣ P
⊢ 0 < ∏ p ∈ d.primeFactors, ν p
Tactic:
apply prod_pos
State after:
case h0
s : Sieve
d : ℕ
hd : d ∣ P
⊢ ∀ i ∈ d.primeFactors, 0 < ν i

State before:
case h0
s : Sieve
d : ℕ
hd : d ∣ P
⊢ ∀ i ∈ d.primeFactors, 0 < ν i
Tactic:
intro p hpd
State after:
case h0
s : Sieve
d : ℕ
hd : d ∣ P
p : ℕ
hpd : p ∈ d.primeFactors
⊢ 0 < ν p

State before:
case h0
s : Sieve
d : ℕ
hd : d ∣ P
p : ℕ
hpd : p ∈ d.primeFactors
⊢ 0 < ν p
Tactic:
have hp_prime : p.Prime := prime_of_mem_primeFactors hpd
State after:
case h0
s : Sieve
d : ℕ
hd : d ∣ P
p : ℕ
hpd : p ∈ d.primeFactors
hp_prime : p.Prime
⊢ 0 < ν p

State before:
case h0
s : Sieve
d : ℕ
hd : d ∣ P
p : ℕ
hpd : p ∈ d.primeFactors
hp_prime : p.Prime
⊢ 0 < ν p
Tactic:
have hp_dvd : p ∣ P := (dvd_of_mem_primeFactors hpd).trans hd
State after:
case h0
s : Sieve
d : ℕ
hd : d ∣ P
p : ℕ
hpd : p ∈ d.primeFactors
hp_prime : p.Prime
hp_dvd : p ∣ P
⊢ 0 < ν p

State before:
case h0
s : Sieve
d : ℕ
hd : d ∣ P
p : ℕ
hpd : p ∈ d.primeFactors
hp_prime : p.Prime
hp_dvd : p ∣ P
⊢ 0 < ν p
Tactic:
exact s.nu_pos_of_prime p hp_prime hp_dvd
State after:
no goals