awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
linarith : z ≤ 0 → HMul.hMul (α := ℝ) 2 (-1) + (2 - z) + (z - 0) = 0
linarith₁ : z ≤ 0 → GT.gt (α := ℝ) 2 0
⊢ 0 < z

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
this : z ≠ 0
linarith : z = 1 → -1 + (2 - z) + (z - 1) = 0
⊢ z ≠ 1

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
this : z ≠ 0
⊢ log z ≠ 0

Tactic:
have : log z ≠ 0 := by apply log_ne_zero_of_pos_of_ne_one <;> 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_1 : z ≠ 0
this : log z ≠ 0
funProp : z ≠ 0
funProp₁ : log z ≠ 0
⊢ DifferentiableAt ℝ (F := ℝ) (fun (n : ℝ) ↦ (log n)⁻¹) z

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (setOf Nat.Prime).indicator fun (n : ℕ) ↦ log (↑n : ℝ)
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (deriv fun (n : ℝ) ↦ (log n)⁻¹) (Set.Icc 2 x) volume

Tactic:
ContinuousOn.integrableOn_Icc fun z ⟨_, _⟩ ↦ ContinuousWithinAt.congr ?_
      (fun _ _ ↦ deriv_inv_log) deriv_inv_log

Premises used: ContinuousWithinAt, deriv, ContinuousOn.integrableOn_Icc, Real.deriv_inv_log, _private.0.Chebyshev.primeCounting_eq_theta_div_log_add_integral.match_1, Real.log, Inv.inv, Set.Icc, OfNat.ofNat, ContinuousWithinAt.congr
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (setOf Nat.Prime).indicator fun (n : ℕ) ↦ log (↑n : ℝ)
hf_int :
  ∀ z ∈ Set.Icc 2 x,
    2 ≤ z → z ≤ x → ContinuousWithinAt (Y := ℝ) (fun (x : ℝ) ↦ -x⁻¹ / HPow.hPow (β := ℕ) (log x) 2) (Set.Icc 2 x) z
⊢ IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (deriv fun (n : ℝ) ↦ (log n)⁻¹) (Set.Icc 2 x) volume

Tactic:
refine ContinuousOn.integrableOn_Icc fun z ⟨_, _⟩ ↦ ContinuousWithinAt.congr ?_
      (fun _ _ ↦ deriv_inv_log) deriv_inv_log

Premises used: ContinuousOn.integrableOn_Icc
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (setOf Nat.Prime).indicator fun (n : ℕ) ↦ log (↑n : ℝ)
z : ℝ
h : z ∈ Set.Icc 2 x
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 : ℝ
h : z ∈ Set.Icc 2 x
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 : ℝ
h : z ∈ Set.Icc 2 x
left : 2 ≤ z
right : z ≤ x
this : z ≠ 0
⊢ HPow.hPow (β := ℕ) (log z) 2 ≠ 0

Tactic:
pow_ne_zero 2 <| log_ne_zero_of_pos_of_ne_one ?_ ?_

Premises used: pow_ne_zero, OfNat.ofNat, Real.log_ne_zero_of_pos_of_ne_one
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (setOf Nat.Prime).indicator fun (n : ℕ) ↦ log (↑n : ℝ)
z : ℝ
h : z ∈ Set.Icc 2 x
left : 2 ≤ z
right : z ≤ x
this : z ≠ 0
refine_1 : 0 < z
refine_2 : z ≠ 1
⊢ HPow.hPow (β := ℕ) (log z) 2 ≠ 0

Tactic:
refine pow_ne_zero 2 <| log_ne_zero_of_pos_of_ne_one ?_ ?_

Premises used: pow_ne_zero, OfNat.ofNat, Real.log_ne_zero_of_pos_of_ne_one
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (setOf Nat.Prime).indicator fun (n : ℕ) ↦ log (↑n : ℝ)
z : ℝ
h : z ∈ Set.Icc 2 x
left : 2 ≤ z
right : z ≤ x
this : z ≠ 0
linarith : z ≤ 0 → HMul.hMul (α := ℝ) 2 (-1) + (2 - z) + (z - 0) = 0
linarith₁ : z ≤ 0 → GT.gt (α := ℝ) 2 0
⊢ 0 < z

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

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

Tactic:
have : log z ^ 2 ≠ 0 := by
      refine pow_ne_zero 2 <| log_ne_zero_of_pos_of_ne_one ?_ ?_ <;> linarith
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (setOf Nat.Prime).indicator fun (n : ℕ) ↦ log (↑n : ℝ)
z : ℝ
h : z ∈ Set.Icc 2 x
left : 2 ≤ z
right : z ≤ x
this_1 : z ≠ 0
this : HPow.hPow (β := ℕ) (log z) 2 ≠ 0
funProp funProp₁ : z ≠ 0
funProp₂ : HPow.hPow (β := ℕ) (log z) 2 ≠ 0
⊢ ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ -x⁻¹ / HPow.hPow (β := ℕ) (log x) 2) z

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (setOf Nat.Prime).indicator fun (n : ℕ) ↦ log (↑n : ℝ)
z : ℝ
h : z ∈ Set.Icc 2 x
left : 2 ≤ z
right : z ≤ x
this_1 : z ≠ 0
this : HPow.hPow (β := ℕ) (log z) 2 ≠ 0
⊢ ContinuousWithinAt (Y := ℝ) (fun (x : ℝ) ↦ -x⁻¹ / HPow.hPow (β := ℕ) (log x) 2) (Set.Icc 2 x) z

Tactic:
exact ContinuousAt.continuousWithinAt <| by fun_prop

Premises used: ContinuousAt.continuousWithinAt
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 2 ≤ x
rw :
  (∑ a ∈ Icc 0 ⌊x⌋₊, if Nat.Prime a then log (↑a : ℝ) else 0) =
    (↑(π ⌊x⌋₊) : ℝ) * log x - ∫ (t : ℝ) in 2..x, (↑(π ⌊t⌋₊) : ℝ) / t
⊢ θ x = (↑(π ⌊x⌋₊) : ℝ) * log x - ∫ (t : ℝ) in 2..x, (↑(π ⌊t⌋₊) : ℝ) / t

Tactic:
rw [theta_eq_sum_Icc, sum_filter]

Premises used: Chebyshev.theta_eq_sum_Icc, Finset.sum_filter
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (setOf Nat.Prime).indicator fun (n : ℕ) ↦ 1
trans : Eq (α := ℝ) (∑ a ∈ Icc 0 ⌊x⌋₊, if Nat.Prime a then log (↑a : ℝ) 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
⊢ (∑ a ∈ Icc 0 ⌊x⌋₊, if Nat.Prime a then log (↑a : ℝ) else 0) =
    (↑(π ⌊x⌋₊) : ℝ) * log x - ∫ (t : ℝ) in 2..x, (↑(π ⌊t⌋₊) : ℝ) / t

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 : ℕ) ↦ 1
⊢ Eq (α := ℝ) (∑ a ∈ Icc 0 ⌊x⌋₊, if Nat.Prime a then log (↑a : ℝ) else 0) (∑ n ∈ Icc 0 ⌊x⌋₊, log (↑n : ℝ) * a n)

Tactic:
sum_congr rfl fun n _ ↦ ?_

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

Tactic:
refine sum_congr rfl fun n _ ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (setOf Nat.Prime).indicator fun (n : ℕ) ↦ 1
n : ℕ
h : n ∈ Icc 0 ⌊x⌋₊
pos : ∀ (h : Nat.Prime n), log (↑n : ℝ) = log (↑n : ℝ) * a n
neg : ∀ (h : ¬Nat.Prime n), 0 = log (↑n : ℝ) * a n
⊢ (if Nat.Prime n then log (↑n : ℝ) 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 : ℕ) ↦ 1
n : ℕ
h_1 : n ∈ Icc 0 ⌊x⌋₊
h : Nat.Prime n
⊢ log (↑n : ℝ) = log (↑n : ℝ) * a n

Tactic:
simp [a, h]
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (setOf Nat.Prime).indicator fun (n : ℕ) ↦ 1
n : ℕ
h_1 : 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 : ℕ) ↦ 1
⊢ a 0 = 0

Tactic:
simp [a, not_prime_zero]

Premises used: Nat.not_prime_zero
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (setOf Nat.Prime).indicator fun (n : ℕ) ↦ 1
⊢ a 1 = 0

Tactic:
simp [a, not_prime_one]

Premises used: Nat.not_prime_one
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (setOf Nat.Prime).indicator fun (n : ℕ) ↦ 1
z : ℝ
h : z ∈ Set.Icc 2 x
hz : 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 : ℕ) ↦ 1
z : ℝ
h : z ∈ Set.Icc 2 x
hz : 2 ≤ z
right : z ≤ x
funProp : z ≠ 0
⊢ DifferentiableAt ℝ log z

Tactic:
fun_prop (disch := linarith)
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (setOf Nat.Prime).indicator fun (n : ℕ) ↦ 1
rw :
  log x * ∑ k ∈ Icc 0 ⌊x⌋₊, a k - ∫ (x : ℝ) in 2..x, deriv log x * ∑ k ∈ Icc 0 ⌊x⌋₊, a k =
    (↑(π ⌊x⌋₊) : ℝ) * log x - ∫ (t : ℝ) in 2..x, (↑(π ⌊t⌋₊) : ℝ) / t
rw₁ : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv log) (Set.Icc 2 x) volume
⊢ ∑ n ∈ Icc 0 ⌊x⌋₊, log (↑n : ℝ) * a n = (↑(π ⌊x⌋₊) : ℝ) * log x - ∫ (t : ℝ) in 2..x, (↑(π ⌊t⌋₊) : ℝ) / t

Tactic:
rw [sum_mul_eq_sub_integral_mul₁ a (by simp [a, not_prime_zero])
    (by simp [a, not_prime_one]) _ (fun z ⟨hz, _⟩ ↦ (by fun_prop (disch := linarith))) ?hint,
    ← 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 : ℕ) ↦ 1
rw : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) Inv.inv (Set.Icc 2 x) volume
⊢ IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv log) (Set.Icc 2 x) volume

Tactic:
rw [deriv_log']

Premises used: Real.deriv_log'
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (setOf Nat.Prime).indicator fun (n : ℕ) ↦ 1
⊢ IntegrableOn (mα := MeasureSpace.toMeasurableSpace) Inv.inv (Set.Icc 2 x) volume

Tactic:
ContinuousOn.integrableOn_Icc ?_

Premises used: ContinuousOn.integrableOn_Icc
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (setOf Nat.Prime).indicator fun (n : ℕ) ↦ 1
refine : ContinuousOn Inv.inv (Set.Icc 2 x)
⊢ IntegrableOn (mα := MeasureSpace.toMeasurableSpace) Inv.inv (Set.Icc 2 x) volume

Tactic:
refine ContinuousOn.integrableOn_Icc ?_

Premises used: ContinuousOn.integrableOn_Icc
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (setOf Nat.Prime).indicator fun (n : ℕ) ↦ 1
⊢ ∀ x_1 ∈ Set.Icc 2 x, x_1 ≠ 0

Tactic:
grind
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (setOf Nat.Prime).indicator fun (n : ℕ) ↦ 1
funProp : ∀ x_1 ∈ Set.Icc 2 x, x_1 ≠ 0
⊢ ContinuousOn Inv.inv (Set.Icc 2 x)

Tactic:
fun_prop (disch := grind)
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (setOf Nat.Prime).indicator fun (n : ℕ) ↦ 1
⊢ IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv log) (Set.Icc 2 x) volume

Tactic:
case hint =>
    rw [deriv_log']
    refine ContinuousOn.integrableOn_Icc ?_
    fun_prop (disch := grind)

Premises used: ContinuousOn.integrableOn_Icc, Real.deriv_log'
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (setOf Nat.Prime).indicator fun (n : ℕ) ↦ 1
simp :
  log x * ∑ k ∈ Icc 0 ⌊x⌋₊, a k - ∫ (x : ℝ) in 2..x, deriv log x * ∑ k ∈ Icc 0 ⌊x⌋₊, a k =
    (↑(#({x ∈ range (⌊x⌋₊ + 1) | Nat.Prime x})) : ℝ) * log x -
      ∫ (t : ℝ) in 2..x, (↑(#({x ∈ range (⌊t⌋₊ + 1) | Nat.Prime x})) : ℝ) / t
⊢ log x * ∑ k ∈ Icc 0 ⌊x⌋₊, a k - ∫ (x : ℝ) in 2..x, deriv log x * ∑ k ∈ Icc 0 ⌊x⌋₊, a k =
    (↑(π ⌊x⌋₊) : ℝ) * log x - ∫ (t : ℝ) in 2..x, (↑(π ⌊t⌋₊) : ℝ) / t

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
a : ℕ → ℝ := (setOf Nat.Prime).indicator fun (n : ℕ) ↦ 1
f : ℝ → ℝ
u : ℝ
h : u ∈ Set.uIcc 2 x
rw : u⁻¹ * f u = f u / u
rw₁ : f u * u⁻¹ = f u / u
rw₂ rw₃ : f u * u⁻¹ = f u * u⁻¹
⊢ deriv (fun (x : ℝ) ↦ log x) u * f u = f u / u

Tactic:
rw [deriv_log, mul_comm, div_eq_mul_inv]

Premises used: Real.deriv_log, div_eq_mul_inv, mul_comm
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (setOf Nat.Prime).indicator fun (n : ℕ) ↦ 1
⊢ ∀ (f : ℝ → ℝ), Eq (α := ℝ) (∫ (u : ℝ) in 2..x, deriv (fun (x : ℝ) ↦ log x) u * f u) (∫ (u : ℝ) in 2..x, f u / u)

Tactic:
have int_deriv (f : ℝ → ℝ) :
      ∫ u in 2..x, deriv (fun x ↦ log x) u * f u =
      ∫ u in 2..x, f u / u :=
    intervalIntegral.integral_congr fun u _ ↦ by rw [deriv_log, mul_comm, div_eq_mul_inv]
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (setOf Nat.Prime).indicator fun (n : ℕ) ↦ 1
int_deriv :
  ∀ (f : ℝ → ℝ), Eq (α := ℝ) (∫ (u : ℝ) in 2..x, deriv (fun (x : ℝ) ↦ log x) u * f u) (∫ (u : ℝ) in 2..x, f u / u)
rw :
  log x * ∑ k ∈ Icc 0 ⌊x⌋₊, a k - ∫ (u : ℝ) in 2..x, (∑ k ∈ Icc 0 ⌊u⌋₊, a k) / u =
    (↑(#({x ∈ range (⌊x⌋₊ + 1) | Nat.Prime x})) : ℝ) * log x -
      ∫ (t : ℝ) in 2..x, (↑(#({x ∈ range (⌊t⌋₊ + 1) | Nat.Prime x})) : ℝ) / t
⊢ log x * ∑ k ∈ Icc 0 ⌊x⌋₊, a k - ∫ (x : ℝ) in 2..x, deriv log x * ∑ k ∈ Icc 0 ⌊x⌋₊, a k =
    (↑(#({x ∈ range (⌊x⌋₊ + 1) | Nat.Prime x})) : ℝ) * log x -
      ∫ (t : ℝ) in 2..x, (↑(#({x ∈ range (⌊t⌋₊ + 1) | Nat.Prime x})) : ℝ) / t

Tactic:
rw [int_deriv]
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (setOf Nat.Prime).indicator fun (n : ℕ) ↦ 1
int_deriv :
  ∀ (f : ℝ → ℝ), Eq (α := ℝ) (∫ (u : ℝ) in 2..x, deriv (fun (x : ℝ) ↦ log x) u * f u) (∫ (u : ℝ) in 2..x, f u / u)
⊢ log x * ∑ k ∈ Icc 0 ⌊x⌋₊, a k - ∫ (u : ℝ) in 2..x, (∑ k ∈ Icc 0 ⌊u⌋₊, a k) / u =
    (↑(#({x ∈ range (⌊x⌋₊ + 1) | Nat.Prime x})) : ℝ) * log x -
      ∫ (t : ℝ) in 2..x, (↑(#({x ∈ range (⌊t⌋₊ + 1) | Nat.Prime x})) : ℝ) / t

Tactic:
simp [a, Set.indicator_apply, range_succ_eq_Icc_zero, mul_comm]

Premises used: Set.indicator_apply, Nat.range_succ_eq_Icc_zero, mul_comm
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
a b : ℝ
one_lt_a : 1 < a
one_lt_b : 1 < b
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ 1 / HPow.hPow (β := ℕ) (log x) 2) volume a b

Tactic:
ContinuousOn.intervalIntegrable fun x hx ↦ ContinuousAt.continuousWithinAt ?_

Premises used: ContinuousAt.continuousWithinAt, ContinuousOn.intervalIntegrable
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
a b : ℝ
one_lt_a : 1 < a
one_lt_b : 1 < b
refine : ∀ (x : ℝ) (hx : x ∈ Set.uIcc a b), ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ 1 / HPow.hPow (β := ℕ) (log x) 2) x
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ 1 / HPow.hPow (β := ℕ) (log x) 2) volume a b

Tactic:
refine ContinuousOn.intervalIntegrable fun x hx ↦ ContinuousAt.continuousWithinAt ?_

Premises used: ContinuousAt.continuousWithinAt, ContinuousOn.intervalIntegrable
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
a b : ℝ
one_lt_a : 1 < a
one_lt_b : 1 < b
x : ℝ
hx : x ∈ Set.uIcc a b
⊢ a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a

Tactic:
rw [Set.mem_uIcc] at hx

Premises used: Set.mem_uIcc
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
a b : ℝ
one_lt_a : 1 < a
one_lt_b : 1 < b
x : ℝ
hx : a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a
⊢ x ≠ 0

Tactic:
grind
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
a b : ℝ
one_lt_a : 1 < a
one_lt_b : 1 < b
x : ℝ
hx : a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a
⊢ x ≠ 0

Tactic:
have : x ≠ 0 := by grind
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
a b : ℝ
one_lt_a : 1 < a
one_lt_b : 1 < b
x : ℝ
hx : a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a
this : x ≠ 0
⊢ x ≠ 0 ∧ x ≠ 1 ∧ x ≠ -1

Tactic:
grind
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
a b : ℝ
one_lt_a : 1 < a
one_lt_b : 1 < b
x : ℝ
hx : a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a
this : x ≠ 0
⊢ HPow.hPow (β := ℕ) (log x) 2 ≠ 0

Tactic:
have : log x ^ 2 ≠ 0 := pow_ne_zero _ (log_ne_zero.mpr (by grind))
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
a b : ℝ
one_lt_a : 1 < a
one_lt_b : 1 < b
x : ℝ
hx : a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a
this_1 : x ≠ 0
this : HPow.hPow (β := ℕ) (log x) 2 ≠ 0
funProp : x ≠ 0
funProp₁ : HPow.hPow (β := ℕ) (log x) 2 ≠ 0
⊢ ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ 1 / HPow.hPow (β := ℕ) (log x) 2) x

Tactic:
fun_prop
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
a b : ℝ
hab : a ≤ b
one_lt : 1 < a
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ 1 / HPow.hPow (β := ℕ) (log a) 2) volume a b

Tactic:
simp
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
a b : ℝ
hab : a ≤ b
one_lt : 1 < a
x : ℝ
h : x ∈ Set.Icc a b
left : a ≤ x
right : x ≤ b
hd : 0 < HPow.hPow (β := ℕ) (log a) 2
hdb : 0 ≤ log a
⊢ 1 / HPow.hPow (β := ℕ) (log x) 2 ≤ 1 / HPow.hPow (β := ℕ) (log a) 2

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
a b : ℝ
hab : a ≤ b
one_lt : 1 < a
x : ℝ
h : x ∈ Set.Icc a b
left : a ≤ x
right : x ≤ b
⊢ 0 < HPow.hPow (β := ℕ) (log a) 2

Tactic:
bound
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
a b : ℝ
hab : a ≤ b
one_lt : 1 < a
x : ℝ
h : x ∈ Set.Icc a b
left : a ≤ x
right : x ≤ b
⊢ 0 ≤ log a

Tactic:
bound
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
a b : ℝ
hab : a ≤ b
one_lt : 1 < a
refine : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ 1 / HPow.hPow (β := ℕ) (log x) 2) volume a b
⊢ LE.le (α := ℝ) (∫ (x : ℝ) in a..b, 1 / HPow.hPow (β := ℕ) (log x) 2)
    (∫ (x : ℝ) in a..b, 1 / HPow.hPow (β := ℕ) (log a) 2)

Tactic:
refine intervalIntegral.integral_mono_on hab ?_ (by simp) fun x ⟨_, _⟩ ↦ by gcongr <;> bound

Premises used: intervalIntegral.integral_mono_on, LE.le, _private.0.Chebyshev.integral_1_div_log_sq_le.match_1
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
a b : ℝ
hab : a ≤ b
one_lt one_lt_a : 1 < a
one_lt_b : 1 < b
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ 1 / HPow.hPow (β := ℕ) (log x) 2) volume a b

Tactic:
apply intervalIntegrable_one_div_log_sq

Premises used: Chebyshev.intervalIntegrable_one_div_log_sq
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
a b : ℝ
hab : a ≤ b
one_lt : 1 < a
linarith : a ≤ 1 → 1 - a + (a - 1) = 0
⊢ 1 < a

Tactic:
linarith
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
a b : ℝ
hab : a ≤ b
one_lt : 1 < a
linarith : b ≤ 1 → a - b + (1 - a) + (b - 1) = 0
⊢ 1 < b

Tactic:
linarith
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
a b : ℝ
hab : a ≤ b
one_lt : 1 < a
⊢ ∫ (x : ℝ) in a..b, 1 / HPow.hPow (β := ℕ) (log a) 2 ≤ (b - a) / HPow.hPow (β := ℕ) (log a) 2

Tactic:
simp [field]
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
a b : ℝ
hab : a ≤ b
one_lt : 1 < a
_ :
  LE.le (α := ℝ) (∫ (x : ℝ) in a..b, 1 / HPow.hPow (β := ℕ) (log x) 2)
    (∫ (x : ℝ) in a..b, 1 / HPow.hPow (β := ℕ) (log a) 2)
_₁ : ∫ (x : ℝ) in a..b, 1 / HPow.hPow (β := ℕ) (log a) 2 ≤ (b - a) / HPow.hPow (β := ℕ) (log a) 2
⊢ ∫ (x : ℝ) in a..b, 1 / HPow.hPow (β := ℕ) (log x) 2 ≤ (b - a) / HPow.hPow (β := ℕ) (log a) 2

Tactic:
calc
  _ ≤ ∫ x in a..b, 1 / log a ^ 2 := by
      refine intervalIntegral.integral_mono_on hab ?_ (by simp) fun x ⟨_, _⟩ ↦ by gcongr <;> bound
      apply intervalIntegrable_one_div_log_sq <;> linarith
  _ ≤ _ := by simp [field]

Premises used: Real.log
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 4 ≤ x
⊢ HPow.hPow (α := ℝ) (β := ℕ) 2 2 ≤ x

Tactic:
norm_num [hx]
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 4 ≤ x
⊢ 2 ≤ √x

Tactic:
have two_le_sqrt : 2 ≤ x.sqrt := le_sqrt_of_sq_le <| by norm_num [hx]
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
linarith : x < 0 → HMul.hMul (α := ℝ) 4 (-1) + (4 - x) + (x - 0) = 0
linarith₁ : x < 0 → GT.gt (α := ℝ) 4 0
⊢ 0 ≤ x

Tactic:
linarith
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
⊢ x ≤ HPow.hPow (β := ℕ) x 2

Tactic:
bound
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
⊢ √x ≤ x

Tactic:
have sqrt_le_x : x.sqrt ≤ x := sqrt_le_left (by linarith) |>.mpr (by bound)
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
rw :
  HAdd.hAdd (α := ℝ) (∫ (x : ℝ) in 2..√x, 1 / HPow.hPow (β := ℕ) (log x) 2)
      (∫ (x : ℝ) in √x..x, 1 / HPow.hPow (β := ℕ) (log x) 2) ≤
    4 * x / HPow.hPow (β := ℕ) (log x) 2 + √x / HPow.hPow (β := ℕ) (log 2) 2
hab : IntervalIntegrable (ε := ℝ) (fun (t : ℝ) ↦ 1 / HPow.hPow (β := ℕ) (log t) 2) volume 2 √x
hbc : IntervalIntegrable (ε := ℝ) (fun (t : ℝ) ↦ 1 / HPow.hPow (β := ℕ) (log t) 2) volume (√x) x
⊢ ∫ (t : ℝ) in 2..x, 1 / HPow.hPow (β := ℕ) (log t) 2 ≤
    4 * x / HPow.hPow (β := ℕ) (log x) 2 + √x / HPow.hPow (β := ℕ) (log 2) 2

Tactic:
rw [← intervalIntegral.integral_add_adjacent_intervals (b := x.sqrt)]

Premises used: intervalIntegral.integral_add_adjacent_intervals
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
linarith : LE.le (α := ℝ) 2 1 → -1 + HSub.hSub (α := ℝ) 2 1 = 0
⊢ LT.lt (α := ℝ) 1 2

Tactic:
linarith
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
linarith : √x ≤ 1 → -1 + (2 - √x) + (√x - 1) = 0
⊢ 1 < √x

Tactic:
linarith
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
grw :
  (√x - 2) / HPow.hPow (β := ℕ) (log 2) 2 + (x - √x) / HPow.hPow (β := ℕ) (log √x) 2 ≤
    4 * x / HPow.hPow (β := ℕ) (log x) 2 + √x / HPow.hPow (β := ℕ) (log 2) 2
⊢ HAdd.hAdd (α := ℝ) (∫ (x : ℝ) in 2..√x, 1 / HPow.hPow (β := ℕ) (log x) 2)
      (∫ (x : ℝ) in √x..x, 1 / HPow.hPow (β := ℕ) (log x) 2) ≤
    4 * x / HPow.hPow (β := ℕ) (log x) 2 + √x / HPow.hPow (β := ℕ) (log 2) 2

Tactic:
grw [integral_1_div_log_sq_le two_le_sqrt (by linarith),
      integral_1_div_log_sq_le sqrt_le_x (by linarith)]

Premises used: _private.0.Chebyshev.integral_1_div_log_sq_le
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
linarith : x < 0 → HMul.hMul (α := ℝ) 4 (-1) + (4 - x) + (x - 0) = 0
linarith₁ : x < 0 → GT.gt (α := ℝ) 4 0
⊢ 0 ≤ x

Tactic:
linarith
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
rw :
  HPow.hPow (α := ℝ) (β := ℕ) 2 2 * ((x - √x) / HPow.hPow (β := ℕ) (log x) 2) +
      (√x - 2) / HPow.hPow (β := ℕ) (log 2) 2 ≤
    4 * (x / HPow.hPow (β := ℕ) (log x) 2) + √x / HPow.hPow (β := ℕ) (log 2) 2
⊢ (√x - 2) / HPow.hPow (β := ℕ) (log 2) 2 + (x - √x) / HPow.hPow (β := ℕ) (log √x) 2 ≤
    4 * x / HPow.hPow (β := ℕ) (log x) 2 + √x / HPow.hPow (β := ℕ) (log 2) 2

Tactic:
rw [log_sqrt (by linarith), add_comm, div_pow, ← div_mul, mul_comm, mul_div_assoc]

Premises used: Real.log_sqrt, mul_div_assoc, div_mul, add_comm, div_pow, mul_comm
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
norm_num :
  4 * ((x - √x) / HPow.hPow (β := ℕ) (log x) 2) + (√x - 2) / HPow.hPow (β := ℕ) (log 2) 2 ≤
    4 * (x / HPow.hPow (β := ℕ) (log x) 2) + √x / HPow.hPow (β := ℕ) (log 2) 2
⊢ HPow.hPow (α := ℝ) (β := ℕ) 2 2 * ((x - √x) / HPow.hPow (β := ℕ) (log x) 2) +
      (√x - 2) / HPow.hPow (β := ℕ) (log 2) 2 ≤
    4 * (x / HPow.hPow (β := ℕ) (log x) 2) + √x / HPow.hPow (β := ℕ) (log 2) 2

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
h₁ : x - √x ≤ x
h₂ : √x - 2 ≤ √x
⊢ 4 * ((x - √x) / HPow.hPow (β := ℕ) (log x) 2) + (√x - 2) / HPow.hPow (β := ℕ) (log 2) 2 ≤
    4 * (x / HPow.hPow (β := ℕ) (log x) 2) + √x / HPow.hPow (β := ℕ) (log 2) 2

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
linarith : x < x - √x → HMul.hMul (α := ℝ) 2 (-1) + (2 - √x) + (x - (x - √x)) = 0
linarith₁ : x < x - √x → GT.gt (α := ℝ) 2 0
⊢ x - √x ≤ x

Tactic:
linarith
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
sqrt_le_x : √x ≤ x
linarith : √x < √x - 2 → HMul.hMul (α := ℝ) 2 (-1) + (√x - (√x - 2)) = 0
linarith₁ : √x < √x - 2 → GT.gt (α := ℝ) 2 0
⊢ √x - 2 ≤ √x

Tactic:
linarith