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

State before:
s : Sieve
l : ℕ
hl : l ∣ P
⊢ 0 < g l
Tactic:
rw [selbergTerms_apply]
State after:
s : Sieve
l : ℕ
hl : l ∣ P
⊢ 0 < ν l * ∏ p ∈ l.primeFactors, 1 / (1 - ν p)

State before:
s : Sieve
l : ℕ
hl : l ∣ P
⊢ 0 < ν l * ∏ p ∈ l.primeFactors, 1 / (1 - ν p)
Tactic:
apply mul_pos
State after:
case ha
s : Sieve
l : ℕ
hl : l ∣ P
⊢ 0 < ν l

case hb
s : Sieve
l : ℕ
hl : l ∣ P
⊢ 0 < ∏ p ∈ l.primeFactors, 1 / (1 - ν p)

State before:
case ha
s : Sieve
l : ℕ
hl : l ∣ P
⊢ 0 < ν l

case hb
s : Sieve
l : ℕ
hl : l ∣ P
⊢ 0 < ∏ p ∈ l.primeFactors, 1 / (1 - ν p)
Tactic:
exact s.nu_pos_of_dvd_prodPrimes hl
State after:
case hb
s : Sieve
l : ℕ
hl : l ∣ P
⊢ 0 < ∏ p ∈ l.primeFactors, 1 / (1 - ν p)

State before:
case hb
s : Sieve
l : ℕ
hl : l ∣ P
⊢ 0 < ∏ p ∈ l.primeFactors, 1 / (1 - ν p)
Tactic:
apply prod_pos
State after:
case hb.h0
s : Sieve
l : ℕ
hl : l ∣ P
⊢ ∀ i ∈ l.primeFactors, 0 < 1 / (1 - ν i)

State before:
case hb.h0
s : Sieve
l : ℕ
hl : l ∣ P
⊢ ∀ i ∈ l.primeFactors, 0 < 1 / (1 - ν i)
Tactic:
intro p hp
State after:
case hb.h0
s : Sieve
l : ℕ
hl : l ∣ P
p : ℕ
hp : p ∈ l.primeFactors
⊢ 0 < 1 / (1 - ν p)

State before:
case hb.h0
s : Sieve
l : ℕ
hl : l ∣ P
p : ℕ
hp : p ∈ l.primeFactors
⊢ 0 < 1 / (1 - ν p)
Tactic:
rw [one_div_pos]
State after:
case hb.h0
s : Sieve
l : ℕ
hl : l ∣ P
p : ℕ
hp : p ∈ l.primeFactors
⊢ 0 < 1 - ν p

State before:
case hb.h0
s : Sieve
l : ℕ
hl : l ∣ P
p : ℕ
hp : p ∈ l.primeFactors
⊢ 0 < 1 - ν p
Tactic:
have hp_prime : p.Prime := prime_of_mem_primeFactors hp
State after:
case hb.h0
s : Sieve
l : ℕ
hl : l ∣ P
p : ℕ
hp : p ∈ l.primeFactors
hp_prime : p.Prime
⊢ 0 < 1 - ν p

State before:
case hb.h0
s : Sieve
l : ℕ
hl : l ∣ P
p : ℕ
hp : p ∈ l.primeFactors
hp_prime : p.Prime
⊢ 0 < 1 - ν p
Tactic:
have hp_dvd : p ∣ P := (Nat.dvd_of_mem_primeFactors hp).trans hl
State after:
case hb.h0
s : Sieve
l : ℕ
hl : l ∣ P
p : ℕ
hp : p ∈ l.primeFactors
hp_prime : p.Prime
hp_dvd : p ∣ P
⊢ 0 < 1 - ν p

State before:
case hb.h0
s : Sieve
l : ℕ
hl : l ∣ P
p : ℕ
hp : p ∈ l.primeFactors
hp_prime : p.Prime
hp_dvd : p ∣ P
⊢ 0 < 1 - ν p
Tactic:
linarith only [s.nu_lt_one_of_prime p hp_prime hp_dvd]
State after:
no goals