awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
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)
⊢ ∑ n ∈ Icc 0 ⌊x⌋₊, (log (↑n : ℝ))⁻¹ * a n = θ x / log x + ∫ (t : ℝ) in 2..x, θ t / (t * HPow.hPow (β := ℕ) (log t) 2)
have hf_diff : ∀ t ∈ Set.Icc 2 x, DifferentiableAt ℝ (F := ℝ) (fun (n : ℝ) ↦ (log n)⁻¹) t
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]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
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
⊢ ∑ n ∈ Icc 0 ⌊x⌋₊, (log (↑n : ℝ))⁻¹ * a n = θ x / log x + ∫ (t : ℝ) in 2..x, θ t / (t * HPow.hPow (β := ℕ) (log t) 2)
have hf_int : IntegrableOn (ε := ℝ) (mα := MeasureSpace.toMeasurableSpace) (deriv fun (n : ℝ) ↦ (log n)⁻¹) (Set.Icc 2 x) volume
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]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (hypothesis)
Goal:
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (setOf Nat.Prime).indicator fun (n : ℕ) ↦ log (↑n : ℝ)
⊢ (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)
have 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)⁻¹)
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]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
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)⁻¹ * ∑ 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)
have 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)
Tactic: simp [int_deriv, a, Set.indicator_apply, sum_filter, theta_eq_sum_Icc]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (setOf Nat.Prime).indicator fun (n : ℕ) ↦ log (↑n : ℝ)
z : ℝ
⊢ z ∈ Set.Icc 2 x → DifferentiableAt ℝ (F := ℝ) (fun (n : ℝ) ↦ (log n)⁻¹) z
have hf_diff : 2 ≤ z → z ≤ x → DifferentiableAt ℝ (F := ℝ) (fun (n : ℝ) ↦ (log n)⁻¹) z
Tactic: ⟨_, _⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (setOf Nat.Prime).indicator fun (n : ℕ) ↦ log (↑n : ℝ)
z : ℝ
left : 2 ≤ z
right : z ≤ x
⊢ z ≠ 0
have linarith : z = 0 → HMul.hMul (α := ℝ) 2 (-1) + (2 - z) + (z - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
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
⊢ z ≠ 0
have linarith₁ : z = 0 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (hypothesis)
Goal:
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (setOf Nat.Prime).indicator fun (n : ℕ) ↦ log (↑n : ℝ)
z : ℝ
left : 2 ≤ z
right : z ≤ x
⊢ DifferentiableAt ℝ (F := ℝ) (fun (n : ℝ) ↦ (log n)⁻¹) z
have this : z ≠ 0
Tactic: have : z ≠ 0 := by linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
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
have hx_pos : 0 < z
Tactic: apply log_ne_zero_of_pos_of_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 : ℝ)
z : ℝ
left : 2 ≤ z
right : z ≤ x
this : z ≠ 0
hx_pos : 0 < z
⊢ log z ≠ 0
have hx₁ : z ≠ 1
Tactic: apply log_ne_zero_of_pos_of_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 : ℝ)
z : ℝ
left : 2 ≤ z
right : z ≤ x
this : z ≠ 0
⊢ 0 < z
have linarith : z ≤ 0 → HMul.hMul (α := ℝ) 2 (-1) + (2 - z) + (z - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
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
⊢ 0 < z
have linarith₁ : z ≤ 0 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (setOf Nat.Prime).indicator fun (n : ℕ) ↦ log (↑n : ℝ)
z : ℝ
left : 2 ≤ z
right : z ≤ x
this : z ≠ 0
⊢ z ≠ 1
have linarith : z = 1 → -1 + (2 - z) + (z - 1) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (hypothesis)
Goal:
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (setOf Nat.Prime).indicator fun (n : ℕ) ↦ log (↑n : ℝ)
z : ℝ
left : 2 ≤ z
right : z ≤ x
this : z ≠ 0
⊢ DifferentiableAt ℝ (F := ℝ) (fun (n : ℝ) ↦ (log n)⁻¹) z
have this₁ : log z ≠ 0
Tactic: have : log z ≠ 0 := by apply log_ne_zero_of_pos_of_ne_one <;> linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
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
have 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
Tactic: refine ContinuousOn.integrableOn_Icc fun z ⟨_, _⟩ ↦ ContinuousWithinAt.congr ?_
      (fun _ _ ↦ deriv_inv_log) deriv_inv_log
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
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
have linarith : z = 0 → HMul.hMul (α := ℝ) 2 (-1) + (2 - z) + (z - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
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
⊢ z ≠ 0
have linarith₁ : z = 0 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (hypothesis)
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
⊢ ContinuousWithinAt (Y := ℝ) (fun (x : ℝ) ↦ -x⁻¹ / HPow.hPow (β := ℕ) (log x) 2) (Set.Icc 2 x) z
have this : z ≠ 0
Tactic: have : z ≠ 0 := by linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
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
have refine_1 : 0 < z
Tactic: refine pow_ne_zero 2 <| log_ne_zero_of_pos_of_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 : ℝ)
z : ℝ
h : z ∈ Set.Icc 2 x
left : 2 ≤ z
right : z ≤ x
this : z ≠ 0
refine_1 : 0 < z
⊢ HPow.hPow (β := ℕ) (log z) 2 ≠ 0
have refine_2 : z ≠ 1
Tactic: refine pow_ne_zero 2 <| log_ne_zero_of_pos_of_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 : ℝ)
z : ℝ
h : z ∈ Set.Icc 2 x
left : 2 ≤ z
right : z ≤ x
this : z ≠ 0
⊢ 0 < z
have linarith : z ≤ 0 → HMul.hMul (α := ℝ) 2 (-1) + (2 - z) + (z - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
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
⊢ 0 < z
have linarith₁ : z ≤ 0 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
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
⊢ z ≠ 1
have linarith : z = 1 → -1 + (2 - z) + (z - 1) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (hypothesis)
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
⊢ ContinuousWithinAt (Y := ℝ) (fun (x : ℝ) ↦ -x⁻¹ / HPow.hPow (β := ℕ) (log x) 2) (Set.Icc 2 x) z
have this₁ : 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
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 2 ≤ x
⊢ θ x = (↑(π ⌊x⌋₊) : ℝ) * log x - ∫ (t : ℝ) in 2..x, (↑(π ⌊t⌋₊) : ℝ) / t
have rw : (∑ a ∈ Icc 0 ⌊x⌋₊, if Nat.Prime a then log (↑a : ℝ) else 0) =
  (↑(π ⌊x⌋₊) : ℝ) * log x - ∫ (t : ℝ) in 2..x, (↑(π ⌊t⌋₊) : ℝ) / t
Tactic: rw [theta_eq_sum_Icc, sum_filter]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (setOf Nat.Prime).indicator fun (n : ℕ) ↦ 1
⊢ (∑ a ∈ Icc 0 ⌊x⌋₊, if Nat.Prime a then log (↑a : ℝ) else 0) =
    (↑(π ⌊x⌋₊) : ℝ) * log x - ∫ (t : ℝ) in 2..x, (↑(π ⌊t⌋₊) : ℝ) / t
have trans : Eq (α := ℝ) (∑ a ∈ Icc 0 ⌊x⌋₊, if Nat.Prime a then log (↑a : ℝ) 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 : ℕ) ↦ 1
trans : Eq (α := ℝ) (∑ a ∈ Icc 0 ⌊x⌋₊, if Nat.Prime a then log (↑a : ℝ) else 0) (∑ n ∈ Icc 0 ⌊x⌋₊, log (↑n : ℝ) * a n)
⊢ (∑ a ∈ Icc 0 ⌊x⌋₊, if Nat.Prime a then log (↑a : ℝ) else 0) =
    (↑(π ⌊x⌋₊) : ℝ) * log x - ∫ (t : ℝ) in 2..x, (↑(π ⌊t⌋₊) : ℝ) / t
have trans₁ : ∑ n ∈ Icc 0 ⌊x⌋₊, log (↑n : ℝ) * a n = (↑(π ⌊x⌋₊) : ℝ) * log x - ∫ (t : ℝ) in 2..x, (↑(π ⌊t⌋₊) : ℝ) / t
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 : ℕ) ↦ 1
⊢ Eq (α := ℝ) (∑ a ∈ Icc 0 ⌊x⌋₊, if Nat.Prime a then log (↑a : ℝ) else 0) (∑ n ∈ Icc 0 ⌊x⌋₊, log (↑n : ℝ) * a n)
have refine : ∀ n ∈ Icc 0 ⌊x⌋₊, (if Nat.Prime n then log (↑n : ℝ) else 0) = log (↑n : ℝ) * a n
Tactic: refine sum_congr rfl fun n _ ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (setOf Nat.Prime).indicator fun (n : ℕ) ↦ 1
n : ℕ
h : n ∈ Icc 0 ⌊x⌋₊
⊢ (if Nat.Prime n then log (↑n : ℝ) else 0) = log (↑n : ℝ) * a n
have pos : ∀ (h : Nat.Prime n), log (↑n : ℝ) = 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 : ℕ) ↦ 1
n : ℕ
h : n ∈ Icc 0 ⌊x⌋₊
pos : ∀ (h : Nat.Prime n), log (↑n : ℝ) = log (↑n : ℝ) * a n
⊢ (if Nat.Prime n then log (↑n : ℝ) 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 (goal)
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
⊢ z ≠ 0
have linarith : z = 0 → HMul.hMul (α := ℝ) 2 (-1) + (2 - z) + (z - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
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
⊢ z ≠ 0
have linarith₁ : z = 0 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
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
⊢ DifferentiableAt ℝ log z
have funProp : z ≠ 0
Tactic: fun_prop (disch := linarith)
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (setOf Nat.Prime).indicator fun (n : ℕ) ↦ 1
⊢ ∑ n ∈ Icc 0 ⌊x⌋₊, log (↑n : ℝ) * a n = (↑(π ⌊x⌋₊) : ℝ) * log x - ∫ (t : ℝ) in 2..x, (↑(π ⌊t⌋₊) : ℝ) / t
have 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
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]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
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
⊢ ∑ n ∈ Icc 0 ⌊x⌋₊, log (↑n : ℝ) * a n = (↑(π ⌊x⌋₊) : ℝ) * log x - ∫ (t : ℝ) in 2..x, (↑(π ⌊t⌋₊) : ℝ) / t
have rw₁ : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv log) (Set.Icc 2 x) volume
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]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (setOf Nat.Prime).indicator fun (n : ℕ) ↦ 1
⊢ IntegrableOn (mα := MeasureSpace.toMeasurableSpace) (deriv log) (Set.Icc 2 x) volume
have rw : IntegrableOn (mα := MeasureSpace.toMeasurableSpace) Inv.inv (Set.Icc 2 x) volume
Tactic: rw [deriv_log']
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (setOf Nat.Prime).indicator fun (n : ℕ) ↦ 1
⊢ IntegrableOn (mα := MeasureSpace.toMeasurableSpace) Inv.inv (Set.Icc 2 x) volume
have refine : ContinuousOn Inv.inv (Set.Icc 2 x)
Tactic: refine ContinuousOn.integrableOn_Icc ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (setOf Nat.Prime).indicator fun (n : ℕ) ↦ 1
⊢ ContinuousOn Inv.inv (Set.Icc 2 x)
have funProp : ∀ x_1 ∈ Set.Icc 2 x, x_1 ≠ 0
Tactic: fun_prop (disch := grind)
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (setOf Nat.Prime).indicator fun (n : ℕ) ↦ 1
⊢ 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
have 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
Tactic: simp only [primeCounting, primeCounting', count_eq_card_filter_range]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (setOf Nat.Prime).indicator fun (n : ℕ) ↦ 1
f : ℝ → ℝ
u : ℝ
h : u ∈ Set.uIcc 2 x
⊢ deriv (fun (x : ℝ) ↦ log x) u * f u = f u / u
have rw : u⁻¹ * f u = f u / u
Tactic: rw [deriv_log, mul_comm, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
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
⊢ deriv (fun (x : ℝ) ↦ log x) u * f u = f u / u
have rw₁ : f u * u⁻¹ = f u / u
Tactic: rw [deriv_log, mul_comm, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
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
⊢ deriv (fun (x : ℝ) ↦ log x) u * f u = f u / u
have rw₂ : f u * u⁻¹ = f u * u⁻¹
Tactic: rw [deriv_log, mul_comm, div_eq_mul_inv]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (hypothesis)
Goal:
x : ℝ
hx : 2 ≤ x
a : ℕ → ℝ := (setOf Nat.Prime).indicator fun (n : ℕ) ↦ 1
⊢ 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
have int_deriv : ∀ (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]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
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 - ∫ (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
have 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
Tactic: rw [int_deriv]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
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
have refine : ∀ (x : ℝ) (hx : x ∈ Set.uIcc a b), ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ 1 / HPow.hPow (β := ℕ) (log x) 2) x
Tactic: refine ContinuousOn.intervalIntegrable fun x hx ↦ ContinuousAt.continuousWithinAt ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (hypothesis)
Goal:
a b : ℝ
one_lt_a : 1 < a
one_lt_b : 1 < b
x : ℝ
hx : x ∈ Set.uIcc a b
⊢ ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ 1 / HPow.hPow (β := ℕ) (log x) 2) x
have hx₁ : a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a
Tactic: rw [Set.mem_uIcc] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (hypothesis)
Goal:
a b : ℝ
one_lt_a : 1 < a
one_lt_b : 1 < b
x : ℝ
hx : a ≤ x ∧ x ≤ b ∨ b ≤ x ∧ x ≤ a
⊢ ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ 1 / HPow.hPow (β := ℕ) (log x) 2) x
have this : x ≠ 0
Tactic: have : x ≠ 0 := by grind
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (hypothesis)
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
⊢ ContinuousAt (Y := ℝ) (fun (x : ℝ) ↦ 1 / HPow.hPow (β := ℕ) (log x) 2) x
have this₁ : HPow.hPow (β := ℕ) (log x) 2 ≠ 0
Tactic: have : log x ^ 2 ≠ 0 := pow_ne_zero _ (log_ne_zero.mpr (by grind))
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
a b : ℝ
hab : a ≤ b
one_lt : 1 < a
x : ℝ
h : x ∈ Set.Icc a b
left : a ≤ x
right : x ≤ b
⊢ 1 / HPow.hPow (β := ℕ) (log x) 2 ≤ 1 / HPow.hPow (β := ℕ) (log a) 2
have hd : 0 < HPow.hPow (β := ℕ) (log a) 2
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
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
⊢ 1 / HPow.hPow (β := ℕ) (log x) 2 ≤ 1 / HPow.hPow (β := ℕ) (log a) 2
have hdb : 0 ≤ log a
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
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)
have refine : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ 1 / HPow.hPow (β := ℕ) (log x) 2) volume a b
Tactic: refine intervalIntegral.integral_mono_on hab ?_ (by simp) fun x ⟨_, _⟩ ↦ by gcongr <;> bound
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
a b : ℝ
hab : a ≤ b
one_lt one_lt_a : 1 < a
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ 1 / HPow.hPow (β := ℕ) (log x) 2) volume a b
have one_lt_b : 1 < b
Tactic: apply intervalIntegrable_one_div_log_sq
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
a b : ℝ
hab : a ≤ b
one_lt : 1 < a
⊢ 1 < a
have linarith : a ≤ 1 → 1 - a + (a - 1) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
a b : ℝ
hab : a ≤ b
one_lt : 1 < a
⊢ 1 < b
have linarith : b ≤ 1 → a - b + (1 - a) + (b - 1) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
a b : ℝ
hab : a ≤ b
one_lt : 1 < a
⊢ ∫ (x : ℝ) in a..b, 1 / HPow.hPow (β := ℕ) (log x) 2 ≤ (b - a) / HPow.hPow (β := ℕ) (log a) 2
have _ : LE.le (α := ℝ) (∫ (x : ℝ) in a..b, 1 / HPow.hPow (β := ℕ) (log x) 2)
  (∫ (x : ℝ) in a..b, 1 / 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]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
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 x) 2 ≤ (b - a) / HPow.hPow (β := ℕ) (log a) 2
have _₁ : ∫ (x : ℝ) in a..b, 1 / HPow.hPow (β := ℕ) (log a) 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]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (hypothesis)
Goal:
x : ℝ
hx : 4 ≤ x
⊢ ∫ (t : ℝ) in 2..x, 1 / HPow.hPow (β := ℕ) (log t) 2 ≤
    4 * x / HPow.hPow (β := ℕ) (log x) 2 + √x / HPow.hPow (β := ℕ) (log 2) 2
have two_le_sqrt : 2 ≤ √x
Tactic: have two_le_sqrt : 2 ≤ x.sqrt := le_sqrt_of_sq_le <| by norm_num [hx]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
⊢ 0 ≤ x
have linarith : x < 0 → HMul.hMul (α := ℝ) 4 (-1) + (4 - x) + (x - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
linarith : x < 0 → HMul.hMul (α := ℝ) 4 (-1) + (4 - x) + (x - 0) = 0
⊢ 0 ≤ x
have linarith₁ : x < 0 → GT.gt (α := ℝ) 4 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (hypothesis)
Goal:
x : ℝ
hx : 4 ≤ x
two_le_sqrt : 2 ≤ √x
⊢ ∫ (t : ℝ) in 2..x, 1 / HPow.hPow (β := ℕ) (log t) 2 ≤
    4 * x / HPow.hPow (β := ℕ) (log x) 2 + √x / HPow.hPow (β := ℕ) (log 2) 2
have sqrt_le_x : √x ≤ x
Tactic: have sqrt_le_x : x.sqrt ≤ x := sqrt_le_left (by linarith) |>.mpr (by bound)