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

State before:
s : Sieve
μPlus : UpperBoundSieve
⊢ s.siftedSum ≤ ∑ d ∈ P.divisors, μPlus.μPlus d * s.multSum d
Tactic:
have hμ : ∀ n, δ n ≤ ∑ d in n.divisors, μPlus d := μPlus.hμPlus
State after:
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
⊢ s.siftedSum ≤ ∑ d ∈ P.divisors, μPlus.μPlus d * s.multSum d

State before:
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
⊢ s.siftedSum ≤ ∑ d ∈ P.divisors, μPlus.μPlus d * s.multSum d
Tactic:
rw [siftedSum_as_delta]
State after:
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
⊢ ∑ d ∈ A, s.weights d * δ (P.gcd d) ≤ ∑ d ∈ P.divisors, μPlus.μPlus d * s.multSum d

State before:
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
⊢ ∑ d ∈ A, s.weights d * δ (P.gcd d) ≤ ∑ d ∈ P.divisors, μPlus.μPlus d * s.multSum d
Tactic:
trans (∑ n in s.support, a n * ∑ d in (Nat.gcd P n).divisors, μPlus d)
State after:
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
⊢ ∑ d ∈ A, s.weights d * δ (P.gcd d) ≤ ∑ n ∈ A, s.weights n * ∑ d ∈ (P.gcd n).divisors, μPlus.μPlus d

s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
⊢ ∑ n ∈ A, s.weights n * ∑ d ∈ (P.gcd n).divisors, μPlus.μPlus d ≤ ∑ d ∈ P.divisors, μPlus.μPlus d * s.multSum d

State before:
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
⊢ ∑ n ∈ A, s.weights n * ∑ d ∈ (P.gcd n).divisors, μPlus.μPlus d ≤ ∑ d ∈ P.divisors, μPlus.μPlus d * s.multSum d
Tactic:
apply le_of_eq
State after:
case a
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
⊢ ∑ n ∈ A, s.weights n * ∑ d ∈ (P.gcd n).divisors, μPlus.μPlus d = ∑ d ∈ P.divisors, μPlus.μPlus d * s.multSum d

State before:
case a
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
⊢ ∑ n ∈ A, s.weights n * ∑ d ∈ (P.gcd n).divisors, μPlus.μPlus d = ∑ d ∈ P.divisors, μPlus.μPlus d * s.multSum d
Tactic:
trans (∑ n in s.support, ∑ d in divisors P, if d ∣ n then a n * μPlus d else 0)
State after:
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
⊢ ∑ n ∈ A, s.weights n * ∑ d ∈ (P.gcd n).divisors, μPlus.μPlus d =
    ∑ n ∈ A, ∑ d ∈ P.divisors, if d ∣ n then s.weights n * μPlus.μPlus d else 0

s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
⊢ (∑ n ∈ A, ∑ d ∈ P.divisors, if d ∣ n then s.weights n * μPlus.μPlus d else 0) =
    ∑ d ∈ P.divisors, μPlus.μPlus d * s.multSum d

State before:
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
⊢ (∑ n ∈ A, ∑ d ∈ P.divisors, if d ∣ n then s.weights n * μPlus.μPlus d else 0) =
    ∑ d ∈ P.divisors, μPlus.μPlus d * s.multSum d
Tactic:
rw [sum_comm, sum_congr rfl]
State after:
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
⊢ ∀ x ∈ P.divisors, (∑ x_1 ∈ A, if x ∣ x_1 then s.weights x_1 * μPlus.μPlus x else 0) = μPlus.μPlus x * s.multSum x

State before:
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
⊢ ∀ x ∈ P.divisors, (∑ x_1 ∈ A, if x ∣ x_1 then s.weights x_1 * μPlus.μPlus x else 0) = μPlus.μPlus x * s.multSum x
Tactic:
intro d _
State after:
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
d : ℕ
a✝ : d ∈ P.divisors
⊢ (∑ x ∈ A, if d ∣ x then s.weights x * μPlus.μPlus d else 0) = μPlus.μPlus d * s.multSum d

State before:
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
d : ℕ
a✝ : d ∈ P.divisors
⊢ (∑ x ∈ A, if d ∣ x then s.weights x * μPlus.μPlus d else 0) = μPlus.μPlus d * s.multSum d
Tactic:
dsimp only [multSum]
State after:
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
d : ℕ
a✝ : d ∈ P.divisors
⊢ (∑ x ∈ A, if d ∣ x then s.weights x * μPlus.μPlus d else 0) =
    μPlus.μPlus d * ∑ n ∈ A, if d ∣ n then s.weights n else 0

State before:
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
d : ℕ
a✝ : d ∈ P.divisors
⊢ (∑ x ∈ A, if d ∣ x then s.weights x * μPlus.μPlus d else 0) =
    μPlus.μPlus d * ∑ n ∈ A, if d ∣ n then s.weights n else 0
Tactic:
rw [mul_sum, sum_congr rfl]
State after:
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
d : ℕ
a✝ : d ∈ P.divisors
⊢ ∀ x ∈ A, (if d ∣ x then s.weights x * μPlus.μPlus d else 0) = μPlus.μPlus d * if d ∣ x then s.weights x else 0

State before:
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
d : ℕ
a✝ : d ∈ P.divisors
⊢ ∀ x ∈ A, (if d ∣ x then s.weights x * μPlus.μPlus d else 0) = μPlus.μPlus d * if d ∣ x then s.weights x else 0
Tactic:
intro n _
State after:
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
d : ℕ
a✝¹ : d ∈ P.divisors
n : ℕ
a✝ : n ∈ A
⊢ (if d ∣ n then s.weights n * μPlus.μPlus d else 0) = μPlus.μPlus d * if d ∣ n then s.weights n else 0

State before:
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
d : ℕ
a✝¹ : d ∈ P.divisors
n : ℕ
a✝ : n ∈ A
⊢ (if d ∣ n then s.weights n * μPlus.μPlus d else 0) = μPlus.μPlus d * if d ∣ n then s.weights n else 0
Tactic:
rw [←ite_zero_mul, mul_comm]
State after:
no goals

State before:
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
⊢ ∑ d ∈ A, s.weights d * δ (P.gcd d) ≤ ∑ n ∈ A, s.weights n * ∑ d ∈ (P.gcd n).divisors, μPlus.μPlus d
Tactic:
apply Finset.sum_le_sum
State after:
case h
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
⊢ ∀ i ∈ A, s.weights i * δ (P.gcd i) ≤ s.weights i * ∑ d ∈ (P.gcd i).divisors, μPlus.μPlus d

State before:
case h
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
⊢ ∀ i ∈ A, s.weights i * δ (P.gcd i) ≤ s.weights i * ∑ d ∈ (P.gcd i).divisors, μPlus.μPlus d
Tactic:
intro n _
State after:
case h
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
n : ℕ
a✝ : n ∈ A
⊢ s.weights n * δ (P.gcd n) ≤ s.weights n * ∑ d ∈ (P.gcd n).divisors, μPlus.μPlus d

State before:
case h
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
n : ℕ
a✝ : n ∈ A
⊢ s.weights n * δ (P.gcd n) ≤ s.weights n * ∑ d ∈ (P.gcd n).divisors, μPlus.μPlus d
Tactic:
exact mul_le_mul_of_nonneg_left (hμ (Nat.gcd P n)) (s.weights_nonneg n)
State after:
no goals

State before:
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
⊢ ∑ n ∈ A, s.weights n * ∑ d ∈ (P.gcd n).divisors, μPlus.μPlus d =
    ∑ n ∈ A, ∑ d ∈ P.divisors, if d ∣ n then s.weights n * μPlus.μPlus d else 0
Tactic:
apply sum_congr rfl
State after:
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
⊢ ∀ x ∈ A,
    s.weights x * ∑ d ∈ (P.gcd x).divisors, μPlus.μPlus d =
      ∑ d ∈ P.divisors, if d ∣ x then s.weights x * μPlus.μPlus d else 0

State before:
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
⊢ ∀ x ∈ A,
    s.weights x * ∑ d ∈ (P.gcd x).divisors, μPlus.μPlus d =
      ∑ d ∈ P.divisors, if d ∣ x then s.weights x * μPlus.μPlus d else 0
Tactic:
intro n _
State after:
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
n : ℕ
a✝ : n ∈ A
⊢ s.weights n * ∑ d ∈ (P.gcd n).divisors, μPlus.μPlus d =
    ∑ d ∈ P.divisors, if d ∣ n then s.weights n * μPlus.μPlus d else 0

State before:
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
n : ℕ
a✝ : n ∈ A
⊢ s.weights n * ∑ d ∈ (P.gcd n).divisors, μPlus.μPlus d =
    ∑ d ∈ P.divisors, if d ∣ n then s.weights n * μPlus.μPlus d else 0
Tactic:
rw [mul_sum, sum_over_dvd_ite s.prodPrimes_ne_zero (Nat.gcd_dvd_left _ _), sum_congr rfl]
State after:
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
n : ℕ
a✝ : n ∈ A
⊢ ∀ x ∈ P.divisors,
    (if x ∣ P.gcd n then s.weights n * μPlus.μPlus x else 0) = if x ∣ n then s.weights n * μPlus.μPlus x else 0

State before:
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
n : ℕ
a✝ : n ∈ A
⊢ ∀ x ∈ P.divisors,
    (if x ∣ P.gcd n then s.weights n * μPlus.μPlus x else 0) = if x ∣ n then s.weights n * μPlus.μPlus x else 0
Tactic:
intro d hd
State after:
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
n : ℕ
a✝ : n ∈ A
d : ℕ
hd : d ∈ P.divisors
⊢ (if d ∣ P.gcd n then s.weights n * μPlus.μPlus d else 0) = if d ∣ n then s.weights n * μPlus.μPlus d else 0

State before:
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
n : ℕ
a✝ : n ∈ A
d : ℕ
hd : d ∈ P.divisors
⊢ (if d ∣ P.gcd n then s.weights n * μPlus.μPlus d else 0) = if d ∣ n then s.weights n * μPlus.μPlus d else 0
Tactic:
apply if_congr _ rfl rfl
State after:
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
n : ℕ
a✝ : n ∈ A
d : ℕ
hd : d ∈ P.divisors
⊢ d ∣ P.gcd n ↔ d ∣ n

State before:
s : Sieve
μPlus : UpperBoundSieve
hμ : ∀ (n : ℕ), δ n ≤ ∑ d ∈ n.divisors, μPlus.μPlus d
n : ℕ
a✝ : n ∈ A
d : ℕ
hd : d ∈ P.divisors
⊢ d ∣ P.gcd n ↔ d ∣ n
Tactic:
rw [Nat.dvd_gcd_iff, and_iff_right (dvd_of_mem_divisors hd)]
State after:
no goals