Theorem: SelbergSieve.selbergBoundingSum_pos (PrimeNumberTheoremAnd/Mathlib/NumberTheory/Sieve/Selberg.lean)

State before:
s : SelbergSieve
⊢ 0 < S
Tactic:
dsimp only [selbergBoundingSum]
State after:
s : SelbergSieve
⊢ 0 < ∑ l ∈ P.divisors, if ↑l ^ 2 ≤ y then g l else 0

State before:
s : SelbergSieve
⊢ 0 < ∑ l ∈ P.divisors, if ↑l ^ 2 ≤ y then g l else 0
Tactic:
rw [← sum_filter]
State after:
s : SelbergSieve
⊢ 0 < ∑ a ∈ filter (fun l => ↑l ^ 2 ≤ y) P.divisors, g a

State before:
s : SelbergSieve
⊢ 0 < ∑ a ∈ filter (fun l => ↑l ^ 2 ≤ y) P.divisors, g a
Tactic:
apply sum_pos
State after:
case h
s : SelbergSieve
⊢ ∀ i ∈ filter (fun l => ↑l ^ 2 ≤ y) P.divisors, 0 < g i

case hs
s : SelbergSieve
⊢ (filter (fun l => ↑l ^ 2 ≤ y) P.divisors).Nonempty

State before:
case h
s : SelbergSieve
⊢ ∀ i ∈ filter (fun l => ↑l ^ 2 ≤ y) P.divisors, 0 < g i
Tactic:
intro l hl
State after:
case h
s : SelbergSieve
l : ℕ
hl : l ∈ filter (fun l => ↑l ^ 2 ≤ y) P.divisors
⊢ 0 < g l

State before:
case h
s : SelbergSieve
l : ℕ
hl : l ∈ filter (fun l => ↑l ^ 2 ≤ y) P.divisors
⊢ 0 < g l
Tactic:
rw [mem_filter, mem_divisors] at hl
State after:
case h
s : SelbergSieve
l : ℕ
hl : (l ∣ P ∧ P ≠ 0) ∧ ↑l ^ 2 ≤ y
⊢ 0 < g l

State before:
case h
s : SelbergSieve
l : ℕ
hl : (l ∣ P ∧ P ≠ 0) ∧ ↑l ^ 2 ≤ y
⊢ 0 < g l
Tactic:
apply s.selbergTerms_pos _ (hl.1.1)
State after:
no goals

State before:
case hs
s : SelbergSieve
⊢ (filter (fun l => ↑l ^ 2 ≤ y) P.divisors).Nonempty
Tactic:
simp_rw [Finset.Nonempty, mem_filter]
State after:
case hs
s : SelbergSieve
⊢ ∃ x ∈ P.divisors, ↑x ^ 2 ≤ y

State before:
case hs
s : SelbergSieve
⊢ ∃ x ∈ P.divisors, ↑x ^ 2 ≤ y
Tactic:
use 1
State after:
case h
s : SelbergSieve
⊢ 1 ∈ P.divisors ∧ ↑1 ^ 2 ≤ y

State before:
case h
s : SelbergSieve
⊢ 1 ∈ P.divisors ∧ ↑1 ^ 2 ≤ y
Tactic:
constructor
State after:
case h.left
s : SelbergSieve
⊢ 1 ∈ P.divisors

case h.right
s : SelbergSieve
⊢ ↑1 ^ 2 ≤ y

State before:
case h.right
s : SelbergSieve
⊢ ↑1 ^ 2 ≤ y
Tactic:
rw [cast_one, one_pow]
State after:
case h.right
s : SelbergSieve
⊢ 1 ≤ y

State before:
case h.right
s : SelbergSieve
⊢ 1 ≤ y
Tactic:
exact s.one_le_level
State after:
no goals

State before:
case h.left
s : SelbergSieve
⊢ 1 ∈ P.divisors
Tactic:
apply one_mem_divisors.mpr s.prodPrimes_ne_zero
State after:
no goals