awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 1 ≤ x
⊢ ψ x - θ x ≤ 2 * √x * log x

Tactic:
le_trans (le_abs_self _) (abs_psi_sub_theta_le_sqrt_mul_log hx)

Premises used: Chebyshev.abs_psi_sub_theta_le_sqrt_mul_log, le_abs_self, le_trans
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 1 ≤ x
⊢ ψ x - θ x ≤ 2 * √x * log x

Tactic:
exact le_trans (le_abs_self _) (abs_psi_sub_theta_le_sqrt_mul_log hx)

Premises used: Chebyshev.abs_psi_sub_theta_le_sqrt_mul_log, le_abs_self, le_trans
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 1 ≤ x
linarith : x < 0 → -1 + (1 - x) + (x - 0) = 0
⊢ 0 ≤ x

Tactic:
linarith
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 1 ≤ x
⊢ θ x ≤ log 4 * x

Tactic:
exact theta_le_log4_mul_x (by linarith)

Premises used: Chebyshev.theta_le_log4_mul_x
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 1 ≤ x
⊢ 2 * √x * log x + log 4 * x = log 4 * x + 2 * √x * log x

Tactic:
ring
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 1 ≤ x
_ : ψ x = ψ x - θ x + θ x
_₁ : ψ x - θ x + θ x ≤ 2 * √x * log x + log 4 * x
_₂ : 2 * √x * log x + log 4 * x = log 4 * x + 2 * √x * log x
⊢ ψ 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

Premises used: Real.log, Chebyshev.psi, Chebyshev.theta, Real.sqrt, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 0 ≤ x
pos : ∀ (hx : x < 1), ψ x ≤ (log 4 + 4) * x
neg : ∀ (hx : 1 ≤ x), ψ x ≤ (log 4 + 4) * x
⊢ ψ x ≤ (log 4 + 4) * x

Tactic:
by_cases! hx : x < 1
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx_1 : 0 ≤ x
hx : x < 1
linarith : 2 ≤ x → -1 + (x - 1) + (2 - x) = 0
⊢ x < 2

Tactic:
linarith
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx_1 : 0 ≤ x
hx : x < 1
pos : 0 ≤ (log 4 + 4) * x
⊢ ψ x ≤ (log 4 + 4) * x

Tactic:
rw [psi_eq_zero_of_lt_two (by linarith)]

Premises used: Chebyshev.psi_eq_zero_of_lt_two
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx_1 : 0 ≤ x
hx : x < 1
⊢ 0 ≤ (log 4 + 4) * x

Tactic:
bound
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx_1 : 0 ≤ x
hx : 1 ≤ x
neg : log 4 * x + 2 * √x * log x ≤ (log 4 + 4) * x
⊢ ψ x ≤ (log 4 + 4) * x

Tactic:
apply le_trans (psi_le hx)

Premises used: Chebyshev.psi_le, le_trans
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx_1 : 0 ≤ x
hx : 1 ≤ x
neg : log 4 * x + 2 * √x * log x ≤ log 4 * x + 4 * x
⊢ log 4 * x + 2 * √x * log x ≤ (log 4 + 4) * x

Tactic:
rw [add_mul]

Premises used: add_mul
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx_1 : 0 ≤ x
hx : 1 ≤ x
neg : 2 * √x * log x ≤ 4 * x
⊢ log 4 * x + 2 * √x * log x ≤ log 4 * x + 4 * x

Tactic:
gcongr 1
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx_1 : 0 ≤ x
hx : 1 ≤ x
linarith : x < 0 → -1 + (1 - x) + (x - 0) = 0
⊢ 0 ≤ x

Tactic:
linarith
-- Module: Mathlib.NumberTheory.Chebyshev
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
linarith₃ : 1 / 2 ≤ 0 → -1 + HMul.hMul (α := ℝ) 1 1 = 0
⊢ 0 < 1 / 2

Tactic:
linarith
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx_1 : 0 ≤ x
hx : 1 ≤ x
neg : 2 * x ^ (1 / 2) * x ^ (1 / 2) * (1 / (1 / 2)) ≤ 4 * x
⊢ 2 * √x * log x ≤ 4 * x

Tactic:
grw [sqrt_eq_rpow, log_le_rpow_div (ε := 1 / 2) (by linarith) (by linarith), ← mul_div_assoc,
    ← mul_one_div]

Premises used: mul_div_assoc, Real.log_le_rpow_div, mul_one_div, Real.sqrt_eq_rpow
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx_1 : 0 ≤ x
hx : 1 ≤ x
neg : 2 * (x ^ (1 / 2) * x ^ (1 / 2)) * (1 / (1 / 2)) ≤ 4 * x
⊢ 2 * x ^ (1 / 2) * x ^ (1 / 2) * (1 / (1 / 2)) ≤ 4 * x

Tactic:
nth_rw 2 [mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx_1 : 0 ≤ x
hx : 1 ≤ x
linarith : x ≤ 0 → -1 + (1 - x) + (x - 0) = 0
⊢ 0 < x

Tactic:
linarith
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx_1 : 0 ≤ x
hx : 1 ≤ x
neg : 2 * x ^ (1 / 2 + 1 / 2) * (1 / (1 / 2)) ≤ 4 * x
⊢ 2 * (x ^ (1 / 2) * x ^ (1 / 2)) * (1 / (1 / 2)) ≤ 4 * x

Tactic:
rw [← rpow_add (by linarith)]

Premises used: Real.rpow_add
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx_1 : 0 ≤ x
hx : 1 ≤ x
neg : 2 * x * 2 ≤ 4 * x
⊢ 2 * x ^ (1 / 2 + 1 / 2) * (1 / (1 / 2)) ≤ 4 * x

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx_1 : 0 ≤ x
hx : 1 ≤ x
linarith : 4 * x < 2 * x * 2 → 4 * x - 2 * x * 2 = 0
⊢ 2 * x * 2 ≤ 4 * x

Tactic:
linarith
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
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)
⊢ ψ x - θ x = ∑ n ∈ Ioc 0 ⌊x⌋₊ with ¬Nat.Prime n, (Λ : (a : ℕ) → ℝ) n

Tactic:
rw [psi, theta, sum_filter, sum_filter, ← sum_sub_distrib]

Premises used: Chebyshev.psi, Chebyshev.theta, Finset.sum_sub_distrib, Finset.sum_filter
-- Module: Mathlib.NumberTheory.Chebyshev
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)

Tactic:
sum_congr rfl fun n hn ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
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
⊢ 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:
refine sum_congr rfl fun n hn ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
n : ℕ
hn : n ∈ Ioc 0 ⌊x⌋₊
pos : ∀ (h : Nat.Prime n), HSub.hSub (α := ℝ) ((Λ : (a : ℕ) → ℝ) n : ℝ) (log (↑n : ℝ)) = 0
neg : ∀ (h : ¬Nat.Prime n), HSub.hSub (α := ℝ) (β := ℝ) ((Λ : (a : ℕ) → ℝ) n : ℝ) (0 : ℝ) = (Λ : (a : ℕ) → ℝ) n
⊢ HSub.hSub (α := ℝ) ((Λ : (a : ℕ) → ℝ) n : ℝ) (if Nat.Prime n then log (↑n : ℝ) else 0) =
    if ¬Nat.Prime n then (Λ : (a : ℕ) → ℝ) n else 0

Tactic:
split_ifs with h
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
n : ℕ
hn : n ∈ Ioc 0 ⌊x⌋₊
h : Nat.Prime n
⊢ HSub.hSub (α := ℝ) ((Λ : (a : ℕ) → ℝ) n : ℝ) (log (↑n : ℝ)) = 0

Tactic:
simp [h, vonMangoldt_apply_prime]

Premises used: ArithmeticFunction.vonMangoldt_apply_prime
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
n : ℕ
hn : n ∈ Ioc 0 ⌊x⌋₊
h : ¬Nat.Prime n
⊢ HSub.hSub (α := ℝ) (β := ℝ) ((Λ : (a : ℕ) → ℝ) n : ℝ) (0 : ℝ) = (Λ : (a : ℕ) → ℝ) n

Tactic:
simp
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n : ℕ
⊢ HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 ≠ 0

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n : ℕ
⊢ Ne (α := ℝ) (↑n.lcmUpto : ℝ) 0

Tactic:
simp [lcmUpto_ne_zero]

Premises used: Nat.lcmUpto_ne_zero
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n : ℕ
rw : log (HPow.hPow (α := ℝ) 2 n) ≤ log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑n.lcmUpto : ℝ))
⊢ (↑n : ℝ) * log 2 - log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) ≤ ψ (↑n : ℝ)

Tactic:
rw [tsub_le_iff_left, psi_eq_log_lcmUpto, ← log_pow 2,
    ← log_mul (by positivity) (by simp [lcmUpto_ne_zero])]

Premises used: Chebyshev.psi_eq_log_lcmUpto, tsub_le_iff_left, Real.log_pow, OfNat.ofNat, Real.log_mul
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n : ℕ
⊢ 0 < HPow.hPow (α := ℝ) 2 n

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n : ℕ
⊢ log (HPow.hPow (α := ℝ) 2 n) ≤ log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 * (↑n.lcmUpto : ℝ))

Tactic:
exact log_le_log (by positivity) <| mod_cast two_pow_le_mul_lcmUpto n

Premises used: Chebyshev.two_pow_le_mul_lcmUpto, Real.log_le_log
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 0 ≤ x
grw : (x - 1) * log 2 - log (x + 2) ≤ (↑⌊x⌋₊ : ℝ) * log 2 - log (HAdd.hAdd (α := ℝ) (↑⌊x⌋₊ : ℝ) 1)
⊢ (x - 1) * log 2 - log (x + 2) ≤ ψ x

Tactic:
grw [psi_eq_psi_coe_floor, ← psi_ge]

Premises used: Chebyshev.psi_eq_psi_coe_floor, Chebyshev.psi_ge
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 0 ≤ x
hab : x - 1 ≤ (↑⌊x⌋₊ : ℝ)
hcd : (↑⌊x⌋₊ : ℝ) ≤ x
hcd₁ : LE.le (α := ℝ) 1 2
⊢ (x - 1) * log 2 - log (x + 2) ≤ (↑⌊x⌋₊ : ℝ) * log 2 - log (HAdd.hAdd (α := ℝ) (↑⌊x⌋₊ : ℝ) 1)

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 0 ≤ x
⊢ x - 1 ≤ (↑⌊x⌋₊ : ℝ)

Tactic:
(Nat.sub_one_lt_floor x).le

Premises used: LT.lt.le, Nat.sub_one_lt_floor
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 0 ≤ x
⊢ x - 1 ≤ (↑⌊x⌋₊ : ℝ)

Tactic:
exact (Nat.sub_one_lt_floor x).le

Premises used: LT.lt.le, Nat.sub_one_lt_floor
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 0 ≤ x
⊢ LE.le (α := ℝ) 1 2

Tactic:
one_le_two

Premises used: one_le_two
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 0 ≤ x
⊢ LE.le (α := ℝ) 1 2

Tactic:
exact one_le_two

Premises used: one_le_two
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 1 ≤ x
grw : ψ x - θ x ≤ |ψ x - θ x|
⊢ ψ x - θ x ≤ 2 * √x * log x

Tactic:
grw [← abs_psi_sub_theta_le_sqrt_mul_log hx]

Premises used: Chebyshev.abs_psi_sub_theta_le_sqrt_mul_log
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 1 ≤ x
⊢ ψ x - θ x ≤ |ψ x - θ x|

Tactic:
le_abs_self _

Premises used: le_abs_self
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 1 ≤ x
⊢ ψ x - θ x ≤ |ψ x - θ x|

Tactic:
exact le_abs_self _

Premises used: le_abs_self
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n : ℕ
inl : (↑0 : ℝ) * log 2 - log (HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1) - 2 * √(↑0 : ℝ) * log (↑0 : ℝ) ≤ θ (↑0 : ℝ)
inr : ∀ (hn : n > 0), (↑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 : ℝ)

Tactic:
rcases n.eq_zero_or_pos with rfl | hn

Premises used: Nat.eq_zero_or_pos, rfl
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
⊢ (↑0 : ℝ) * log 2 - log (HAdd.hAdd (α := ℝ) (↑0 : ℝ) 1) - 2 * √(↑0 : ℝ) * log (↑0 : ℝ) ≤ θ (↑0 : ℝ)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n : ℕ
hn : n > 0
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
⊢ (↑n : ℝ) * log 2 - log (HAdd.hAdd (α := ℝ) (↑n : ℝ) 1) - 2 * √(↑n : ℝ) * log (↑n : ℝ) ≤ θ (↑n : ℝ)

Tactic:
linarith [psi_ge n, psi_sub_theta_le (x := n) (mod_cast (one_le_of_lt hn))]

Premises used: congrArg, cast, Chebyshev.psi_sub_theta_le, Nat.cast_le._simp_1, LE.le, Nat.one_le_of_lt, Nat.cast, Chebyshev.psi_ge, congrFun', Eq.symm, Nat.cast_one, Eq.trans
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 1 ≤ x
grw : ψ x - 2 * √x * log x ≤ θ x
⊢ (x - 1) * log 2 - log (x + 2) - 2 * √x * log x ≤ θ x

Tactic:
grw [psi_ge' (by linarith)]

Premises used: Chebyshev.psi_ge'
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 1 ≤ x
linarith : θ x < ψ x - 2 * √x * log x → θ x - (ψ x - 2 * √x * log x) + (ψ x - θ x - 2 * √x * log x) = 0
⊢ ψ x - 2 * √x * log x ≤ θ x

Tactic:
linarith [psi_sub_theta_le hx]

Premises used: Chebyshev.psi_sub_theta_le
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
arg : fun (t : ℝ) ↦ θ t / (t * HPow.hPow (β := ℕ) (log t) 2)
| IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ θ t / (t * HPow.hPow (β := ℕ) (log t) 2))
    (Set.Icc 2 x) volume

Tactic:
arg 1
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
h : ∀ (x : ℝ), θ x / (x * HPow.hPow (β := ℕ) (log x) 2)
| fun (t : ℝ) ↦ θ t / (t * HPow.hPow (β := ℕ) (log t) 2)

Tactic:
ext
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x x_1 : ℝ
h : 1 / (x_1 * HPow.hPow (β := ℕ) (log x_1) 2) * ∑ a ∈ Ioc 0 ⌊x_1⌋₊, if Nat.Prime a then log (↑a : ℝ) else 0
| θ x_1 / (x_1 * HPow.hPow (β := ℕ) (log x_1) 2)

Tactic:
rw [theta, div_eq_mul_one_div, mul_comm, sum_filter]

Premises used: Chebyshev.theta, div_eq_mul_one_div, mul_comm, Finset.sum_filter
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
h : ∀ (x : ℝ), 1 / (x * HPow.hPow (β := ℕ) (log x) 2) * ∑ a ∈ Ioc 0 ⌊x⌋₊, if Nat.Prime a then log (↑a : ℝ) else 0
| IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ θ t / (t * HPow.hPow (β := ℕ) (log t) 2))
    (Set.Icc 2 x) volume

Tactic:
arg 1; ext; rw [theta, div_eq_mul_one_div, mul_comm, sum_filter]

Premises used: Chebyshev.theta, div_eq_mul_one_div, mul_comm, Finset.sum_filter
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
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
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (fun (t : ℝ) ↦ θ t / (t * HPow.hPow (β := ℕ) (log t) 2))
    (Set.Icc 2 x) volume

Tactic:
conv => arg 1; ext; rw [theta, div_eq_mul_one_div, mul_comm, sum_filter]

Premises used: Chebyshev.theta, div_eq_mul_one_div, mul_comm, Finset.sum_filter
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
⊢ LE.le (α := ℝ) 0 2

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
refine :
  ∀ (x_1 : ℝ) (hx : x_1 ∈ Set.Icc 2 x), ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ 1 / (x * HPow.hPow (β := ℕ) (log x) 2)) x_1
⊢ 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:
refine integrableOn_mul_sum_Icc _ (by norm_num) <| ContinuousOn.integrableOn_Icc fun x hx ↦
    ContinuousAt.continuousWithinAt ?_

Premises used: ContinuousOn.integrableOn_Icc, ContinuousAt.continuousWithinAt, integrableOn_mul_sum_Icc
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x_1 x : ℝ
hx : x ∈ Set.Icc 2 x_1
linarith : x = 0 → HMul.hMul (α := ℝ) 2 (-1) + (x - 0) + (2 - x) = 0
linarith₁ : x = 0 → GT.gt (α := ℝ) 2 0
⊢ x ≠ 0

Tactic:
linarith [hx.1]

Premises used: And.left
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x_1 x : ℝ
hx : x ∈ Set.Icc 2 x_1
⊢ x ≠ 0

Tactic:
have : x ≠ 0 := by linarith [hx.1]
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x_1 x : ℝ
hx : x ∈ Set.Icc 2 x_1
this : x ≠ 0
simp : ¬x = 0 ∧ ¬x = 1 ∧ ¬x = -1
⊢ HPow.hPow (β := ℕ) (log x) 2 ≠ 0

Tactic:
simp
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x_1 x : ℝ
hx : x ∈ Set.Icc 2 x_1
this : x ≠ 0
⊢ ¬x = 0 ∧ ¬x = 1 ∧ ¬x = -1

Tactic:
grind
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x_1 x : ℝ
hx : x ∈ Set.Icc 2 x_1
this : x ≠ 0
⊢ x * HPow.hPow (β := ℕ) (log x) 2 ≠ 0

Tactic:
have : x * log x ^ 2 ≠ 0 := mul_ne_zero this <| by simp; grind
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x_1 x : ℝ
hx : x ∈ Set.Icc 2 x_1
this_1 : x ≠ 0
this : x * HPow.hPow (β := ℕ) (log x) 2 ≠ 0
funProp : x ≠ 0
funProp₁ : x * HPow.hPow (β := ℕ) (log x) 2 ≠ 0
⊢ ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ 1 / (x * HPow.hPow (β := ℕ) (log x) 2)) x

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 2 ≤ x
simp :
  (↑(#({x ∈ range (⌊x⌋₊ + 1) | Nat.Prime x})) : ℝ) =
    θ x / log x + ∫ (t : ℝ) in 2..x, θ t / (t * HPow.hPow (β := ℕ) (log t) 2)
⊢ (↑(π ⌊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]

Premises used: Nat.count_eq_card_filter_range, Nat.primeCounting', Nat.primeCounting
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 2 ≤ x
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)
⊢ (↑(#({x ∈ range (⌊x⌋₊ + 1) | Nat.Prime x})) : ℝ) =
    θ 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]

Premises used: Finset.card_eq_sum_ones, Nat.range_succ_eq_Icc_zero, Finset.sum_filter
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 2 ≤ x
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)
⊢ (↑(∑ 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:
push_cast
-- Module: Mathlib.NumberTheory.Chebyshev
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)
trans₁ :
  ∑ n ∈ Icc 0 ⌊x⌋₊, (log (↑n : ℝ))⁻¹ * a n = θ x / log x + ∫ (t : ℝ) in 2..x, θ t / (t * HPow.hPow (β := ℕ) (log t) 2)
⊢ (∑ 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:
trans ∑ n ∈ Icc 0 ⌊x⌋₊, (log n)⁻¹ * a n

Premises used: Finset.Icc, Nat.floor, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Chebyshev
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)

Tactic:
sum_congr rfl fun n hn ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (setOf Nat.Prime).indicator fun (n : ℕ) ↦ log (↑n : ℝ)
refine : ∀ (n : ℕ) (hn : n ∈ Icc 0 ⌊x⌋₊), (if Nat.Prime n then 1 else 0) = (log (↑n : ℝ))⁻¹ * a n
⊢ Eq (α := ℝ) (∑ x ∈ Icc 0 ⌊x⌋₊, if Nat.Prime x then 1 else 0) (∑ n ∈ Icc 0 ⌊x⌋₊, (log (↑n : ℝ))⁻¹ * a n)

Tactic:
refine sum_congr rfl fun n hn ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.NumberTheory.Chebyshev
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
neg : ∀ (h : ¬Nat.Prime n), 0 = (log (↑n : ℝ))⁻¹ * a n
⊢ (if Nat.Prime n then 1 else 0) = (log (↑n : ℝ))⁻¹ * a n

Tactic:
split_ifs with h
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (setOf Nat.Prime).indicator fun (n : ℕ) ↦ log (↑n : ℝ)
n : ℕ
hn : n ∈ Icc 0 ⌊x⌋₊
h : Nat.Prime n
⊢ 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)
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (setOf Nat.Prime).indicator fun (n : ℕ) ↦ log (↑n : ℝ)
n : ℕ
hn : n ∈ Icc 0 ⌊x⌋₊
h : Nat.Prime n
this : log (↑n : ℝ) ≠ 0
⊢ 1 = (log (↑n : ℝ))⁻¹ * a n

Tactic:
simp [a, h, field]
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (setOf Nat.Prime).indicator fun (n : ℕ) ↦ log (↑n : ℝ)
n : ℕ
hn : n ∈ Icc 0 ⌊x⌋₊
h : ¬Nat.Prime n
⊢ 0 = (log (↑n : ℝ))⁻¹ * a n

Tactic:
simp [a, h]
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (setOf Nat.Prime).indicator fun (n : ℕ) ↦ log (↑n : ℝ)
⊢ a 0 = 0

Tactic:
simp [a]
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (setOf Nat.Prime).indicator fun (n : ℕ) ↦ log (↑n : ℝ)
⊢ a 1 = 0

Tactic:
simp [a]
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (setOf Nat.Prime).indicator fun (n : ℕ) ↦ log (↑n : ℝ)
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)
hf_diff : ∀ t ∈ Set.Icc 2 x, DifferentiableAt ℝ (F := ℝ) (fun (n : ℝ) ↦ (log n)⁻¹) t
hf_int :
  IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (deriv fun (n : ℝ) ↦ (log n)⁻¹) (Set.Icc 2 x) volume
⊢ ∑ n ∈ Icc 0 ⌊x⌋₊, (log (↑n : ℝ))⁻¹ * a n = θ 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]

Premises used: sum_mul_eq_sub_integral_mul₁, intervalIntegral.integral_of_le
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (setOf Nat.Prime).indicator fun (n : ℕ) ↦ log (↑n : ℝ)
f : ℝ → ℝ
u : ℝ
h : u ∈ Set.uIcc 2 x
⊢ deriv (fun (x : ℝ) ↦ (log x)⁻¹) u * f u = f u * -(u * HPow.hPow (β := ℕ) (log u) 2)⁻¹

Tactic:
simp [deriv_inv_log, field]

Premises used: Real.deriv_inv_log
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (setOf Nat.Prime).indicator fun (n : ℕ) ↦ log (↑n : ℝ)
⊢ ∀ (f : ℝ → ℝ),
    Eq (α := ℝ) (∫ (u : ℝ) in 2..x, deriv (fun (x : ℝ) ↦ (log x)⁻¹) u * f u)
      (∫ (u : ℝ) in 2..x, f u * -(u * HPow.hPow (β := ℕ) (log u) 2)⁻¹)

Tactic:
have int_deriv (f : ℝ → ℝ) :
        ∫ u in 2..x, deriv (fun x ↦ (log x)⁻¹) u * f u =
        ∫ u in 2..x, f u * -(u * log u ^ 2)⁻¹ :=
      intervalIntegral.integral_congr fun u _ ↦ by simp [deriv_inv_log, field]
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (setOf Nat.Prime).indicator fun (n : ℕ) ↦ log (↑n : ℝ)
int_deriv :
  ∀ (f : ℝ → ℝ),
    Eq (α := ℝ) (∫ (u : ℝ) in 2..x, deriv (fun (x : ℝ) ↦ (log x)⁻¹) u * f u)
      (∫ (u : ℝ) in 2..x, f u * -(u * HPow.hPow (β := ℕ) (log u) 2)⁻¹)
simp :
  ((log x)⁻¹ * ∑ x ∈ Icc 0 ⌊x⌋₊, if Nat.Prime x then log (↑x : ℝ) else 0) +
      ∫ (x : ℝ) in 2..x,
        (∑ x ∈ Icc 0 ⌊x⌋₊, if Nat.Prime x then log (↑x : ℝ) else 0) * ((HPow.hPow (β := ℕ) (log x) 2)⁻¹ * x⁻¹) =
    (∑ a ∈ Icc 0 ⌊x⌋₊, if Nat.Prime a then log (↑a : ℝ) else 0) / log x +
      ∫ (t : ℝ) in 2..x,
        (∑ a ∈ Icc 0 ⌊t⌋₊, if Nat.Prime a then log (↑a : ℝ) else 0) / (t * HPow.hPow (β := ℕ) (log t) 2)
⊢ (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:
simp [int_deriv, a, Set.indicator_apply, sum_filter, theta_eq_sum_Icc]

Premises used: Set.indicator_apply, Chebyshev.theta_eq_sum_Icc, Finset.sum_filter
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (setOf Nat.Prime).indicator fun (n : ℕ) ↦ log (↑n : ℝ)
int_deriv :
  ∀ (f : ℝ → ℝ),
    Eq (α := ℝ) (∫ (u : ℝ) in 2..x, deriv (fun (x : ℝ) ↦ (log x)⁻¹) u * f u)
      (∫ (u : ℝ) in 2..x, f u * -(u * HPow.hPow (β := ℕ) (log u) 2)⁻¹)
⊢ ((log x)⁻¹ * ∑ x ∈ Icc 0 ⌊x⌋₊, if Nat.Prime x then log (↑x : ℝ) else 0) +
      ∫ (x : ℝ) in 2..x,
        (∑ x ∈ Icc 0 ⌊x⌋₊, if Nat.Prime x then log (↑x : ℝ) else 0) * ((HPow.hPow (β := ℕ) (log x) 2)⁻¹ * x⁻¹) =
    (∑ a ∈ Icc 0 ⌊x⌋₊, if Nat.Prime a then log (↑a : ℝ) else 0) / log x +
      ∫ (t : ℝ) in 2..x,
        (∑ a ∈ Icc 0 ⌊t⌋₊, if Nat.Prime a then log (↑a : ℝ) else 0) / (t * HPow.hPow (β := ℕ) (log t) 2)

Tactic:
grind
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (setOf Nat.Prime).indicator fun (n : ℕ) ↦ log (↑n : ℝ)
z : ℝ
hf_diff : 2 ≤ z → z ≤ x → DifferentiableAt ℝ (F := ℝ) (fun (n : ℝ) ↦ (log n)⁻¹) z
⊢ z ∈ Set.Icc 2 x → DifferentiableAt ℝ (F := ℝ) (fun (n : ℝ) ↦ (log n)⁻¹) z

Tactic:
⟨_, _⟩
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (setOf Nat.Prime).indicator fun (n : ℕ) ↦ log (↑n : ℝ)
z : ℝ
left : 2 ≤ z
right : z ≤ x
linarith : z = 0 → HMul.hMul (α := ℝ) 2 (-1) + (2 - z) + (z - 0) = 0
linarith₁ : z = 0 → GT.gt (α := ℝ) 2 0
⊢ z ≠ 0

Tactic:
linarith
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (setOf Nat.Prime).indicator fun (n : ℕ) ↦ log (↑n : ℝ)
z : ℝ
left : 2 ≤ z
right : z ≤ x
⊢ z ≠ 0

Tactic:
have : z ≠ 0 := by linarith
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (setOf Nat.Prime).indicator fun (n : ℕ) ↦ log (↑n : ℝ)
z : ℝ
left : 2 ≤ z
right : z ≤ x
this : z ≠ 0
hx_pos : 0 < z
hx₁ : z ≠ 1
⊢ log z ≠ 0

Tactic:
apply log_ne_zero_of_pos_of_ne_one

Premises used: Real.log_ne_zero_of_pos_of_ne_one