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

State before:
s : Sieve
μPlus : UpperBoundSieve
⊢ s.siftedSum ≤ X * s.mainSum μPlus.μPlus + s.errSum μPlus.μPlus
Tactic:
dsimp only [mainSum, errSum]
State after:
s : Sieve
μPlus : UpperBoundSieve
⊢ s.siftedSum ≤ X * ∑ d ∈ P.divisors, μPlus.μPlus d * ν d + ∑ d ∈ P.divisors, |μPlus.μPlus d| * |s.rem d|

State before:
s : Sieve
μPlus : UpperBoundSieve
⊢ s.siftedSum ≤ X * ∑ d ∈ P.divisors, μPlus.μPlus d * ν d + ∑ d ∈ P.divisors, |μPlus.μPlus d| * |s.rem d|
Tactic:
trans (∑ d in divisors P, μPlus d * s.multSum d)
State after:
s : Sieve
μPlus : UpperBoundSieve
⊢ s.siftedSum ≤ ∑ d ∈ P.divisors, μPlus.μPlus d * s.multSum d

s : Sieve
μPlus : UpperBoundSieve
⊢ ∑ d ∈ P.divisors, μPlus.μPlus d * s.multSum d ≤
    X * ∑ d ∈ P.divisors, μPlus.μPlus d * ν d + ∑ d ∈ P.divisors, |μPlus.μPlus d| * |s.rem d|

State before:
s : Sieve
μPlus : UpperBoundSieve
⊢ ∑ d ∈ P.divisors, μPlus.μPlus d * s.multSum d ≤
    X * ∑ d ∈ P.divisors, μPlus.μPlus d * ν d + ∑ d ∈ P.divisors, |μPlus.μPlus d| * |s.rem d|
Tactic:
trans ( X * ∑ d in divisors P, μPlus d * ν d + ∑ d in divisors P, μPlus d * R d )
State after:
s : Sieve
μPlus : UpperBoundSieve
⊢ ∑ d ∈ P.divisors, μPlus.μPlus d * s.multSum d ≤
    X * ∑ d ∈ P.divisors, μPlus.μPlus d * ν d + ∑ d ∈ P.divisors, μPlus.μPlus d * s.rem d

s : Sieve
μPlus : UpperBoundSieve
⊢ X * ∑ d ∈ P.divisors, μPlus.μPlus d * ν d + ∑ d ∈ P.divisors, μPlus.μPlus d * s.rem d ≤
    X * ∑ d ∈ P.divisors, μPlus.μPlus d * ν d + ∑ d ∈ P.divisors, |μPlus.μPlus d| * |s.rem d|

State before:
s : Sieve
μPlus : UpperBoundSieve
⊢ X * ∑ d ∈ P.divisors, μPlus.μPlus d * ν d + ∑ d ∈ P.divisors, μPlus.μPlus d * s.rem d ≤
    X * ∑ d ∈ P.divisors, μPlus.μPlus d * ν d + ∑ d ∈ P.divisors, |μPlus.μPlus d| * |s.rem d|
Tactic:
apply _root_.add_le_add (le_rfl)
State after:
s : Sieve
μPlus : UpperBoundSieve
⊢ ∑ d ∈ P.divisors, μPlus.μPlus d * s.rem d ≤ ∑ d ∈ P.divisors, |μPlus.μPlus d| * |s.rem d|

State before:
s : Sieve
μPlus : UpperBoundSieve
⊢ ∑ d ∈ P.divisors, μPlus.μPlus d * s.rem d ≤ ∑ d ∈ P.divisors, |μPlus.μPlus d| * |s.rem d|
Tactic:
apply sum_le_sum
State after:
case h
s : Sieve
μPlus : UpperBoundSieve
⊢ ∀ i ∈ P.divisors, μPlus.μPlus i * s.rem i ≤ |μPlus.μPlus i| * |s.rem i|

State before:
case h
s : Sieve
μPlus : UpperBoundSieve
⊢ ∀ i ∈ P.divisors, μPlus.μPlus i * s.rem i ≤ |μPlus.μPlus i| * |s.rem i|
Tactic:
intro d _
State after:
case h
s : Sieve
μPlus : UpperBoundSieve
d : ℕ
a✝ : d ∈ P.divisors
⊢ μPlus.μPlus d * s.rem d ≤ |μPlus.μPlus d| * |s.rem d|

State before:
case h
s : Sieve
μPlus : UpperBoundSieve
d : ℕ
a✝ : d ∈ P.divisors
⊢ μPlus.μPlus d * s.rem d ≤ |μPlus.μPlus d| * |s.rem d|
Tactic:
rw [←abs_mul]
State after:
case h
s : Sieve
μPlus : UpperBoundSieve
d : ℕ
a✝ : d ∈ P.divisors
⊢ μPlus.μPlus d * s.rem d ≤ |μPlus.μPlus d * s.rem d|

State before:
case h
s : Sieve
μPlus : UpperBoundSieve
d : ℕ
a✝ : d ∈ P.divisors
⊢ μPlus.μPlus d * s.rem d ≤ |μPlus.μPlus d * s.rem d|
Tactic:
exact le_abs_self (UpperBoundSieve.μPlus μPlus d * rem s d)
State after:
no goals

State before:
s : Sieve
μPlus : UpperBoundSieve
⊢ s.siftedSum ≤ ∑ d ∈ P.divisors, μPlus.μPlus d * s.multSum d
Tactic:
apply upper_bound_of_UpperBoundSieve
State after:
no goals

State before:
s : Sieve
μPlus : UpperBoundSieve
⊢ ∑ d ∈ P.divisors, μPlus.μPlus d * s.multSum d ≤
    X * ∑ d ∈ P.divisors, μPlus.μPlus d * ν d + ∑ d ∈ P.divisors, μPlus.μPlus d * s.rem d
Tactic:
apply le_of_eq
State after:
case a
s : Sieve
μPlus : UpperBoundSieve
⊢ ∑ d ∈ P.divisors, μPlus.μPlus d * s.multSum d =
    X * ∑ d ∈ P.divisors, μPlus.μPlus d * ν d + ∑ d ∈ P.divisors, μPlus.μPlus d * s.rem d

State before:
case a
s : Sieve
μPlus : UpperBoundSieve
⊢ ∑ d ∈ P.divisors, μPlus.μPlus d * s.multSum d =
    X * ∑ d ∈ P.divisors, μPlus.μPlus d * ν d + ∑ d ∈ P.divisors, μPlus.μPlus d * s.rem d
Tactic:
rw [mul_sum, ←sum_add_distrib]
State after:
case a
s : Sieve
μPlus : UpperBoundSieve
⊢ ∑ d ∈ P.divisors, μPlus.μPlus d * s.multSum d =
    ∑ x ∈ P.divisors, (X * (μPlus.μPlus x * ν x) + μPlus.μPlus x * s.rem x)

State before:
case a
s : Sieve
μPlus : UpperBoundSieve
⊢ ∑ d ∈ P.divisors, μPlus.μPlus d * s.multSum d =
    ∑ x ∈ P.divisors, (X * (μPlus.μPlus x * ν x) + μPlus.μPlus x * s.rem x)
Tactic:
apply sum_congr rfl
State after:
case a
s : Sieve
μPlus : UpperBoundSieve
⊢ ∀ x ∈ P.divisors, μPlus.μPlus x * s.multSum x = X * (μPlus.μPlus x * ν x) + μPlus.μPlus x * s.rem x

State before:
case a
s : Sieve
μPlus : UpperBoundSieve
⊢ ∀ x ∈ P.divisors, μPlus.μPlus x * s.multSum x = X * (μPlus.μPlus x * ν x) + μPlus.μPlus x * s.rem x
Tactic:
intro d _
State after:
case a
s : Sieve
μPlus : UpperBoundSieve
d : ℕ
a✝ : d ∈ P.divisors
⊢ μPlus.μPlus d * s.multSum d = X * (μPlus.μPlus d * ν d) + μPlus.μPlus d * s.rem d

State before:
case a
s : Sieve
μPlus : UpperBoundSieve
d : ℕ
a✝ : d ∈ P.divisors
⊢ μPlus.μPlus d * s.multSum d = X * (μPlus.μPlus d * ν d) + μPlus.μPlus d * s.rem d
Tactic:
dsimp only [rem]
State after:
case a
s : Sieve
μPlus : UpperBoundSieve
d : ℕ
a✝ : d ∈ P.divisors
⊢ μPlus.μPlus d * s.multSum d = X * (μPlus.μPlus d * ν d) + μPlus.μPlus d * (s.multSum d - ν d * X)

State before:
case a
s : Sieve
μPlus : UpperBoundSieve
d : ℕ
a✝ : d ∈ P.divisors
⊢ μPlus.μPlus d * s.multSum d = X * (μPlus.μPlus d * ν d) + μPlus.μPlus d * (s.multSum d - ν d * X)
Tactic:
ring
State after:
no goals