awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx_1 : 1 ≤ x
hx : 2 ≤ x
⊢ (↑(⌊log x / log 2⌋₊ - 1) : ℝ) * (log 4 * √x) ≤ log x / log 2 * (log 4 * √x)
have hbc : (↑(⌊log x / log 2⌋₊ - 1) : ℝ) ≤ log x / log 2
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx_1 : 1 ≤ x
hx : 2 ≤ x
⊢ (↑(⌊log x / log 2⌋₊ - 1) : ℝ) ≤ log x / log 2
have hbc : HSub.hSub (α := ℝ) (↑⌊log x / log 2⌋₊ : ℝ) (↑1 : ℝ) ≤ log x / log 2
Tactic: rw [cast_sub]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx_1 : 1 ≤ x
hx : 2 ≤ x
hbc : HSub.hSub (α := ℝ) (↑⌊log x / log 2⌋₊ : ℝ) (↑1 : ℝ) ≤ log x / log 2
⊢ (↑(⌊log x / log 2⌋₊ - 1) : ℝ) ≤ log x / log 2
have hbc₁ : 1 ≤ ⌊log x / log 2⌋₊
Tactic: rw [cast_sub]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx_1 : 1 ≤ x
hx : 2 ≤ x
⊢ HSub.hSub (α := ℝ) (↑⌊log x / log 2⌋₊ : ℝ) (↑1 : ℝ) ≤ log x / log 2
have trans : HSub.hSub (α := ℝ) (↑⌊log x / log 2⌋₊ : ℝ) (↑1 : ℝ) ≤ (↑⌊log x / log 2⌋₊ : ℝ)
Tactic: trans ↑⌊log x / log 2⌋₊
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx_1 : 1 ≤ x
hx : 2 ≤ x
trans : HSub.hSub (α := ℝ) (↑⌊log x / log 2⌋₊ : ℝ) (↑1 : ℝ) ≤ (↑⌊log x / log 2⌋₊ : ℝ)
⊢ HSub.hSub (α := ℝ) (↑⌊log x / log 2⌋₊ : ℝ) (↑1 : ℝ) ≤ log x / log 2
have trans₁ : (↑⌊log x / log 2⌋₊ : ℝ) ≤ log x / log 2
Tactic: trans ↑⌊log x / log 2⌋₊
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx_1 : 1 ≤ x
hx : 2 ≤ x
⊢ HSub.hSub (α := ℝ) (↑⌊log x / log 2⌋₊ : ℝ) (↑1 : ℝ) ≤ (↑⌊log x / log 2⌋₊ : ℝ)
have linarith : (↑⌊log x / log 2⌋₊ : ℝ) < HSub.hSub (α := ℝ) (↑⌊log x / log 2⌋₊ : ℝ) (↑1 : ℝ) →
  -1 +
      (HMul.hMul (α := ℝ) 1 (↑⌊log x / log 2⌋₊ : ℝ) -
        (HMul.hMul (α := ℝ) 1 (↑⌊log x / log 2⌋₊ : ℝ) - HMul.hMul (α := ℝ) 1 1)) =
    0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx_1 : 1 ≤ x
hx : 2 ≤ x
⊢ 1 ≤ ⌊log x / log 2⌋₊
have hbc : (↑1 : ℝ) ≤ log x / log 2
Tactic: apply le_floor
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx_1 : 1 ≤ x
hx : 2 ≤ x
⊢ (↑1 : ℝ) ≤ log x / log 2
have hbc : 1 ≤ log x / log 2
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx_1 : 1 ≤ x
hx : 2 ≤ x
⊢ 1 ≤ log x / log 2
have hbc : log 2 ≤ log x
Tactic: apply one_le_div _ |>.mpr
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx_1 : 1 ≤ x
hx : 2 ≤ x
hbc : log 2 ≤ log x
⊢ 1 ≤ log x / log 2
have apply : 0 < log 2
Tactic: apply one_le_div _ |>.mpr
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx_1 : 1 ≤ x
hx : 2 ≤ x
⊢ log 4 / log 2 * √x * log x = 2 * √x * log x
have e_a : log 4 / log 2 = 2
Tactic: congr
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx_1 : 1 ≤ x
hx : 2 ≤ x
⊢ log 4 / log 2 = 2
have e_a : (↑2 : ℝ) * log 2 / log 2 = 2
Tactic: rw [(by norm_num : (4 : ℝ) = 2 ^ 2), Real.log_pow]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx_1 : 1 ≤ x
hx : 2 ≤ x
⊢ (↑(⌊log x / log 2⌋₊ - 1) : ℝ) * (log 4 * √x) ≤ 2 * √x * log x
have _ : (↑(⌊log x / log 2⌋₊ - 1) : ℝ) * (log 4 * √x) ≤ log x / log 2 * (log 4 * √x)
Tactic: calc
  _ ≤ (log x / log 2) * (log 4 * √x) := by
    gcongr
    rw [cast_sub]
    · trans ↑⌊log x / log 2⌋₊
      · linarith
      · exact floor_le (by bound)
    apply le_floor
    norm_cast
    apply one_le_div _ |>.mpr <;> bound
  _ = (log 4 / log 2) * x.sqrt * x.log := by field
  _ = _ := by
    congr
    rw [(by norm_num : (4 : ℝ) = 2 ^ 2), Real.log_pow]
    field
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx_1 : 1 ≤ x
hx : 2 ≤ x
_ : (↑(⌊log x / log 2⌋₊ - 1) : ℝ) * (log 4 * √x) ≤ log x / log 2 * (log 4 * √x)
⊢ (↑(⌊log x / log 2⌋₊ - 1) : ℝ) * (log 4 * √x) ≤ 2 * √x * log x
have _₁ : log x / log 2 * (log 4 * √x) = log 4 / log 2 * √x * log x
Tactic: calc
  _ ≤ (log x / log 2) * (log 4 * √x) := by
    gcongr
    rw [cast_sub]
    · trans ↑⌊log x / log 2⌋₊
      · linarith
      · exact floor_le (by bound)
    apply le_floor
    norm_cast
    apply one_le_div _ |>.mpr <;> bound
  _ = (log 4 / log 2) * x.sqrt * x.log := by field
  _ = _ := by
    congr
    rw [(by norm_num : (4 : ℝ) = 2 ^ 2), Real.log_pow]
    field
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx_1 : 1 ≤ x
hx : 2 ≤ x
_ : (↑(⌊log x / log 2⌋₊ - 1) : ℝ) * (log 4 * √x) ≤ log x / log 2 * (log 4 * √x)
_₁ : log x / log 2 * (log 4 * √x) = log 4 / log 2 * √x * log x
⊢ (↑(⌊log x / log 2⌋₊ - 1) : ℝ) * (log 4 * √x) ≤ 2 * √x * log x
have _₂ : log 4 / log 2 * √x * log x = 2 * √x * log x
Tactic: calc
  _ ≤ (log x / log 2) * (log 4 * √x) := by
    gcongr
    rw [cast_sub]
    · trans ↑⌊log x / log 2⌋₊
      · linarith
      · exact floor_le (by bound)
    apply le_floor
    norm_cast
    apply one_le_div _ |>.mpr <;> bound
  _ = (log 4 / log 2) * x.sqrt * x.log := by field
  _ = _ := by
    congr
    rw [(by norm_num : (4 : ℝ) = 2 ^ 2), Real.log_pow]
    field
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 1 ≤ x
⊢ ψ x - θ x + θ x ≤ 2 * √x * log x + log 4 * x
have h₁ : ψ x - θ x ≤ 2 * √x * log x
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 1 ≤ x
h₁ : ψ x - θ x ≤ 2 * √x * log x
⊢ ψ x - θ x + θ x ≤ 2 * √x * log x + log 4 * x
have h₂ : θ x ≤ log 4 * x
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 1 ≤ x
⊢ 0 ≤ x
have linarith : x < 0 → -1 + (1 - x) + (x - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 1 ≤ x
⊢ ψ x ≤ log 4 * x + 2 * √x * log x
have _ : ψ x = ψ x - θ x + θ x
Tactic: calc
  _ = ψ x - θ x + θ x := by ring
  _ ≤ 2 * x.sqrt * x.log + log 4 * x := by
    gcongr
    · exact le_trans (le_abs_self _) (abs_psi_sub_theta_le_sqrt_mul_log hx)
    · exact theta_le_log4_mul_x (by linarith)
  _ = _ := by ring
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 1 ≤ x
_ : ψ x = ψ x - θ x + θ x
⊢ ψ x ≤ log 4 * x + 2 * √x * log x
have _₁ : ψ x - θ x + θ x ≤ 2 * √x * log x + log 4 * x
Tactic: calc
  _ = ψ x - θ x + θ x := by ring
  _ ≤ 2 * x.sqrt * x.log + log 4 * x := by
    gcongr
    · exact le_trans (le_abs_self _) (abs_psi_sub_theta_le_sqrt_mul_log hx)
    · exact theta_le_log4_mul_x (by linarith)
  _ = _ := by ring
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 1 ≤ x
_ : ψ x = ψ x - θ x + θ x
_₁ : ψ x - θ x + θ x ≤ 2 * √x * log x + log 4 * x
⊢ ψ x ≤ log 4 * x + 2 * √x * log x
have _₂ : 2 * √x * log x + log 4 * x = log 4 * x + 2 * √x * log x
Tactic: calc
  _ = ψ x - θ x + θ x := by ring
  _ ≤ 2 * x.sqrt * x.log + log 4 * x := by
    gcongr
    · exact le_trans (le_abs_self _) (abs_psi_sub_theta_le_sqrt_mul_log hx)
    · exact theta_le_log4_mul_x (by linarith)
  _ = _ := by ring
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 0 ≤ x
⊢ ψ x ≤ (log 4 + 4) * x
have pos : ∀ (hx : x < 1), ψ x ≤ (log 4 + 4) * x
Tactic: by_cases! hx : x < 1
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 0 ≤ x
pos : ∀ (hx : x < 1), ψ x ≤ (log 4 + 4) * x
⊢ ψ x ≤ (log 4 + 4) * x
have neg : ∀ (hx : 1 ≤ x), ψ x ≤ (log 4 + 4) * x
Tactic: by_cases! hx : x < 1
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx_1 : 0 ≤ x
hx : x < 1
⊢ x < 2
have linarith : 2 ≤ x → -1 + (x - 1) + (2 - x) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx_1 : 0 ≤ x
hx : x < 1
⊢ ψ x ≤ (log 4 + 4) * x
have pos : 0 ≤ (log 4 + 4) * x
Tactic: rw [psi_eq_zero_of_lt_two (by linarith)]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx_1 : 0 ≤ x
hx : 1 ≤ x
⊢ ψ x ≤ (log 4 + 4) * x
have neg : log 4 * x + 2 * √x * log x ≤ (log 4 + 4) * x
Tactic: apply le_trans (psi_le hx)
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx_1 : 0 ≤ x
hx : 1 ≤ x
⊢ log 4 * x + 2 * √x * log x ≤ (log 4 + 4) * x
have neg : log 4 * x + 2 * √x * log x ≤ log 4 * x + 4 * x
Tactic: rw [add_mul]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx_1 : 0 ≤ x
hx : 1 ≤ x
⊢ log 4 * x + 2 * √x * log x ≤ log 4 * x + 4 * x
have neg : 2 * √x * log x ≤ 4 * x
Tactic: gcongr 1
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx_1 : 0 ≤ x
hx : 1 ≤ x
⊢ 0 ≤ x
have linarith : x < 0 → -1 + (1 - x) + (x - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx_1 : 0 ≤ x
hx : 1 ≤ x
⊢ 0 < 1 / 2
have linarith : 1 / 2 ≤ 0 → 2 / 2 = 1
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx_1 : 0 ≤ x
hx : 1 ≤ x
linarith : 1 / 2 ≤ 0 → 2 / 2 = 1
⊢ 0 < 1 / 2
have linarith₁ : 1 / 2 ≤ 0 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx_1 : 0 ≤ x
hx : 1 ≤ x
linarith : 1 / 2 ≤ 0 → 2 / 2 = 1
linarith₁ : 1 / 2 ≤ 0 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ 0 < 1 / 2
have linarith₂ : 1 / 2 ≤ 0 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx_1 : 0 ≤ x
hx : 1 ≤ x
linarith : 1 / 2 ≤ 0 → 2 / 2 = 1
linarith₁ : 1 / 2 ≤ 0 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : 1 / 2 ≤ 0 → GT.gt (α := ℝ) 2 0
⊢ 0 < 1 / 2
have linarith₃ : 1 / 2 ≤ 0 → -1 + HMul.hMul (α := ℝ) 1 1 = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx_1 : 0 ≤ x
hx : 1 ≤ x
⊢ 2 * √x * log x ≤ 4 * x
have neg : 2 * x ^ (1 / 2) * x ^ (1 / 2) * (1 / (1 / 2)) ≤ 4 * x
Tactic: grw [sqrt_eq_rpow, log_le_rpow_div (ε := 1 / 2) (by linarith) (by linarith), ← mul_div_assoc,
    ← mul_one_div]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx_1 : 0 ≤ x
hx : 1 ≤ x
⊢ 2 * x ^ (1 / 2) * x ^ (1 / 2) * (1 / (1 / 2)) ≤ 4 * x
have neg : 2 * (x ^ (1 / 2) * x ^ (1 / 2)) * (1 / (1 / 2)) ≤ 4 * x
Tactic: nth_rw 2 [mul_assoc]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx_1 : 0 ≤ x
hx : 1 ≤ x
⊢ 0 < x
have linarith : x ≤ 0 → -1 + (1 - x) + (x - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx_1 : 0 ≤ x
hx : 1 ≤ x
⊢ 2 * (x ^ (1 / 2) * x ^ (1 / 2)) * (1 / (1 / 2)) ≤ 4 * x
have neg : 2 * x ^ (1 / 2 + 1 / 2) * (1 / (1 / 2)) ≤ 4 * x
Tactic: rw [← rpow_add (by linarith)]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx_1 : 0 ≤ x
hx : 1 ≤ x
⊢ 2 * x ^ (1 / 2 + 1 / 2) * (1 / (1 / 2)) ≤ 4 * x
have neg : 2 * x * 2 ≤ 4 * x
Tactic: norm_num
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx_1 : 0 ≤ x
hx : 1 ≤ x
⊢ 2 * x * 2 ≤ 4 * x
have linarith : 4 * x < 2 * x * 2 → 4 * x - 2 * x * 2 = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
⊢ ψ x - θ x = ∑ n ∈ Ioc 0 ⌊x⌋₊ with ¬Nat.Prime n, (Λ : (a : ℕ) → ℝ) n
have rw : Eq (α := ℝ) (∑ x ∈ Ioc 0 ⌊x⌋₊, HSub.hSub (α := ℝ) ((Λ : (a : ℕ) → ℝ) x : ℝ) (if Nat.Prime x then log (↑x : ℝ) else 0))
  (∑ a ∈ Ioc 0 ⌊x⌋₊, if ¬Nat.Prime a then (Λ : (a : ℕ) → ℝ) a else 0)
Tactic: rw [psi, theta, sum_filter, sum_filter, ← sum_sub_distrib]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
⊢ Eq (α := ℝ) (∑ x ∈ Ioc 0 ⌊x⌋₊, HSub.hSub (α := ℝ) ((Λ : (a : ℕ) → ℝ) x : ℝ) (if Nat.Prime x then log (↑x : ℝ) else 0))
    (∑ a ∈ Ioc 0 ⌊x⌋₊, if ¬Nat.Prime a then (Λ : (a : ℕ) → ℝ) a else 0)
have refine : ∀ (n : ℕ) (hn : n ∈ Ioc 0 ⌊x⌋₊),
  HSub.hSub (α := ℝ) ((Λ : (a : ℕ) → ℝ) n : ℝ) (if Nat.Prime n then log (↑n : ℝ) else 0) =
    if ¬Nat.Prime n then (Λ : (a : ℕ) → ℝ) n else 0
Tactic: refine sum_congr rfl fun n hn ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
n : ℕ
hn : n ∈ Ioc 0 ⌊x⌋₊
⊢ HSub.hSub (α := ℝ) ((Λ : (a : ℕ) → ℝ) n : ℝ) (if Nat.Prime n then log (↑n : ℝ) else 0) =
    if ¬Nat.Prime n then (Λ : (a : ℕ) → ℝ) n else 0
have pos : ∀ (h : Nat.Prime n), HSub.hSub (α := ℝ) ((Λ : (a : ℕ) → ℝ) n : ℝ) (log (↑n : ℝ)) = 0
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
n : ℕ
hn : n ∈ Ioc 0 ⌊x⌋₊
pos : ∀ (h : Nat.Prime n), HSub.hSub (α := ℝ) ((Λ : (a : ℕ) → ℝ) n : ℝ) (log (↑n : ℝ)) = 0
⊢ HSub.hSub (α := ℝ) ((Λ : (a : ℕ) → ℝ) n : ℝ) (if Nat.Prime n then log (↑n : ℝ) else 0) =
    if ¬Nat.Prime n then (Λ : (a : ℕ) → ℝ) n else 0
have neg : ∀ (h : ¬Nat.Prime n), HSub.hSub (α := ℝ) (β := ℝ) ((Λ : (a : ℕ) → ℝ) n : ℝ) (0 : ℝ) = (Λ : (a : ℕ) → ℝ) n
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
n : ℕ
⊢ (↑n : ℝ) * log 2 - log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) ≤ ψ (↑n : ℝ)
have rw : log (HPow.hPow (α := ℝ) 2 n) ≤ log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑n.lcmUpto : ℝ))
Tactic: rw [tsub_le_iff_left, psi_eq_log_lcmUpto, ← log_pow 2,
    ← log_mul (by positivity) (by simp [lcmUpto_ne_zero])]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 0 ≤ x
⊢ (x - 1) * log 2 - log (x + 2) ≤ ψ x
have grw : (x - 1) * log 2 - log (x + 2) ≤ (↑⌊x⌋₊ : ℝ) * log 2 - log (HAdd.hAdd (α := ℝ) (↑⌊x⌋₊ : ℝ) 1)
Tactic: grw [psi_eq_psi_coe_floor, ← psi_ge]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 0 ≤ x
⊢ (x - 1) * log 2 - log (x + 2) ≤ (↑⌊x⌋₊ : ℝ) * log 2 - log (HAdd.hAdd (α := ℝ) (↑⌊x⌋₊ : ℝ) 1)
have hab : x - 1 ≤ (↑⌊x⌋₊ : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 0 ≤ x
hab : x - 1 ≤ (↑⌊x⌋₊ : ℝ)
⊢ (x - 1) * log 2 - log (x + 2) ≤ (↑⌊x⌋₊ : ℝ) * log 2 - log (HAdd.hAdd (α := ℝ) (↑⌊x⌋₊ : ℝ) 1)
have hcd : (↑⌊x⌋₊ : ℝ) ≤ x
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 0 ≤ x
hab : x - 1 ≤ (↑⌊x⌋₊ : ℝ)
hcd : (↑⌊x⌋₊ : ℝ) ≤ x
⊢ (x - 1) * log 2 - log (x + 2) ≤ (↑⌊x⌋₊ : ℝ) * log 2 - log (HAdd.hAdd (α := ℝ) (↑⌊x⌋₊ : ℝ) 1)
have hcd₁ : LE.le (α := ℝ) 1 2
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 1 ≤ x
⊢ ψ x - θ x ≤ 2 * √x * log x
have grw : ψ x - θ x ≤ |ψ x - θ x|
Tactic: grw [← abs_psi_sub_theta_le_sqrt_mul_log hx]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
n : ℕ
⊢ (↑n : ℝ) * log 2 - log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - 2 * √(↑n : ℝ) * log (↑n : ℝ) ≤ θ (↑n : ℝ)
have inl : (↑0 : ℝ) * log 2 - log (HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1) - 2 * √(↑0 : ℝ) * log (↑0 : ℝ) ≤ θ (↑0 : ℝ)
Tactic: rcases n.eq_zero_or_pos with rfl | hn
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
n : ℕ
inl : (↑0 : ℝ) * log 2 - log (HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1) - 2 * √(↑0 : ℝ) * log (↑0 : ℝ) ≤ θ (↑0 : ℝ)
⊢ (↑n : ℝ) * log 2 - log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - 2 * √(↑n : ℝ) * log (↑n : ℝ) ≤ θ (↑n : ℝ)
have inr : ∀ (hn : n > 0), (↑n : ℝ) * log 2 - log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - 2 * √(↑n : ℝ) * log (↑n : ℝ) ≤ θ (↑n : ℝ)
Tactic: rcases n.eq_zero_or_pos with rfl | hn
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
n : ℕ
hn : n > 0
⊢ (↑n : ℝ) * log 2 - log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - 2 * √(↑n : ℝ) * log (↑n : ℝ) ≤ θ (↑n : ℝ)
have linarith : θ (↑n : ℝ) < (↑n : ℝ) * log 2 - log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - 2 * √(↑n : ℝ) * log (↑n : ℝ) →
  θ (↑n : ℝ) - ((↑n : ℝ) * log 2 - log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - 2 * √(↑n : ℝ) * log (↑n : ℝ)) +
        ((↑n : ℝ) * log 2 - log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - ψ (↑n : ℝ)) +
      (ψ (↑n : ℝ) - θ (↑n : ℝ) - 2 * √(↑n : ℝ) * log (↑n : ℝ)) =
    0
Tactic: linarith [psi_ge n, psi_sub_theta_le (x := n) (mod_cast (one_le_of_lt hn))]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 1 ≤ x
⊢ (x - 1) * log 2 - log (x + 2) - 2 * √x * log x ≤ θ x
have grw : ψ x - 2 * √x * log x ≤ θ x
Tactic: grw [psi_ge' (by linarith)]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 1 ≤ x
⊢ ψ x - 2 * √x * log x ≤ θ x
have linarith : θ x < ψ x - 2 * √x * log x → θ x - (ψ x - 2 * √x * log x) + (ψ x - θ x - 2 * √x * log x) = 0
Tactic: linarith [psi_sub_theta_le hx]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
| IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ θ t / (t * HPow.hPow (β := ℕ) (log t) 2))
    (Set.Icc 2 x) volume
have arg : fun (t : ℝ) ↦ θ t / (t * HPow.hPow (β := ℕ) (log t) 2)
Tactic: arg 1
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
| fun (t : ℝ) ↦ θ t / (t * HPow.hPow (β := ℕ) (log t) 2)
have h : ∀ (x : ℝ), θ x / (x * HPow.hPow (β := ℕ) (log x) 2)
Tactic: ext
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x x_1 : ℝ
| θ x_1 / (x_1 * HPow.hPow (β := ℕ) (log x_1) 2)
have h : 1 / (x_1 * HPow.hPow (β := ℕ) (log x_1) 2) * ∑ a ∈ Ioc 0 ⌊x_1⌋₊, if Nat.Prime a then log (↑a : ℝ) else 0
Tactic: rw [theta, div_eq_mul_one_div, mul_comm, sum_filter]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
| IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ θ t / (t * HPow.hPow (β := ℕ) (log t) 2))
    (Set.Icc 2 x) volume
have h : ∀ (x : ℝ), 1 / (x * HPow.hPow (β := ℕ) (log x) 2) * ∑ a ∈ Ioc 0 ⌊x⌋₊, if Nat.Prime a then log (↑a : ℝ) else 0
Tactic: arg 1; ext; rw [theta, div_eq_mul_one_div, mul_comm, sum_filter]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ θ t / (t * HPow.hPow (β := ℕ) (log t) 2))
    (Set.Icc 2 x) volume
have conv : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
  (fun (x : ℝ) ↦ 1 / (x * HPow.hPow (β := ℕ) (log x) 2) * ∑ a ∈ Ioc 0 ⌊x⌋₊, if Nat.Prime a then log (↑a : ℝ) else 0)
  (Set.Icc 2 x) volume
Tactic: conv => arg 1; ext; rw [theta, div_eq_mul_one_div, mul_comm, sum_filter]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace)
    (fun (x : ℝ) ↦ 1 / (x * HPow.hPow (β := ℕ) (log x) 2) * ∑ a ∈ Ioc 0 ⌊x⌋₊, if Nat.Prime a then log (↑a : ℝ) else 0)
    (Set.Icc 2 x) volume
have refine : ∀ (x_1 : ℝ) (hx : x_1 ∈ Set.Icc 2 x), ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ 1 / (x * HPow.hPow (β := ℕ) (log x) 2)) x_1
Tactic: refine integrableOn_mul_sum_Icc _ (by norm_num) <| ContinuousOn.integrableOn_Icc fun x hx ↦
    ContinuousAt.continuousWithinAt ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x_1 x : ℝ
hx : x ∈ Set.Icc 2 x_1
⊢ x ≠ 0
have linarith : x = 0 → HMul.hMul (α := ℝ) 2 (-1) + (x - 0) + (2 - x) = 0
Tactic: linarith [hx.1]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x_1 x : ℝ
hx : x ∈ Set.Icc 2 x_1
linarith : x = 0 → HMul.hMul (α := ℝ) 2 (-1) + (x - 0) + (2 - x) = 0
⊢ x ≠ 0
have linarith₁ : x = 0 → GT.gt (α := ℝ) 2 0
Tactic: linarith [hx.1]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (hypothesis)
Goal:
x_1 x : ℝ
hx : x ∈ Set.Icc 2 x_1
⊢ ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ 1 / (x * HPow.hPow (β := ℕ) (log x) 2)) x
have this : x ≠ 0
Tactic: have : x ≠ 0 := by linarith [hx.1]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x_1 x : ℝ
hx : x ∈ Set.Icc 2 x_1
this : x ≠ 0
⊢ HPow.hPow (β := ℕ) (log x) 2 ≠ 0
have simp : ¬x = 0 ∧ ¬x = 1 ∧ ¬x = -1
Tactic: simp
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (hypothesis)
Goal:
x_1 x : ℝ
hx : x ∈ Set.Icc 2 x_1
this : x ≠ 0
⊢ ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ 1 / (x * HPow.hPow (β := ℕ) (log x) 2)) x
have this₁ : x * HPow.hPow (β := ℕ) (log x) 2 ≠ 0
Tactic: have : x * log x ^ 2 ≠ 0 := mul_ne_zero this <| by simp; grind
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 2 ≤ x
⊢ (↑(π ⌊x⌋₊) : ℝ) = θ x / log x + ∫ (t : ℝ) in 2..x, θ t / (t * HPow.hPow (β := ℕ) (log t) 2)
have simp : (↑(#({x ∈ range (⌊x⌋₊ + 1) | Nat.Prime x})) : ℝ) =
  θ x / log x + ∫ (t : ℝ) in 2..x, θ t / (t * HPow.hPow (β := ℕ) (log t) 2)
Tactic: simp only [primeCounting, primeCounting', count_eq_card_filter_range]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 2 ≤ x
⊢ (↑(#({x ∈ range (⌊x⌋₊ + 1) | Nat.Prime x})) : ℝ) =
    θ x / log x + ∫ (t : ℝ) in 2..x, θ t / (t * HPow.hPow (β := ℕ) (log t) 2)
have rw : (↑(∑ a ∈ Icc 0 ⌊x⌋₊, if Nat.Prime a then 1 else 0) : ℝ) =
  θ x / log x + ∫ (t : ℝ) in 2..x, θ t / (t * HPow.hPow (β := ℕ) (log t) 2)
Tactic: rw [card_eq_sum_ones, range_succ_eq_Icc_zero, sum_filter]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 2 ≤ x
⊢ (↑(∑ a ∈ Icc 0 ⌊x⌋₊, if Nat.Prime a then 1 else 0) : ℝ) =
    θ x / log x + ∫ (t : ℝ) in 2..x, θ t / (t * HPow.hPow (β := ℕ) (log t) 2)
have push_cast : (∑ x ∈ Icc 0 ⌊x⌋₊, if Nat.Prime x then 1 else 0) =
  θ x / log x + ∫ (t : ℝ) in 2..x, θ t / (t * HPow.hPow (β := ℕ) (log t) 2)
Tactic: push_cast
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (setOf Nat.Prime).indicator fun (n : ℕ) ↦ log (↑n : ℝ)
⊢ (∑ x ∈ Icc 0 ⌊x⌋₊, if Nat.Prime x then 1 else 0) =
    θ x / log x + ∫ (t : ℝ) in 2..x, θ t / (t * HPow.hPow (β := ℕ) (log t) 2)
have trans : Eq (α := ℝ) (∑ x ∈ Icc 0 ⌊x⌋₊, if Nat.Prime x then 1 else 0) (∑ n ∈ Icc 0 ⌊x⌋₊, (log (↑n : ℝ))⁻¹ * a n)
Tactic: trans ∑ n ∈ Icc 0 ⌊x⌋₊, (log n)⁻¹ * a n
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (setOf Nat.Prime).indicator fun (n : ℕ) ↦ log (↑n : ℝ)
trans : Eq (α := ℝ) (∑ x ∈ Icc 0 ⌊x⌋₊, if Nat.Prime x then 1 else 0) (∑ n ∈ Icc 0 ⌊x⌋₊, (log (↑n : ℝ))⁻¹ * a n)
⊢ (∑ x ∈ Icc 0 ⌊x⌋₊, if Nat.Prime x then 1 else 0) =
    θ x / log x + ∫ (t : ℝ) in 2..x, θ t / (t * HPow.hPow (β := ℕ) (log t) 2)
have trans₁ : ∑ n ∈ Icc 0 ⌊x⌋₊, (log (↑n : ℝ))⁻¹ * a n = θ x / log x + ∫ (t : ℝ) in 2..x, θ t / (t * HPow.hPow (β := ℕ) (log t) 2)
Tactic: trans ∑ n ∈ Icc 0 ⌊x⌋₊, (log n)⁻¹ * a n
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (setOf Nat.Prime).indicator fun (n : ℕ) ↦ log (↑n : ℝ)
⊢ Eq (α := ℝ) (∑ x ∈ Icc 0 ⌊x⌋₊, if Nat.Prime x then 1 else 0) (∑ n ∈ Icc 0 ⌊x⌋₊, (log (↑n : ℝ))⁻¹ * a n)
have refine : ∀ (n : ℕ) (hn : n ∈ Icc 0 ⌊x⌋₊), (if Nat.Prime n then 1 else 0) = (log (↑n : ℝ))⁻¹ * a n
Tactic: refine sum_congr rfl fun n hn ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (setOf Nat.Prime).indicator fun (n : ℕ) ↦ log (↑n : ℝ)
n : ℕ
hn : n ∈ Icc 0 ⌊x⌋₊
⊢ (if Nat.Prime n then 1 else 0) = (log (↑n : ℝ))⁻¹ * a n
have pos : ∀ (h : Nat.Prime n), 1 = (log (↑n : ℝ))⁻¹ * a n
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (setOf Nat.Prime).indicator fun (n : ℕ) ↦ log (↑n : ℝ)
n : ℕ
hn : n ∈ Icc 0 ⌊x⌋₊
pos : ∀ (h : Nat.Prime n), 1 = (log (↑n : ℝ))⁻¹ * a n
⊢ (if Nat.Prime n then 1 else 0) = (log (↑n : ℝ))⁻¹ * a n
have neg : ∀ (h : ¬Nat.Prime n), 0 = (log (↑n : ℝ))⁻¹ * a n
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (hypothesis)
Goal:
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (setOf Nat.Prime).indicator fun (n : ℕ) ↦ log (↑n : ℝ)
n : ℕ
hn : n ∈ Icc 0 ⌊x⌋₊
h : Nat.Prime n
⊢ 1 = (log (↑n : ℝ))⁻¹ * a n
have this : log (↑n : ℝ) ≠ 0
Tactic: have : log n ≠ 0 := log_ne_zero_of_pos_of_ne_one (mod_cast h.pos) (mod_cast h.ne_one)
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (setOf Nat.Prime).indicator fun (n : ℕ) ↦ log (↑n : ℝ)
⊢ ∑ n ∈ Icc 0 ⌊x⌋₊, (log (↑n : ℝ))⁻¹ * a n = θ x / log x + ∫ (t : ℝ) in 2..x, θ t / (t * HPow.hPow (β := ℕ) (log t) 2)
have rw : (log x)⁻¹ * ∑ k ∈ Icc 0 ⌊x⌋₊, a k -
    ∫ (x : ℝ) in 2..x, HMul.hMul (α := ℝ) (deriv (fun (n : ℝ) ↦ (log n)⁻¹) x) (∑ k ∈ Icc 0 ⌊x⌋₊, a k) =
  θ x / log x + ∫ (t : ℝ) in 2..x, θ t / (t * HPow.hPow (β := ℕ) (log t) 2)
Tactic: rw [sum_mul_eq_sub_integral_mul₁ a (f := fun n ↦ (log n)⁻¹) (by simp [a]) (by simp [a]),
    ← intervalIntegral.integral_of_le hx]