awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
refine : Tendsto (β := ℝ) (fun (x : ℝ) ↦ x / HPow.hPow (β := ℕ) (log x) 2 / (x / log x)) atTop (nhds 0)
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ x / HPow.hPow (β := ℕ) (log x) 2) fun (x : ℝ) ↦ x / log x

Tactic:
refine isLittleO_iff_tendsto' (by simp) |>.mpr ?_

Premises used: Iff.mpr, Asymptotics.isLittleO_iff_tendsto'
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ x / HPow.hPow (β := ℕ) (log x) 2 / (x / log x)) atTop (nhds 0)

Tactic:
Tendsto.congr' (f₁ := fun x ↦ (log x)⁻¹) ?_ tendsto_log_atTop.inv_tendsto_atTop

Premises used: Real.tendsto_log_atTop, Filter.Tendsto.inv_tendsto_atTop, Filter.Tendsto.congr'
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
refine :
  EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ (log x)⁻¹) fun (x : ℝ) ↦ x / HPow.hPow (β := ℕ) (log x) 2 / (x / log x)
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ x / HPow.hPow (β := ℕ) (log x) 2 / (x / log x)) atTop (nhds 0)

Tactic:
refine Tendsto.congr' (f₁ := fun x ↦ (log x)⁻¹) ?_ tendsto_log_atTop.inv_tendsto_atTop

Premises used: Real.tendsto_log_atTop, Filter.Tendsto.inv_tendsto_atTop, Filter.Tendsto.congr'
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
h : 0 < x → (log x)⁻¹ = x / HPow.hPow (β := ℕ) (log x) 2 / (x / log x)
⊢ 0 < x → (log x)⁻¹ = x / HPow.hPow (β := ℕ) (log x) 2 / (x / log x)

Tactic:
_
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
h : ∀ (x : ℝ), 0 < x → (log x)⁻¹ = x / HPow.hPow (β := ℕ) (log x) 2 / (x / log x)
⊢ EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ (log x)⁻¹) fun (x : ℝ) ↦ x / HPow.hPow (β := ℕ) (log x) 2 / (x / log x)

Tactic:
filter_upwards [eventually_gt_atTop 0] with x _

Premises used: OfNat.ofNat, Filter.eventually_gt_atTop
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
h : 0 < x
⊢ (log x)⁻¹ = x / HPow.hPow (β := ℕ) (log x) 2 / (x / log x)

Tactic:
field
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
⊢ EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ x / HPow.hPow (β := ℕ) (log x) 2) fun (x : ℝ) ↦
    x / HPow.hPow (β := ℕ) (log x) 2

Tactic:
rfl
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
apply :
  EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ ∫ (t : ℝ) in 2..x, θ t / (t * HPow.hPow (β := ℕ) (log t) 2)) fun (x : ℝ) ↦
    (↑(π ⌊x⌋₊) : ℝ) - θ x / log x
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ (↑(π ⌊x⌋₊) : ℝ) - θ x / log x) fun (x : ℝ) ↦
    x / HPow.hPow (β := ℕ) (log x) 2

Tactic:
apply integral_theta_div_log_sq_isBigO.congr' _ (by rfl)

Premises used: Asymptotics.IsBigO.congr', Chebyshev.integral_theta_div_log_sq_isBigO
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
h : ∀ (x : ℝ) (hx : 2 ≤ x), ∫ (t : ℝ) in 2..x, θ t / (t * HPow.hPow (β := ℕ) (log t) 2) = (↑(π ⌊x⌋₊) : ℝ) - θ x / log x
⊢ EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ ∫ (t : ℝ) in 2..x, θ t / (t * HPow.hPow (β := ℕ) (log t) 2)) fun (x : ℝ) ↦
    (↑(π ⌊x⌋₊) : ℝ) - θ x / log x

Tactic:
filter_upwards [eventually_ge_atTop 2] with x hx

Premises used: Filter.eventually_ge_atTop, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 2 ≤ x
h :
  ∫ (t : ℝ) in 2..x, θ t / (t * HPow.hPow (β := ℕ) (log t) 2) =
    (θ x / log x + ∫ (t : ℝ) in 2..x, θ t / (t * HPow.hPow (β := ℕ) (log t) 2)) - θ x / log x
⊢ ∫ (t : ℝ) in 2..x, θ t / (t * HPow.hPow (β := ℕ) (log t) 2) = (↑(π ⌊x⌋₊) : ℝ) - θ x / log x

Tactic:
rw [primeCounting_eq_theta_div_log_add_integral hx]

Premises used: Chebyshev.primeCounting_eq_theta_div_log_add_integral
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 2 ≤ x
⊢ ∫ (t : ℝ) in 2..x, θ t / (t * HPow.hPow (β := ℕ) (log t) 2) =
    (θ x / log x + ∫ (t : ℝ) in 2..x, θ t / (t * HPow.hPow (β := ℕ) (log t) 2)) - θ x / log x

Tactic:
simp
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
ε : ℝ
εpos : 0 < ε
⊢ ∀ᶠ (x : ℝ) in atTop,
    Norm.norm (E := ℝ) (∫ (t : ℝ) in 2..x, θ t / (t * HPow.hPow (β := ℕ) (log t) 2)) ≤ ε * ‖x / log x‖

Tactic:
have := integral_theta_div_log_sq_isLittleO.bound εpos
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
ε : ℝ
εpos : 0 < ε
this :
  ∀ᶠ (x : ℝ) in atTop,
    Norm.norm (E := ℝ) (∫ (t : ℝ) in 2..x, θ t / (t * HPow.hPow (β := ℕ) (log t) 2)) ≤ ε * ‖x / log x‖
h :
  ∀ (x : ℝ) (hx : 2 ≤ x)
    (hx2 : Norm.norm (E := ℝ) (∫ (t : ℝ) in 2..x, θ t / (t * HPow.hPow (β := ℕ) (log t) 2)) ≤ ε * ‖x / log x‖),
    (↑(π ⌊x⌋₊) : ℝ) ≤ (log 4 + ε) * x / log x
⊢ ∀ᶠ (x : ℝ) in atTop, (↑(π ⌊x⌋₊) : ℝ) ≤ (log 4 + ε) * x / log x

Tactic:
filter_upwards [eventually_ge_atTop 2, this] with x hx hx2

Premises used: Filter.eventually_ge_atTop, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
ε : ℝ
εpos : 0 < ε
this :
  ∀ᶠ (x : ℝ) in atTop,
    Norm.norm (E := ℝ) (∫ (t : ℝ) in 2..x, θ t / (t * HPow.hPow (β := ℕ) (log t) 2)) ≤ ε * ‖x / log x‖
x : ℝ
hx : 2 ≤ x
hx2 : Norm.norm (E := ℝ) (∫ (t : ℝ) in 2..x, θ t / (t * HPow.hPow (β := ℕ) (log t) 2)) ≤ ε * ‖x / log x‖
h : θ x / log x + ∫ (t : ℝ) in 2..x, θ t / (t * HPow.hPow (β := ℕ) (log t) 2) ≤ log 4 * x / log x + ε * x / log x
⊢ (↑(π ⌊x⌋₊) : ℝ) ≤ (log 4 + ε) * x / log x

Tactic:
rw [primeCounting_eq_theta_div_log_add_integral hx, add_mul, add_div]

Premises used: add_mul, Chebyshev.primeCounting_eq_theta_div_log_add_integral, add_div
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
ε : ℝ
εpos : 0 < ε
this :
  ∀ᶠ (x : ℝ) in atTop,
    Norm.norm (E := ℝ) (∫ (t : ℝ) in 2..x, θ t / (t * HPow.hPow (β := ℕ) (log t) 2)) ≤ ε * ‖x / log x‖
x : ℝ
hx : 2 ≤ x
hx2 : Norm.norm (E := ℝ) (∫ (t : ℝ) in 2..x, θ t / (t * HPow.hPow (β := ℕ) (log t) 2)) ≤ ε * ‖x / log x‖
⊢ 0 ≤ log x

Tactic:
bound
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
ε : ℝ
εpos : 0 < ε
this :
  ∀ᶠ (x : ℝ) in atTop,
    Norm.norm (E := ℝ) (∫ (t : ℝ) in 2..x, θ t / (t * HPow.hPow (β := ℕ) (log t) 2)) ≤ ε * ‖x / log x‖
x : ℝ
hx : 2 ≤ x
hx2 : Norm.norm (E := ℝ) (∫ (t : ℝ) in 2..x, θ t / (t * HPow.hPow (β := ℕ) (log t) 2)) ≤ ε * ‖x / log x‖
⊢ 0 ≤ log x

Tactic:
have : 0 ≤ log x := by bound
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
ε : ℝ
εpos : 0 < ε
this_1 :
  ∀ᶠ (x : ℝ) in atTop,
    Norm.norm (E := ℝ) (∫ (t : ℝ) in 2..x, θ t / (t * HPow.hPow (β := ℕ) (log t) 2)) ≤ ε * ‖x / log x‖
x : ℝ
hx : 2 ≤ x
hx2 : Norm.norm (E := ℝ) (∫ (t : ℝ) in 2..x, θ t / (t * HPow.hPow (β := ℕ) (log t) 2)) ≤ ε * ‖x / log x‖
this : 0 ≤ log x
⊢ 0 ≤ x / log x

Tactic:
bound
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
ε : ℝ
εpos : 0 < ε
this_1 :
  ∀ᶠ (x : ℝ) in atTop,
    Norm.norm (E := ℝ) (∫ (t : ℝ) in 2..x, θ t / (t * HPow.hPow (β := ℕ) (log t) 2)) ≤ ε * ‖x / log x‖
x : ℝ
hx : 2 ≤ x
hx2 : Norm.norm (E := ℝ) (∫ (t : ℝ) in 2..x, θ t / (t * HPow.hPow (β := ℕ) (log t) 2)) ≤ ε * ‖x / log x‖
this : 0 ≤ log x
⊢ Norm.norm (E := ℝ) (∫ (t : ℝ) in 2..x, θ t / (t * HPow.hPow (β := ℕ) (log t) 2)) ≤ ε * x / log x

Tactic:
rw [norm_of_nonneg (show 0 ≤ x / log x by bound), ← mul_div_assoc] at hx2

Premises used: mul_div_assoc, Real.norm_of_nonneg
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
ε : ℝ
εpos : 0 < ε
this_1 :
  ∀ᶠ (x : ℝ) in atTop,
    Norm.norm (E := ℝ) (∫ (t : ℝ) in 2..x, θ t / (t * HPow.hPow (β := ℕ) (log t) 2)) ≤ ε * ‖x / log x‖
x : ℝ
hx : 2 ≤ x
hx2 : Norm.norm (E := ℝ) (∫ (t : ℝ) in 2..x, θ t / (t * HPow.hPow (β := ℕ) (log t) 2)) ≤ ε * ‖x / log x‖
this : 0 ≤ log x
hx2₁ : Norm.norm (E := ℝ) (∫ (t : ℝ) in 2..x, θ t / (t * HPow.hPow (β := ℕ) (log t) 2)) ≤ ε * x / log x
⊢ 0 ≤ log x

Tactic:
rw [norm_of_nonneg (show 0 ≤ x / log x by bound), ← mul_div_assoc] at hx2

Premises used: mul_div_assoc, Real.norm_of_nonneg
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
ε : ℝ
εpos : 0 < ε
this_1 :
  ∀ᶠ (x : ℝ) in atTop,
    Norm.norm (E := ℝ) (∫ (t : ℝ) in 2..x, θ t / (t * HPow.hPow (β := ℕ) (log t) 2)) ≤ ε * ‖x / log x‖
x : ℝ
hx : 2 ≤ x
hx2 : Norm.norm (E := ℝ) (∫ (t : ℝ) in 2..x, θ t / (t * HPow.hPow (β := ℕ) (log t) 2)) ≤ ε * x / log x
this : 0 ≤ log x
linarith : x < 0 → HMul.hMul (α := ℝ) 2 (-1) + (2 - x) + (x - 0) = 0
linarith₁ : x < 0 → GT.gt (α := ℝ) 2 0
⊢ 0 ≤ x

Tactic:
linarith
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
ε : ℝ
εpos : 0 < ε
this_1 :
  ∀ᶠ (x : ℝ) in atTop,
    Norm.norm (E := ℝ) (∫ (t : ℝ) in 2..x, θ t / (t * HPow.hPow (β := ℕ) (log t) 2)) ≤ ε * ‖x / log x‖
x : ℝ
hx : 2 ≤ x
hx2 : Norm.norm (E := ℝ) (∫ (t : ℝ) in 2..x, θ t / (t * HPow.hPow (β := ℕ) (log t) 2)) ≤ ε * x / log x
this : 0 ≤ log x
h :
  log 4 * x / log x + ∫ (t : ℝ) in 2..x, θ t / (t * HPow.hPow (β := ℕ) (log t) 2) ≤
    log 4 * x / log x + Norm.norm (E := ℝ) (∫ (t : ℝ) in 2..x, θ t / (t * HPow.hPow (β := ℕ) (log t) 2))
⊢ θ x / log x + ∫ (t : ℝ) in 2..x, θ t / (t * HPow.hPow (β := ℕ) (log t) 2) ≤ log 4 * x / log x + ε * x / log x

Tactic:
grw [theta_le_log4_mul_x (by linarith), ← hx2]

Premises used: Chebyshev.theta_le_log4_mul_x
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
ε : ℝ
εpos : 0 < ε
this_1 :
  ∀ᶠ (x : ℝ) in atTop,
    Norm.norm (E := ℝ) (∫ (t : ℝ) in 2..x, θ t / (t * HPow.hPow (β := ℕ) (log t) 2)) ≤ ε * ‖x / log x‖
x : ℝ
hx : 2 ≤ x
hx2 : Norm.norm (E := ℝ) (∫ (t : ℝ) in 2..x, θ t / (t * HPow.hPow (β := ℕ) (log t) 2)) ≤ ε * x / log x
this : 0 ≤ log x
⊢ log 4 * x / log x + ∫ (t : ℝ) in 2..x, θ t / (t * HPow.hPow (β := ℕ) (log t) 2) ≤
    log 4 * x / log x + Norm.norm (E := ℝ) (∫ (t : ℝ) in 2..x, θ t / (t * HPow.hPow (β := ℕ) (log t) 2))

Tactic:
grind [le_norm_self]

Premises used: Real.le_norm_self
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n : ℕ
⊢ n = 0 ∨ n = 1 ∨ 1 < n

Tactic:
lia
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n : ℕ
inl : ((↑0 : ℝ) * log 2 - log (HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1)) / log (↑0 : ℝ) ≤ (↑(π 0) : ℝ)
inr : ((↑1 : ℝ) * log 2 - log (HAdd.hAdd (α := ℝ) (↑1 : ℝ) 1)) / log (↑1 : ℝ) ≤ (↑(π 1) : ℝ)
inr₁ : ∀ (h : 1 < n), ((↑n : ℝ) * log 2 - log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)) / log (↑n : ℝ) ≤ (↑(π n) : ℝ)
⊢ ((↑n : ℝ) * log 2 - log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)) / log (↑n : ℝ) ≤ (↑(π n) : ℝ)

Tactic:
rcases (show n = 0 ∨ n = 1 ∨ 1 < n by lia) with rfl | rfl | h

Premises used: rfl
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
⊢ ((↑0 : ℝ) * log 2 - log (HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1)) / log (↑0 : ℝ) ≤ (↑(π 0) : ℝ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
⊢ ((↑1 : ℝ) * log 2 - log (HAdd.hAdd (α := ℝ) (↑1 : ℝ) 1)) / log (↑1 : ℝ) ≤ (↑(π 1) : ℝ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n : ℕ
h : 1 < n
inr : (↑n : ℝ) * log 2 - log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) ≤ (↑(π n) : ℝ) * log (↑n : ℝ)
inr₁ : (↑n : ℝ) * log 2 - log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) ≤ ψ (↑n : ℝ)
inr₂ inr₃ : ψ (↑n : ℝ) ≤ ψ (↑n : ℝ)
⊢ ((↑n : ℝ) * log 2 - log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)) / log (↑n : ℝ) ≤ (↑(π n) : ℝ)

Tactic:
grw [div_le_iff₀ (log_pos (mod_cast h)), ← psi_le_primeCounting_mul_log, psi_ge]

Premises used: div_le_iff₀, Real.log_pos, Chebyshev.psi_le_primeCounting_mul_log, Chebyshev.psi_ge
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 1 < x
grw : 0 ≤ x
⊢ ((x - 1) * log 2 - log (x + 2)) / log x ≤ (↑(π ⌊x⌋₊) : ℝ)

Tactic:
grw [div_le_iff₀ (log_pos hx), ← psi_le_primeCounting_mul_log', psi_ge']

Premises used: div_le_iff₀, Chebyshev.psi_le_primeCounting_mul_log', Real.log_pos, Chebyshev.psi_ge'
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 1 < x
⊢ 0 ≤ x

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n : ℕ
⊢ θ (↑n : ℝ) ≤ (↑(π n) : ℝ) * log (↑n : ℝ)

Tactic:
(theta_le_psi n).trans (psi_le_primeCounting_mul_log n)

Premises used: Nat.cast, Chebyshev.psi_le_primeCounting_mul_log, LE.le.trans, Chebyshev.theta_le_psi
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
grw : θ x ≤ ψ x
grw₁ grw₂ : ψ x ≤ ψ x
⊢ θ x ≤ (↑(π ⌊x⌋₊) : ℝ) * log x

Tactic:
grw [← psi_le_primeCounting_mul_log', theta_le_psi]

Premises used: Chebyshev.psi_le_primeCounting_mul_log', Chebyshev.theta_le_psi
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 1 ≤ x
⊢ (↑(π ⌊x⌋₊) : ℝ) * log √x = ∑ p ∈ ⌊x⌋₊.primesLE, log √x

Tactic:
simp
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 1 ≤ x
⊢ LE.le (α := ℝ) (∑ p ∈ ⌊x⌋₊.primesLE, log √x)
    (∑ p ∈ ⌊x⌋₊.primesLE, (log (↑p : ℝ) + if (↑p : ℝ) ≤ √x then log √x else 0))

Tactic:
sum_le_sum fun p _ ↦ ?_

Premises used: Finset.sum_le_sum
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 1 ≤ x
refine : ∀ p ∈ ⌊x⌋₊.primesLE, log √x ≤ log (↑p : ℝ) + if (↑p : ℝ) ≤ √x then log √x else 0
⊢ LE.le (α := ℝ) (∑ p ∈ ⌊x⌋₊.primesLE, log √x)
    (∑ p ∈ ⌊x⌋₊.primesLE, (log (↑p : ℝ) + if (↑p : ℝ) ≤ √x then log √x else 0))

Tactic:
refine sum_le_sum fun p _ ↦ ?_

Premises used: Finset.sum_le_sum
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 1 ≤ x
p : ℕ
h : p ∈ ⌊x⌋₊.primesLE
pos : ∀ (h : (↑p : ℝ) ≤ √x), log √x ≤ log (↑p : ℝ) + log √x
neg : ∀ (h : ¬(↑p : ℝ) ≤ √x), log √x ≤ log (↑p : ℝ) + 0
⊢ log √x ≤ log (↑p : ℝ) + if (↑p : ℝ) ≤ √x then log √x else 0

Tactic:
split_ifs with h
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 1 ≤ x
p : ℕ
h_1 : p ∈ ⌊x⌋₊.primesLE
h : (↑p : ℝ) ≤ √x
⊢ log √x ≤ log (↑p : ℝ) + log √x

Tactic:
simp [log_natCast_nonneg]

Premises used: Real.log_natCast_nonneg
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 1 ≤ x
p : ℕ
h_1 : p ∈ ⌊x⌋₊.primesLE
h : ¬(↑p : ℝ) ≤ √x
⊢ 0 < √x

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 1 ≤ x
p : ℕ
h_1 : p ∈ ⌊x⌋₊.primesLE
h : ¬(↑p : ℝ) ≤ √x
⊢ log √x < log (↑p : ℝ)

Tactic:
have : log √x < log p := log_lt_log (by positivity) (not_le.mp h)
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 1 ≤ x
p : ℕ
h_1 : p ∈ ⌊x⌋₊.primesLE
h : ¬(↑p : ℝ) ≤ √x
this : log √x < log (↑p : ℝ)
⊢ log √x ≤ log (↑p : ℝ) + 0

Tactic:
grind
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 1 ≤ x
⊢ 0 ≤ x

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 1 ≤ x
grw : ∑ p ∈ ⌊x⌋₊.primesLE, (log (↑p : ℝ) + if (↑p : ℝ) ≤ √x then log √x else 0) ≤ θ x + √x * log √x
⊢ ∑ p ∈ ⌊x⌋₊.primesLE, (log (↑p : ℝ) + if (↑p : ℝ) ≤ √x then log √x else 0) ≤ log 4 * x + √x * log √x

Tactic:
grw [← theta_le_log4_mul_x (by positivity)]

Premises used: Chebyshev.theta_le_log4_mul_x
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 1 ≤ x
rw :
  HAdd.hAdd (α := ℝ) (∑ x ∈ ⌊x⌋₊.primesLE, log (↑x : ℝ)) (∑ a ∈ ⌊x⌋₊.primesLE with (↑a : ℝ) ≤ √x, log √x) ≤
    ∑ p ∈ ⌊x⌋₊.primesLE, log (↑p : ℝ) + √x * log √x
⊢ ∑ p ∈ ⌊x⌋₊.primesLE, (log (↑p : ℝ) + if (↑p : ℝ) ≤ √x then log √x else 0) ≤ θ x + √x * log √x

Tactic:
rw [sum_add_distrib, theta_eq_theta_coe_floor, theta_eq_sum_primesLE_log, ← sum_filter]

Premises used: Chebyshev.theta_eq_theta_coe_floor, Finset.sum_add_distrib, Chebyshev.theta_eq_sum_primesLE_log, Finset.sum_filter
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 1 ≤ x
simp :
  ∑ x ∈ ⌊x⌋₊.primesLE, log (↑x : ℝ) + (↑(#({a ∈ ⌊x⌋₊.primesLE | (↑a : ℝ) ≤ √x})) : ℝ) * log √x ≤
    ∑ x ∈ ⌊x⌋₊.primesLE, log (↑x : ℝ) + √x * log √x
⊢ HAdd.hAdd (α := ℝ) (∑ x ∈ ⌊x⌋₊.primesLE, log (↑x : ℝ)) (∑ a ∈ ⌊x⌋₊.primesLE with (↑a : ℝ) ≤ √x, log √x) ≤
    ∑ p ∈ ⌊x⌋₊.primesLE, log (↑p : ℝ) + √x * log √x

Tactic:
simp only [sum_const, nsmul_eq_mul]

Premises used: nsmul_eq_mul, Finset.sum_const
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 1 ≤ x
bc : 0 ≤ log √x
bc₁ : (↑(#({a ∈ ⌊x⌋₊.primesLE | (↑a : ℝ) ≤ √x})) : ℝ) ≤ √x
⊢ ∑ x ∈ ⌊x⌋₊.primesLE, log (↑x : ℝ) + (↑(#({a ∈ ⌊x⌋₊.primesLE | (↑a : ℝ) ≤ √x})) : ℝ) * log √x ≤
    ∑ x ∈ ⌊x⌋₊.primesLE, log (↑x : ℝ) + √x * log √x

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 1 ≤ x
⊢ 0 ≤ log √x

Tactic:
log_nonneg (one_le_sqrt.mpr hx)

Premises used: Real.one_le_sqrt, Iff.mpr, Real.log_nonneg
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 1 ≤ x
⊢ 0 ≤ log √x

Tactic:
exact log_nonneg (one_le_sqrt.mpr hx)

Premises used: Real.one_le_sqrt, Iff.mpr, Real.log_nonneg
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 1 ≤ x
⊢ (↑(#({a ∈ ⌊x⌋₊.primesLE | (↑a : ℝ) ≤ √x})) : ℝ) ≤ √x

Tactic:
le_trans ?_ <| floor_le (sqrt_nonneg x)

Premises used: Nat.floor_le, Real.sqrt_nonneg, le_trans
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 1 ≤ x
bc : LE.le (α := ℝ) (↑(#({a ∈ ⌊x⌋₊.primesLE | (↑a : ℝ) ≤ √x})) : ℝ) (↑⌊√x⌋₊ : ℝ)
⊢ (↑(#({a ∈ ⌊x⌋₊.primesLE | (↑a : ℝ) ≤ √x})) : ℝ) ≤ √x

Tactic:
refine le_trans ?_ <| floor_le (sqrt_nonneg x)

Premises used: Nat.floor_le, Real.sqrt_nonneg, le_trans
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 1 ≤ x
bc : #({a ∈ ⌊x⌋₊.primesLE | (↑a : ℝ) ≤ √x}) ≤ ⌊√x⌋₊
⊢ LE.le (α := ℝ) (↑(#({a ∈ ⌊x⌋₊.primesLE | (↑a : ℝ) ≤ √x})) : ℝ) (↑⌊√x⌋₊ : ℝ)

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 1 ≤ x
⊢ ⌊√x⌋₊ = #(Icc 1 ⌊√x⌋₊)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 1 ≤ x
bc : #({a ∈ ⌊x⌋₊.primesLE | (↑a : ℝ) ≤ √x}) ≤ #(Icc 1 ⌊√x⌋₊)
⊢ #({a ∈ ⌊x⌋₊.primesLE | (↑a : ℝ) ≤ √x}) ≤ ⌊√x⌋₊

Tactic:
rw [show ⌊√x⌋₊ = #(Icc 1 ⌊√x⌋₊) by simp]
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 1 ≤ x
⊢ #({a ∈ ⌊x⌋₊.primesLE | (↑a : ℝ) ≤ √x}) ≤ #(Icc 1 ⌊√x⌋₊)

Tactic:
card_le_card fun p hp ↦ ?_

Premises used: Finset.card_le_card
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 1 ≤ x
bc : ∀ (p : ℕ) (hp : p ∈ {a ∈ ⌊x⌋₊.primesLE | (↑a : ℝ) ≤ √x}), p ∈ Icc 1 ⌊√x⌋₊
⊢ #({a ∈ ⌊x⌋₊.primesLE | (↑a : ℝ) ≤ √x}) ≤ #(Icc 1 ⌊√x⌋₊)

Tactic:
refine card_le_card fun p hp ↦ ?_

Premises used: Finset.card_le_card
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 1 ≤ x
p : ℕ
hp : p ∈ {a ∈ ⌊x⌋₊.primesLE | (↑a : ℝ) ≤ √x}
bc : ∀ (hp : (p ≤ ⌊x⌋₊ ∧ Nat.Prime p) ∧ (↑p : ℝ) ≤ √x), 1 ≤ p ∧ p ≤ ⌊√x⌋₊
⊢ p ∈ Icc 1 ⌊√x⌋₊

Tactic:
simp only [mem_filter, mem_Icc, mem_primesLE] at hp ⊢

Premises used: Nat.mem_primesLE, Finset.mem_Icc, Finset.mem_filter
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 1 ≤ x
p : ℕ
hp : (p ≤ ⌊x⌋₊ ∧ Nat.Prime p) ∧ (↑p : ℝ) ≤ √x
⊢ 1 ≤ p ∧ p ≤ ⌊√x⌋₊

Tactic:
⟨hp.1.2.one_le, le_floor hp.2⟩

Premises used: Nat.Prime.one_le, And.right, And.left, And.intro, Nat.le_floor
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 1 ≤ x
p : ℕ
hp : (p ≤ ⌊x⌋₊ ∧ Nat.Prime p) ∧ (↑p : ℝ) ≤ √x
⊢ 1 ≤ p ∧ p ≤ ⌊√x⌋₊

Tactic:
exact ⟨hp.1.2.one_le, le_floor hp.2⟩
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 1 < x
⊢ HPow.hPow (α := ℝ) (β := ℕ) 1 2 < x

Tactic:
simp [hx]
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 1 < x
⊢ 0 < log √x

Tactic:
have : 0 < log √x := log_pos (lt_sqrt_of_sq_lt (by simp [hx]))
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 1 < x
this : 0 < log √x
field_simp : (↑(π ⌊x⌋₊) : ℝ) * log √x ≤ log 4 * x + log √x * √x
⊢ (↑(π ⌊x⌋₊) : ℝ) ≤ log 4 * x / log √x + √x

Tactic:
field_simp
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleAbs
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
⊢ LT.lt (α := ℝ) 0 (↑|b| : ℝ)

Tactic:
have hb' : (0 : ℝ) < ↑(abs b) := Int.cast_pos.mpr (abs_pos.mpr hb)
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleAbs
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : LT.lt (α := ℝ) 0 (↑|b| : ℝ)
rw : 0 < HMul.hMul (α := ℝ) ((algebraMap ℤ ℝ : (a : ℤ) → ℝ) |b| : ℝ) ε
⊢ 0 < |b| • ε

Tactic:
rw [Algebra.smul_def]

Premises used: Algebra.smul_def
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleAbs
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : LT.lt (α := ℝ) 0 (↑|b| : ℝ)
⊢ 0 < HMul.hMul (α := ℝ) ((algebraMap ℤ ℝ : (a : ℤ) → ℝ) |b| : ℝ) ε

Tactic:
mul_pos hb' hε

Premises used: mul_pos
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleAbs
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : LT.lt (α := ℝ) 0 (↑|b| : ℝ)
⊢ 0 < HMul.hMul (α := ℝ) ((algebraMap ℤ ℝ : (a : ℤ) → ℝ) |b| : ℝ) ε

Tactic:
exact mul_pos hb' hε

Premises used: mul_pos
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleAbs
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : LT.lt (α := ℝ) 0 (↑|b| : ℝ)
⊢ 0 < |b| • ε

Tactic:
have hbε : 0 < abs b • ε := by
    rw [Algebra.smul_def]
    exact mul_pos hb' hε
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleAbs
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : LT.lt (α := ℝ) 0 (↑|b| : ℝ)
hbε : 0 < |b| • ε
⊢ ∀ (i : Fin n), 0 ≤ ⌊(↑(A i % b) : ℝ) / |b| • ε⌋

Tactic:
have hfloor : ∀ i, 0 ≤ floor ((A i % b : ℤ) / abs b • ε : ℝ) :=
    fun _ ↦ floor_nonneg.mpr (div_nonneg (cast_nonneg (emod_nonneg _ hb)) hbε.le)
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleAbs
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : LT.lt (α := ℝ) 0 (↑|b| : ℝ)
hbε : 0 < |b| • ε
hfloor : ∀ (i : Fin n), 0 ≤ ⌊(↑(A i % b) : ℝ) / |b| • ε⌋
⊢ ∃ (t : Fin n → Fin ⌈1 / ε⌉₊), ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ → (↑|A i₁ % b - A i₀ % b| : ℝ) < |b| • ε

Tactic:
⟨fun i ↦ ⟨natAbs (floor ((A i % b : ℤ) / abs b • ε : ℝ)), ?_⟩, ?_⟩

Premises used: Int.cast, Int.floor, abs, Fin.mk, HDiv.hDiv, HMod.hMod, Int.natAbs, Exists.intro, HSMul.hSMul
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleAbs
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : LT.lt (α := ℝ) 0 (↑|b| : ℝ)
hbε : 0 < |b| • ε
hfloor : ∀ (i : Fin n), 0 ≤ ⌊(↑(A i % b) : ℝ) / |b| • ε⌋
refine_1 : ∀ (i : Fin n), ⌊(↑(A i % b) : ℝ) / |b| • ε⌋.natAbs < ⌈1 / ε⌉₊
refine_2 :
  ∀ (i₀ i₁ : Fin n),
    Eq (α := Fin ⌈1 / ε⌉₊) ((fun (i : Fin n) ↦ (⟨⌊(↑(A i % b) : ℝ) / |b| • ε⌋.natAbs, ⋯⟩ : Fin ⌈1 / ε⌉₊)) i₀)
        ((fun (i : Fin n) ↦ (⟨⌊(↑(A i % b) : ℝ) / |b| • ε⌋.natAbs, ⋯⟩ : Fin ⌈1 / ε⌉₊)) i₁) →
      (↑|A i₁ % b - A i₀ % b| : ℝ) < |b| • ε
⊢ ∃ (t : Fin n → Fin ⌈1 / ε⌉₊), ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ → (↑|A i₁ % b - A i₀ % b| : ℝ) < |b| • ε

Tactic:
refine ⟨fun i ↦ ⟨natAbs (floor ((A i % b : ℤ) / abs b • ε : ℝ)), ?_⟩, ?_⟩
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleAbs
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : LT.lt (α := ℝ) 0 (↑|b| : ℝ)
hbε : 0 < |b| • ε
hfloor : ∀ (i : Fin n), 0 ≤ ⌊(↑(A i % b) : ℝ) / |b| • ε⌋
i : Fin n
refine_1 : HDiv.hDiv (α := ℝ) (↑(A i % b) : ℝ) (↑|b| : ℝ) / ε < (↑(↑⌈1 / ε⌉₊ : ℤ) : ℝ)
⊢ ⌊(↑(A i % b) : ℝ) / |b| • ε⌋.natAbs < ⌈1 / ε⌉₊

Tactic:
rw [← ofNat_lt, natAbs_of_nonneg (hfloor i), floor_lt, Algebra.smul_def, eq_intCast, ← div_div]

Premises used: Int.floor_lt, Int.ofNat_lt, eq_intCast, Int.natAbs_of_nonneg, Algebra.smul_def, div_div
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleAbs
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : LT.lt (α := ℝ) 0 (↑|b| : ℝ)
hbε : 0 < |b| • ε
hfloor : ∀ (i : Fin n), 0 ≤ ⌊(↑(A i % b) : ℝ) / |b| • ε⌋
i : Fin n
apply : HDiv.hDiv (α := ℝ) (↑(A i % b) : ℝ) (↑|b| : ℝ) / ε < 1 / ε
⊢ HDiv.hDiv (α := ℝ) (↑(A i % b) : ℝ) (↑|b| : ℝ) / ε < (↑(↑⌈1 / ε⌉₊ : ℤ) : ℝ)

Tactic:
apply lt_of_lt_of_le _ (Nat.le_ceil _)

Premises used: Nat.le_ceil, lt_of_lt_of_le
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleAbs
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : LT.lt (α := ℝ) 0 (↑|b| : ℝ)
hbε : 0 < |b| • ε
hfloor : ∀ (i : Fin n), 0 ≤ ⌊(↑(A i % b) : ℝ) / |b| • ε⌋
i : Fin n
h : HDiv.hDiv (α := ℝ) (↑(A i % b) : ℝ) (↑|b| : ℝ) < 1
⊢ HDiv.hDiv (α := ℝ) (↑(A i % b) : ℝ) (↑|b| : ℝ) / ε < 1 / ε

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleAbs
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : LT.lt (α := ℝ) 0 (↑|b| : ℝ)
hbε : 0 < |b| • ε
hfloor : ∀ (i : Fin n), 0 ≤ ⌊(↑(A i % b) : ℝ) / |b| • ε⌋
i : Fin n
h : A i % b < |b|
⊢ HDiv.hDiv (α := ℝ) (↑(A i % b) : ℝ) (↑|b| : ℝ) < 1

Tactic:
rw [div_lt_one hb', cast_lt]

Premises used: Int.cast_lt, div_lt_one
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleAbs
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : LT.lt (α := ℝ) 0 (↑|b| : ℝ)
hbε : 0 < |b| • ε
hfloor : ∀ (i : Fin n), 0 ≤ ⌊(↑(A i % b) : ℝ) / |b| • ε⌋
i : Fin n
⊢ A i % b < |b|

Tactic:
Int.emod_lt_abs _ hb

Premises used: Int.emod_lt_abs
-- Module: Mathlib.NumberTheory.ClassNumber.AdmissibleAbs
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : LT.lt (α := ℝ) 0 (↑|b| : ℝ)
hbε : 0 < |b| • ε
hfloor : ∀ (i : Fin n), 0 ≤ ⌊(↑(A i % b) : ℝ) / |b| • ε⌋
i : Fin n
⊢ A i % b < |b|

Tactic:
exact Int.emod_lt_abs _ hb

Premises used: Int.emod_lt_abs