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

State before:
s : SelbergSieve
⊢ s.siftedSum ≤ X / S + ∑ d ∈ P.divisors, if ↑d ≤ y then 3 ^ ω d * |s.rem d| else 0
Tactic:
let μPlus := s.selbergUbSieve
State after:
s : SelbergSieve
μPlus : UpperBoundSieve := s.selbergUbSieve
⊢ s.siftedSum ≤ X / S + ∑ d ∈ P.divisors, if ↑d ≤ y then 3 ^ ω d * |s.rem d| else 0

State before:
s : SelbergSieve
μPlus : UpperBoundSieve := s.selbergUbSieve
⊢ s.siftedSum ≤ X / S + ∑ d ∈ P.divisors, if ↑d ≤ y then 3 ^ ω d * |s.rem d| else 0
Tactic:
calc
  s.siftedSum ≤ X * s.mainSum μPlus + s.errSum μPlus := s.siftedSum_le_mainSum_errSum_of_UpperBoundSieve μPlus
  _ ≤ _ := ?_
State after:
s : SelbergSieve
μPlus : UpperBoundSieve := s.selbergUbSieve
⊢ X * s.mainSum μPlus.μPlus + s.errSum μPlus.μPlus ≤ X / S + ∑ d ∈ P.divisors, if ↑d ≤ y then 3 ^ ω d * |s.rem d| else 0

State before:
s : SelbergSieve
μPlus : UpperBoundSieve := s.selbergUbSieve
⊢ X * s.mainSum μPlus.μPlus + s.errSum μPlus.μPlus ≤ X / S + ∑ d ∈ P.divisors, if ↑d ≤ y then 3 ^ ω d * |s.rem d| else 0
Tactic:
gcongr
State after:
case h₁
s : SelbergSieve
μPlus : UpperBoundSieve := s.selbergUbSieve
⊢ X * s.mainSum μPlus.μPlus ≤ X / S

case h₂
s : SelbergSieve
μPlus : UpperBoundSieve := s.selbergUbSieve
⊢ s.errSum μPlus.μPlus ≤ ∑ d ∈ P.divisors, if ↑d ≤ y then 3 ^ ω d * |s.rem d| else 0

State before:
case h₁
s : SelbergSieve
μPlus : UpperBoundSieve := s.selbergUbSieve
⊢ X * s.mainSum μPlus.μPlus ≤ X / S
Tactic:
erw [s.selberg_bound_simple_mainSum, div_eq_mul_inv]
State after:
no goals

State before:
case h₂
s : SelbergSieve
μPlus : UpperBoundSieve := s.selbergUbSieve
⊢ s.errSum μPlus.μPlus ≤ ∑ d ∈ P.divisors, if ↑d ≤ y then 3 ^ ω d * |s.rem d| else 0
Tactic:
apply s.selberg_bound_simple_errSum
State after:
no goals