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

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz✝ : 1 ≤ z
hz : 1 < z
this : z ≤ z * (1 + z.log) ^ 3
⊢ ↑(primesBetween x (x + y)) ≤ 2 * y / z.log + 6 * z * (1 + z.log) ^ 3
Tactic:
linarith [siftedSum_le _ _ _ hx hy hz, primesBetween_le_siftedSum_add x y z hz.le]
State after:
no goals

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz✝ : 1 ≤ z
hz : 1 < z
⊢ z ≤ z * (1 + z.log) ^ 3
Tactic:
apply le_mul_of_one_le_right
State after:
case ha
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz✝ : 1 ≤ z
hz : 1 < z
⊢ 0 ≤ z

case h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz✝ : 1 ≤ z
hz : 1 < z
⊢ 1 ≤ (1 + z.log) ^ 3

State before:
case h
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz✝ : 1 ≤ z
hz : 1 < z
⊢ 1 ≤ (1 + z.log) ^ 3
Tactic:
apply one_le_pow_of_one_le _ _
State after:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz✝ : 1 ≤ z
hz : 1 < z
⊢ 1 ≤ 1 + z.log

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz✝ : 1 ≤ z
hz : 1 < z
⊢ 1 ≤ 1 + z.log
Tactic:
linarith [Real.log_nonneg (by linarith)]
State after:
no goals

State before:
case ha
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz✝ : 1 ≤ z
hz : 1 < z
⊢ 0 ≤ z
Tactic:
linarith
State after:
no goals

State before:
x y z : ℝ
hx : 0 < x
hy : 0 < y
hz✝ : 1 ≤ z
hz : 1 < z
⊢ 1 ≤ ?m.110225
Tactic:
linarith
State after:
no goals