Theorem: BrunTitchmarsh.primeSieve_rem_sum_le (PrimeNumberTheoremAnd/BrunTitchmarsh.lean)

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ (∑ d ∈ (primeInterSieve x y z hz).prodPrimes.divisors,
      if ↑d ≤ z then 3 ^ ω d * |(primeInterSieve x y z hz).rem d| else 0) ≤
    5 * z * (1 + z.log) ^ 3
Tactic:
apply rem_sum_le_of_const (primeInterSieve x y z hz) 5 ?_
State after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ ∀ d > 0, |(primeInterSieve x y z hz).rem d| ≤ 5

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
⊢ ∀ d > 0, |(primeInterSieve x y z hz).rem d| ≤ 5
Tactic:
intro d hd
State after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d > 0
⊢ |(primeInterSieve x y z hz).rem d| ≤ 5

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz : 1 ≤ z
d : ℕ
hd : d > 0
⊢ |(primeInterSieve x y z hz).rem d| ≤ 5
Tactic:
apply abs_rem_le <;> linarith
State after:
no goals