awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
h : 4 ≤ x
calc : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ |θ x / (x * HPow.hPow (β := ℕ) (log x) 2)|) volume 2 x
calc₁ : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ log 4 * (1 / HPow.hPow (β := ℕ) (log x) 2)) volume 2 x
⊢ |∫ (t : ℝ) in 2..x, θ t / (t * HPow.hPow (β := ℕ) (log t) 2)| ≤
    log 4 * |∫ (t : ℝ) in 2..x, 1 / HPow.hPow (β := ℕ) (log t) 2|
have calc₂ : ∀ t ∈ Set.Icc 2 x,
  ∀ (ht : 2 ≤ t), t ≤ x → |θ t / (t * HPow.hPow (β := ℕ) (log t) 2)| ≤ log 4 * (1 / HPow.hPow (β := ℕ) (log t) 2)
Tactic: calc |∫ (t : ℝ) in 2..x, θ t / (t * log t ^ 2)|
    _ ≤ ∫ (x : ℝ) in 2..x, |θ x / (x * log x ^ 2)| :=
        intervalIntegral.abs_integral_le_integral_abs (by linarith)
    _ ≤ ∫ (x : ℝ) in 2..x, log 4 * (1 / log x ^ 2) :=
        intervalIntegral.integral_mono_on (by linarith) ?hf ?hg fun t ⟨ht, _⟩ ↦ ?hh
    _ = log 4 * |∫ (t : ℝ) in 2..x, 1 / log t ^ 2| := by
        rw [intervalIntegral.integral_const_mul, abs_of_nonneg]
        exact intervalIntegral.integral_nonneg (by linarith) fun u _ ↦ by positivity
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
h : 4 ≤ x
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ |θ x / (x * HPow.hPow (β := ℕ) (log x) 2)|) volume 2 x
have refine : IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (x : ℝ) ↦ θ x / (x * HPow.hPow (β := ℕ) (log x) 2)) (Set.uIoc 2 x)
  volume
Tactic: refine (intervalIntegrable_iff.mpr ?_).abs
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
h : 4 ≤ x
⊢ IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (x : ℝ) ↦ θ x / (x * HPow.hPow (β := ℕ) (log x) 2)) (Set.uIoc 2 x)
    volume
have rw : IntegrableOn (ε := ℝ) (mα := measurableSpace) (fun (x : ℝ) ↦ θ x / (x * HPow.hPow (β := ℕ) (log x) 2)) (Set.Icc 2 x)
  volume
Tactic: rw [Set.uIoc_of_le (by linarith), ← integrableOn_Icc_iff_integrableOn_Ioc]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
h : 4 ≤ x
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ log 4 * (1 / HPow.hPow (β := ℕ) (log x) 2)) volume 2 x
have refine_1 : LT.lt (α := ℝ) 1 2
Tactic: refine (intervalIntegrable_one_div_log_sq ?_ ?_).const_mul _
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
h : 4 ≤ x
refine_1 : LT.lt (α := ℝ) 1 2
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ log 4 * (1 / HPow.hPow (β := ℕ) (log x) 2)) volume 2 x
have refine_2 : 1 < x
Tactic: refine (intervalIntegrable_one_div_log_sq ?_ ?_).const_mul _
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
h : 4 ≤ x
⊢ LT.lt (α := ℝ) 1 2
have linarith : LE.le (α := ℝ) 2 1 → -1 + HSub.hSub (α := ℝ) 2 1 = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
h : 4 ≤ x
⊢ 1 < x
have linarith : x ≤ 1 → HMul.hMul (α := ℝ) 3 (-1) + (4 - x) + (x - 1) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
h : 4 ≤ x
linarith : x ≤ 1 → HMul.hMul (α := ℝ) 3 (-1) + (4 - x) + (x - 1) = 0
⊢ 1 < x
have linarith₁ : x ≤ 1 → GT.gt (α := ℝ) 3 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
h : 4 ≤ x
t : ℝ
h_1 : t ∈ Set.Icc 2 x
ht : 2 ≤ t
right : t ≤ x
⊢ 0 ≤ θ t / (t * HPow.hPow (β := ℕ) (log t) 2)
have positivity : 0 ≤ θ t → 0 ≤ θ t / (t * HPow.hPow (β := ℕ) (log t) 2)
Tactic: positivity [theta_nonneg t]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
h : 4 ≤ x
t : ℝ
h_1 : t ∈ Set.Icc 2 x
ht : 2 ≤ t
right : t ≤ x
⊢ 0 ≤ t
have linarith : t < 0 → HMul.hMul (α := ℝ) 2 (-1) + (2 - t) + (t - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
h : 4 ≤ x
t : ℝ
h_1 : t ∈ Set.Icc 2 x
ht : 2 ≤ t
right : t ≤ x
linarith : t < 0 → HMul.hMul (α := ℝ) 2 (-1) + (2 - t) + (t - 0) = 0
⊢ 0 ≤ t
have linarith₁ : t < 0 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
h : 4 ≤ x
t : ℝ
h_1 : t ∈ Set.Icc 2 x
ht : 2 ≤ t
right : t ≤ x
⊢ θ t / (t * HPow.hPow (β := ℕ) (log t) 2) ≤ log 4 * t / (t * HPow.hPow (β := ℕ) (log t) 2)
have h₁ : 0 ≤ t * HPow.hPow (β := ℕ) (log t) 2
Tactic: grw [theta_le_log4_mul_x (by linarith)]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
h : 4 ≤ x
t : ℝ
h_1 : t ∈ Set.Icc 2 x
ht : 2 ≤ t
right : t ≤ x
h₁ : 0 ≤ t * HPow.hPow (β := ℕ) (log t) 2
⊢ θ t / (t * HPow.hPow (β := ℕ) (log t) 2) ≤ log 4 * t / (t * HPow.hPow (β := ℕ) (log t) 2)
have grw : log 4 * t / (t * HPow.hPow (β := ℕ) (log t) 2) ≤ log 4 * t / (t * HPow.hPow (β := ℕ) (log t) 2)
Tactic: grw [theta_le_log4_mul_x (by linarith)]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
h : 4 ≤ x
t : ℝ
h_1 : t ∈ Set.Icc 2 x
ht : 2 ≤ t
right : t ≤ x
⊢ |θ t / (t * HPow.hPow (β := ℕ) (log t) 2)| ≤ log 4 * (1 / HPow.hPow (β := ℕ) (log t) 2)
have calc : θ t / (t * HPow.hPow (β := ℕ) (log t) 2) ≤ log 4 * t / (t * HPow.hPow (β := ℕ) (log t) 2)
Tactic: calc |θ t / (t * log t ^ 2)|
    _ = θ t / (t * log t ^ 2) := abs_of_nonneg (by positivity [theta_nonneg t])
    _ ≤ log 4 * t / (t * log t ^ 2) := by grw [theta_le_log4_mul_x (by linarith)]
    _ = log 4 * (1 / log t ^ 2) := by field
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
h : 4 ≤ x
t : ℝ
h_1 : t ∈ Set.Icc 2 x
ht : 2 ≤ t
right : t ≤ x
calc : θ t / (t * HPow.hPow (β := ℕ) (log t) 2) ≤ log 4 * t / (t * HPow.hPow (β := ℕ) (log t) 2)
⊢ |θ t / (t * HPow.hPow (β := ℕ) (log t) 2)| ≤ log 4 * (1 / HPow.hPow (β := ℕ) (log t) 2)
have calc₁ : log 4 * t / (t * HPow.hPow (β := ℕ) (log t) 2) = log 4 * (1 / HPow.hPow (β := ℕ) (log t) 2)
Tactic: calc |θ t / (t * log t ^ 2)|
    _ = θ t / (t * log t ^ 2) := abs_of_nonneg (by positivity [theta_nonneg t])
    _ ≤ log 4 * t / (t * log t ^ 2) := by grw [theta_le_log4_mul_x (by linarith)]
    _ = log 4 * (1 / log t ^ 2) := by field
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
h : 4 ≤ x
t : ℝ
h_1 : t ∈ Set.Icc 2 x
ht : 2 ≤ t
right : t ≤ x
⊢ |θ t / (t * HPow.hPow (β := ℕ) (log t) 2)| ≤ log 4 * (1 / HPow.hPow (β := ℕ) (log t) 2)
have case : θ t / (t * HPow.hPow (β := ℕ) (log t) 2) ≤ log 4 * t / (t * HPow.hPow (β := ℕ) (log t) 2)
Tactic: case hh =>
    calc |θ t / (t * log t ^ 2)|
    _ = θ t / (t * log t ^ 2) := abs_of_nonneg (by positivity [theta_nonneg t])
    _ ≤ log 4 * t / (t * log t ^ 2) := by grw [theta_le_log4_mul_x (by linarith)]
    _ = log 4 * (1 / log t ^ 2) := by field
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
h : 4 ≤ x
t : ℝ
h_1 : t ∈ Set.Icc 2 x
ht : 2 ≤ t
right : t ≤ x
case : θ t / (t * HPow.hPow (β := ℕ) (log t) 2) ≤ log 4 * t / (t * HPow.hPow (β := ℕ) (log t) 2)
⊢ |θ t / (t * HPow.hPow (β := ℕ) (log t) 2)| ≤ log 4 * (1 / HPow.hPow (β := ℕ) (log t) 2)
have case₁ : log 4 * t / (t * HPow.hPow (β := ℕ) (log t) 2) = log 4 * (1 / HPow.hPow (β := ℕ) (log t) 2)
Tactic: case hh =>
    calc |θ t / (t * log t ^ 2)|
    _ = θ t / (t * log t ^ 2) := abs_of_nonneg (by positivity [theta_nonneg t])
    _ ≤ log 4 * t / (t * log t ^ 2) := by grw [theta_le_log4_mul_x (by linarith)]
    _ = log 4 * (1 / log t ^ 2) := by field
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ ∫ (t : ℝ) in 2..x, θ t / (t * HPow.hPow (β := ℕ) (log t) 2))
    fun (x : ℝ) ↦ x / log x
have refine : IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ x / HPow.hPow (β := ℕ) (log x) 2) fun (x : ℝ) ↦ x / log x
Tactic: refine integral_theta_div_log_sq_isBigO.trans_isLittleO ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
⊢ IsLittleO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ x / HPow.hPow (β := ℕ) (log x) 2) fun (x : ℝ) ↦ x / log x
have refine : Tendsto (β := ℝ) (fun (x : ℝ) ↦ x / HPow.hPow (β := ℕ) (log x) 2 / (x / log x)) atTop (nhds 0)
Tactic: refine isLittleO_iff_tendsto' (by simp) |>.mpr ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
⊢ Tendsto (β := ℝ) (fun (x : ℝ) ↦ x / HPow.hPow (β := ℕ) (log x) 2 / (x / log x)) atTop (nhds 0)
have refine : EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ (log x)⁻¹) fun (x : ℝ) ↦ x / HPow.hPow (β := ℕ) (log x) 2 / (x / log x)
Tactic: refine Tendsto.congr' (f₁ := fun x ↦ (log x)⁻¹) ?_ tendsto_log_atTop.inv_tendsto_atTop
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
⊢ EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ (log x)⁻¹) fun (x : ℝ) ↦ x / HPow.hPow (β := ℕ) (log x) 2 / (x / log x)
have h : ∀ (x : ℝ), 0 < x → (log x)⁻¹ = x / HPow.hPow (β := ℕ) (log x) 2 / (x / log x)
Tactic: filter_upwards [eventually_gt_atTop 0] with x _
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
⊢ IsBigO (E := ℝ) (F := ℝ) atTop (fun (x : ℝ) ↦ (↑(π ⌊x⌋₊) : ℝ) - θ x / log x) fun (x : ℝ) ↦
    x / HPow.hPow (β := ℕ) (log x) 2
have apply : EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ ∫ (t : ℝ) in 2..x, θ t / (t * HPow.hPow (β := ℕ) (log t) 2)) fun (x : ℝ) ↦
  (↑(π ⌊x⌋₊) : ℝ) - θ x / log x
Tactic: apply integral_theta_div_log_sq_isBigO.congr' _ (by rfl)
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
⊢ EventuallyEq (β := ℝ) atTop (fun (x : ℝ) ↦ ∫ (t : ℝ) in 2..x, θ t / (t * HPow.hPow (β := ℕ) (log t) 2)) fun (x : ℝ) ↦
    (↑(π ⌊x⌋₊) : ℝ) - θ x / log x
have h : ∀ (x : ℝ) (hx : 2 ≤ x), ∫ (t : ℝ) in 2..x, θ t / (t * HPow.hPow (β := ℕ) (log t) 2) = (↑(π ⌊x⌋₊) : ℝ) - θ x / log x
Tactic: filter_upwards [eventually_ge_atTop 2] with x hx
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 2 ≤ x
⊢ ∫ (t : ℝ) in 2..x, θ t / (t * HPow.hPow (β := ℕ) (log t) 2) = (↑(π ⌊x⌋₊) : ℝ) - θ x / log x
have 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
Tactic: rw [primeCounting_eq_theta_div_log_add_integral hx]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (hypothesis)
Goal:
ε : ℝ
εpos : 0 < ε
⊢ ∀ᶠ (x : ℝ) in atTop, (↑(π ⌊x⌋₊) : ℝ) ≤ (log 4 + ε) * x / log x
have this : ∀ᶠ (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
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
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 : ℝ) in atTop, (↑(π ⌊x⌋₊) : ℝ) ≤ (log 4 + ε) * x / log x
have 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
Tactic: filter_upwards [eventually_ge_atTop 2, this] with x hx hx2
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
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‖
⊢ (↑(π ⌊x⌋₊) : ℝ) ≤ (log 4 + ε) * x / log x
have h : θ x / log x + ∫ (t : ℝ) in 2..x, θ t / (t * HPow.hPow (β := ℕ) (log t) 2) ≤ log 4 * x / log x + ε * x / log x
Tactic: rw [primeCounting_eq_theta_div_log_add_integral hx, add_mul, add_div]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (hypothesis)
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‖
⊢ θ x / log x + ∫ (t : ℝ) in 2..x, θ t / (t * HPow.hPow (β := ℕ) (log t) 2) ≤ log 4 * x / log x + ε * x / log x
have this₁ : 0 ≤ log x
Tactic: have : 0 ≤ log x := by bound
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (hypothesis)
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
⊢ θ x / log x + ∫ (t : ℝ) in 2..x, θ t / (t * HPow.hPow (β := ℕ) (log t) 2) ≤ log 4 * x / log x + ε * x / log x
have hx2₁ : 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
Cleared hypotheses: hx2, this
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
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
have linarith : x < 0 → HMul.hMul (α := ℝ) 2 (-1) + (2 - x) + (x - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
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
⊢ 0 ≤ x
have linarith₁ : x < 0 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
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
⊢ θ x / log x + ∫ (t : ℝ) in 2..x, θ t / (t * HPow.hPow (β := ℕ) (log t) 2) ≤ log 4 * x / log x + ε * x / log x
have 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))
Tactic: grw [theta_le_log4_mul_x (by linarith), ← hx2]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
n : ℕ
⊢ ((↑n : ℝ) * log 2 - log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)) / log (↑n : ℝ) ≤ (↑(π n) : ℝ)
have inl : ((↑0 : ℝ) * log 2 - log (HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1)) / log (↑0 : ℝ) ≤ (↑(π 0) : ℝ)
Tactic: rcases (show n = 0 ∨ n = 1 ∨ 1 < n by lia) with rfl | rfl | h
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
n : ℕ
inl : ((↑0 : ℝ) * log 2 - log (HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1)) / log (↑0 : ℝ) ≤ (↑(π 0) : ℝ)
⊢ ((↑n : ℝ) * log 2 - log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)) / log (↑n : ℝ) ≤ (↑(π n) : ℝ)
have inr : ((↑1 : ℝ) * log 2 - log (HAdd.hAdd (α := ℝ) (↑1 : ℝ) 1)) / log (↑1 : ℝ) ≤ (↑(π 1) : ℝ)
Tactic: rcases (show n = 0 ∨ n = 1 ∨ 1 < n by lia) with rfl | rfl | h
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
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) : ℝ)
⊢ ((↑n : ℝ) * log 2 - log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)) / log (↑n : ℝ) ≤ (↑(π n) : ℝ)
have inr₁ : ∀ (h : 1 < 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
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
n : ℕ
h : 1 < n
⊢ ((↑n : ℝ) * log 2 - log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)) / log (↑n : ℝ) ≤ (↑(π n) : ℝ)
have inr : (↑n : ℝ) * log 2 - log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) ≤ (↑(π n) : ℝ) * log (↑n : ℝ)
Tactic: grw [div_le_iff₀ (log_pos (mod_cast h)), ← psi_le_primeCounting_mul_log, psi_ge]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
n : ℕ
h : 1 < n
inr : (↑n : ℝ) * log 2 - log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) ≤ (↑(π n) : ℝ) * log (↑n : ℝ)
⊢ ((↑n : ℝ) * log 2 - log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)) / log (↑n : ℝ) ≤ (↑(π n) : ℝ)
have inr₁ : (↑n : ℝ) * log 2 - log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) ≤ ψ (↑n : ℝ)
Tactic: grw [div_le_iff₀ (log_pos (mod_cast h)), ← psi_le_primeCounting_mul_log, psi_ge]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
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 : ℝ)
⊢ ((↑n : ℝ) * log 2 - log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1)) / log (↑n : ℝ) ≤ (↑(π n) : ℝ)
have inr₂ : ψ (↑n : ℝ) ≤ ψ (↑n : ℝ)
Tactic: grw [div_le_iff₀ (log_pos (mod_cast h)), ← psi_le_primeCounting_mul_log, psi_ge]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 1 < x
⊢ ((x - 1) * log 2 - log (x + 2)) / log x ≤ (↑(π ⌊x⌋₊) : ℝ)
have grw : 0 ≤ x
Tactic: grw [div_le_iff₀ (log_pos hx), ← psi_le_primeCounting_mul_log', psi_ge']
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
⊢ θ x ≤ (↑(π ⌊x⌋₊) : ℝ) * log x
have grw : θ x ≤ ψ x
Tactic: grw [← psi_le_primeCounting_mul_log', theta_le_psi]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
grw : θ x ≤ ψ x
⊢ θ x ≤ (↑(π ⌊x⌋₊) : ℝ) * log x
have grw₁ : ψ x ≤ ψ x
Tactic: grw [← psi_le_primeCounting_mul_log', theta_le_psi]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
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))
have refine : ∀ p ∈ ⌊x⌋₊.primesLE, log √x ≤ log (↑p : ℝ) + if (↑p : ℝ) ≤ √x then log √x else 0
Tactic: refine sum_le_sum fun p _ ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 1 ≤ x
p : ℕ
h : p ∈ ⌊x⌋₊.primesLE
⊢ log √x ≤ log (↑p : ℝ) + if (↑p : ℝ) ≤ √x then log √x else 0
have pos : ∀ (h : (↑p : ℝ) ≤ √x), log √x ≤ log (↑p : ℝ) + log √x
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 1 ≤ x
p : ℕ
h : p ∈ ⌊x⌋₊.primesLE
pos : ∀ (h : (↑p : ℝ) ≤ √x), log √x ≤ log (↑p : ℝ) + log √x
⊢ log √x ≤ log (↑p : ℝ) + if (↑p : ℝ) ≤ √x then log √x else 0
have neg : ∀ (h : ¬(↑p : ℝ) ≤ √x), log √x ≤ log (↑p : ℝ) + 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (hypothesis)
Goal:
x : ℝ
hx : 1 ≤ x
p : ℕ
h_1 : p ∈ ⌊x⌋₊.primesLE
h : ¬(↑p : ℝ) ≤ √x
⊢ log √x ≤ log (↑p : ℝ) + 0
have this : log √x < log (↑p : ℝ)
Tactic: have : log √x < log p := log_lt_log (by positivity) (not_le.mp h)
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 1 ≤ x
⊢ ∑ p ∈ ⌊x⌋₊.primesLE, (log (↑p : ℝ) + if (↑p : ℝ) ≤ √x then log √x else 0) ≤ log 4 * x + √x * log √x
have grw : ∑ p ∈ ⌊x⌋₊.primesLE, (log (↑p : ℝ) + if (↑p : ℝ) ≤ √x then log √x else 0) ≤ θ x + √x * log √x
Tactic: grw [← theta_le_log4_mul_x (by positivity)]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 1 ≤ x
⊢ ∑ p ∈ ⌊x⌋₊.primesLE, (log (↑p : ℝ) + if (↑p : ℝ) ≤ √x then log √x else 0) ≤ θ x + √x * log √x
have rw : HAdd.hAdd (α := ℝ) (∑ x ∈ ⌊x⌋₊.primesLE, log (↑x : ℝ)) (∑ a ∈ ⌊x⌋₊.primesLE with (↑a : ℝ) ≤ √x, log √x) ≤
  ∑ p ∈ ⌊x⌋₊.primesLE, log (↑p : ℝ) + √x * log √x
Tactic: rw [sum_add_distrib, theta_eq_theta_coe_floor, theta_eq_sum_primesLE_log, ← sum_filter]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 1 ≤ x
⊢ HAdd.hAdd (α := ℝ) (∑ x ∈ ⌊x⌋₊.primesLE, log (↑x : ℝ)) (∑ a ∈ ⌊x⌋₊.primesLE with (↑a : ℝ) ≤ √x, log √x) ≤
    ∑ p ∈ ⌊x⌋₊.primesLE, log (↑p : ℝ) + √x * log √x
have simp : ∑ x ∈ ⌊x⌋₊.primesLE, log (↑x : ℝ) + (↑(#({a ∈ ⌊x⌋₊.primesLE | (↑a : ℝ) ≤ √x})) : ℝ) * log √x ≤
  ∑ x ∈ ⌊x⌋₊.primesLE, log (↑x : ℝ) + √x * log √x
Tactic: simp only [sum_const, nsmul_eq_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 1 ≤ x
⊢ ∑ x ∈ ⌊x⌋₊.primesLE, log (↑x : ℝ) + (↑(#({a ∈ ⌊x⌋₊.primesLE | (↑a : ℝ) ≤ √x})) : ℝ) * log √x ≤
    ∑ x ∈ ⌊x⌋₊.primesLE, log (↑x : ℝ) + √x * log √x
have bc : 0 ≤ log √x
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 1 ≤ x
bc : 0 ≤ log √x
⊢ ∑ x ∈ ⌊x⌋₊.primesLE, log (↑x : ℝ) + (↑(#({a ∈ ⌊x⌋₊.primesLE | (↑a : ℝ) ≤ √x})) : ℝ) * log √x ≤
    ∑ x ∈ ⌊x⌋₊.primesLE, log (↑x : ℝ) + √x * log √x
have bc₁ : (↑(#({a ∈ ⌊x⌋₊.primesLE | (↑a : ℝ) ≤ √x})) : ℝ) ≤ √x
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 1 ≤ x
⊢ (↑(#({a ∈ ⌊x⌋₊.primesLE | (↑a : ℝ) ≤ √x})) : ℝ) ≤ √x
have bc : LE.le (α := ℝ) (↑(#({a ∈ ⌊x⌋₊.primesLE | (↑a : ℝ) ≤ √x})) : ℝ) (↑⌊√x⌋₊ : ℝ)
Tactic: refine le_trans ?_ <| floor_le (sqrt_nonneg x)
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 1 ≤ x
⊢ LE.le (α := ℝ) (↑(#({a ∈ ⌊x⌋₊.primesLE | (↑a : ℝ) ≤ √x})) : ℝ) (↑⌊√x⌋₊ : ℝ)
have bc : #({a ∈ ⌊x⌋₊.primesLE | (↑a : ℝ) ≤ √x}) ≤ ⌊√x⌋₊
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 1 ≤ x
⊢ #({a ∈ ⌊x⌋₊.primesLE | (↑a : ℝ) ≤ √x}) ≤ ⌊√x⌋₊
have bc : #({a ∈ ⌊x⌋₊.primesLE | (↑a : ℝ) ≤ √x}) ≤ #(Icc 1 ⌊√x⌋₊)
Tactic: rw [show ⌊√x⌋₊ = #(Icc 1 ⌊√x⌋₊) by simp]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 1 ≤ x
⊢ #({a ∈ ⌊x⌋₊.primesLE | (↑a : ℝ) ≤ √x}) ≤ #(Icc 1 ⌊√x⌋₊)
have bc : ∀ (p : ℕ) (hp : p ∈ {a ∈ ⌊x⌋₊.primesLE | (↑a : ℝ) ≤ √x}), p ∈ Icc 1 ⌊√x⌋₊
Tactic: refine card_le_card fun p hp ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 1 ≤ x
p : ℕ
hp : p ∈ {a ∈ ⌊x⌋₊.primesLE | (↑a : ℝ) ≤ √x}
⊢ p ∈ Icc 1 ⌊√x⌋₊
have bc : ∀ (hp : (p ≤ ⌊x⌋₊ ∧ Nat.Prime p) ∧ (↑p : ℝ) ≤ √x), 1 ≤ p ∧ p ≤ ⌊√x⌋₊
Tactic: simp only [mem_filter, mem_Icc, mem_primesLE] at hp ⊢
Cleared hypotheses: hp
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (hypothesis)
Goal:
x : ℝ
hx : 1 < x
⊢ (↑(π ⌊x⌋₊) : ℝ) ≤ log 4 * x / log √x + √x
have this : 0 < log √x
Tactic: have : 0 < log √x := log_pos (lt_sqrt_of_sq_lt (by simp [hx]))
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 1 < x
this : 0 < log √x
⊢ (↑(π ⌊x⌋₊) : ℝ) ≤ log 4 * x / log √x + √x
have field_simp : (↑(π ⌊x⌋₊) : ℝ) * log √x ≤ log 4 * x + log √x * √x
Tactic: field_simp
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleAbs (hypothesis)
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
⊢ ∃ (t : Fin n → Fin ⌈1 / ε⌉₊), ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ → (↑|A i₁ % b - A i₀ % b| : ℝ) < |b| • ε
have hb' : LT.lt (α := ℝ) 0 (↑|b| : ℝ)
Tactic: have hb' : (0 : ℝ) < ↑(abs b) := Int.cast_pos.mpr (abs_pos.mpr hb)
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleAbs (goal)
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : LT.lt (α := ℝ) 0 (↑|b| : ℝ)
⊢ 0 < |b| • ε
have rw : 0 < HMul.hMul (α := ℝ) ((algebraMap ℤ ℝ : (a : ℤ) → ℝ) |b| : ℝ) ε
Tactic: rw [Algebra.smul_def]
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleAbs (hypothesis)
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : LT.lt (α := ℝ) 0 (↑|b| : ℝ)
⊢ ∃ (t : Fin n → Fin ⌈1 / ε⌉₊), ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ → (↑|A i₁ % b - A i₀ % b| : ℝ) < |b| • ε
have hbε : 0 < |b| • ε
Tactic: have hbε : 0 < abs b • ε := by
    rw [Algebra.smul_def]
    exact mul_pos hb' hε
-- Lean 4 proof step from Mathlib.NumberTheory.ClassNumber.AdmissibleAbs (hypothesis)
Goal:
n : ℕ
ε : ℝ
hε : 0 < ε
b : ℤ
hb : b ≠ 0
A : Fin n → ℤ
hb' : LT.lt (α := ℝ) 0 (↑|b| : ℝ)
hbε : 0 < |b| • ε
⊢ ∃ (t : Fin n → Fin ⌈1 / ε⌉₊), ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ → (↑|A i₁ % b - A i₀ % b| : ℝ) < |b| • ε
have hfloor : ∀ (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)