awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
R : Type u_1
inst : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
p k : ℕ
hp : _root_.Prime p
hk₀ : 0 < k
h : 0 < p ^ k
hbx : HPow.hPow (α := ℝ) (↑p : ℝ) k ≤ x
⊢ (↑p : ℝ) ≤ HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹

Tactic:
simp_all [le_rpow_inv_iff_of_pos]

Premises used: Real.le_rpow_inv_iff_of_pos
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
R : Type u_1
inst : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
⊢ ∀ (a : ℕ × ℕ)
    (ha :
      a ∈
        {x_1 ∈ Icc 1 ⌊log x / log 2⌋₊ ×ˢ filter Nat.Prime (Ioc 0 ⌊x⌋₊) |
          match (motive := ℕ × ℕ → Prop) x_1 with
          | (k, p) => p ≤ ⌊HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹⌋₊}),
    (match (motive := ℕ × ℕ → R) a with
      | (k, p) => f (p ^ k)) =
      f
        ((fun (x_1 : ℕ × ℕ)
              (x_2 :
                x_1 ∈
                  {x_2 ∈ Icc 1 ⌊log x / log 2⌋₊ ×ˢ filter Nat.Prime (Ioc 0 ⌊x⌋₊) |
                    match (motive := ℕ × ℕ → Prop) x_2 with
                    | (k, p) => p ≤ ⌊HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹⌋₊}) ↦
            (match (motive :=
                (x_3 : ℕ × ℕ) →
                  x_3 ∈
                      {x_4 ∈ Icc 1 ⌊log x / log 2⌋₊ ×ˢ filter Nat.Prime (Ioc 0 ⌊x⌋₊) |
                        match (motive := ℕ × ℕ → Prop) x_4 with
                        | (k, p) => p ≤ ⌊HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹⌋₊} →
                    ℕ)
                x_1, x_2 with
              | (k, p), x => p ^ k :
              ℕ))
          a ha)

Tactic:
simp
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
R : Type u_1
inst : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
rw :
  Eq.{u_1 + 1} (α := R)
    (∑ x_1 ∈ Icc 1 ⌊log x / log 2⌋₊,
      ∑ y ∈ Ioc 0 ⌊x⌋₊ with Nat.Prime y,
        if
            match (motive := ℕ × ℕ → Prop) (x_1, y) with
            | (k, p) => p ≤ ⌊HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹⌋₊ then
          match (motive := ℕ × ℕ → R) (x_1, y) with
          | (k, p) => f (p ^ k)
        else 0)
    (∑ k ∈ Icc 1 ⌊log x / log 2⌋₊, ∑ p ∈ Ioc 0 ⌊x ^ HDiv.hDiv (α := ℝ) 1 (↑k : ℝ)⌋₊ with Nat.Prime p, f (p ^ k))
⊢ Eq.{u_1 + 1} (α := R)
    (∑ x ∈ Icc 1 ⌊log x / log 2⌋₊ ×ˢ filter Nat.Prime (Ioc 0 ⌊x⌋₊) with
      match (motive := ℕ × ℕ → Prop) x with
      | (k, p) => p ≤ ⌊HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹⌋₊,
      match (motive := ℕ × ℕ → R) x with
      | (k, p) => f (p ^ k))
    (∑ k ∈ Icc 1 ⌊log x / log 2⌋₊, ∑ p ∈ Ioc 0 ⌊x ^ HDiv.hDiv (α := ℝ) 1 (↑k : ℝ)⌋₊ with Nat.Prime p, f (p ^ k))

Tactic:
rw [sum_filter, sum_product]

Premises used: Finset.sum_filter, Finset.sum_product
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
R : Type u_1
inst : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
⊢ Eq.{u_1 + 1} (α := R)
    (∑ x_1 ∈ Icc 1 ⌊log x / log 2⌋₊,
      ∑ y ∈ Ioc 0 ⌊x⌋₊ with Nat.Prime y,
        if
            match (motive := ℕ × ℕ → Prop) (x_1, y) with
            | (k, p) => p ≤ ⌊HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹⌋₊ then
          match (motive := ℕ × ℕ → R) (x_1, y) with
          | (k, p) => f (p ^ k)
        else 0)
    (∑ k ∈ Icc 1 ⌊log x / log 2⌋₊, ∑ p ∈ Ioc 0 ⌊x ^ HDiv.hDiv (α := ℝ) 1 (↑k : ℝ)⌋₊ with Nat.Prime p, f (p ^ k))

Tactic:
sum_congr rfl fun k _ ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
R : Type u_1
inst : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
refine :
  ∀ k ∈ Icc 1 ⌊log x / log 2⌋₊,
    Eq.{u_1 + 1} (α := R)
      (∑ y ∈ Ioc 0 ⌊x⌋₊ with Nat.Prime y,
        if
            match (motive := ℕ × ℕ → Prop) (k, y) with
            | (k, p) => p ≤ ⌊HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹⌋₊ then
          match (motive := ℕ × ℕ → R) (k, y) with
          | (k, p) => f (p ^ k)
        else 0)
      (∑ p ∈ Ioc 0 ⌊x ^ HDiv.hDiv (α := ℝ) 1 (↑k : ℝ)⌋₊ with Nat.Prime p, f (p ^ k))
⊢ Eq.{u_1 + 1} (α := R)
    (∑ x_1 ∈ Icc 1 ⌊log x / log 2⌋₊,
      ∑ y ∈ Ioc 0 ⌊x⌋₊ with Nat.Prime y,
        if
            match (motive := ℕ × ℕ → Prop) (x_1, y) with
            | (k, p) => p ≤ ⌊HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹⌋₊ then
          match (motive := ℕ × ℕ → R) (x_1, y) with
          | (k, p) => f (p ^ k)
        else 0)
    (∑ k ∈ Icc 1 ⌊log x / log 2⌋₊, ∑ p ∈ Ioc 0 ⌊x ^ HDiv.hDiv (α := ℝ) 1 (↑k : ℝ)⌋₊ with Nat.Prime p, f (p ^ k))

Tactic:
refine sum_congr rfl fun k _ ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
R : Type u_1
inst : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
k : ℕ
h : k ∈ Icc 1 ⌊log x / log 2⌋₊
simp :
  Eq.{u_1 + 1} (α := R) (∑ x ∈ filter Nat.Prime (Ioc 0 ⌊x⌋₊) with x ≤ ⌊HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹⌋₊, f (x ^ k))
    (∑ x ∈ Ioc 0 ⌊x ^ HDiv.hDiv (α := ℝ) 1 (↑k : ℝ)⌋₊ with Nat.Prime x, f (x ^ k))
⊢ Eq.{u_1 + 1} (α := R)
    (∑ y ∈ Ioc 0 ⌊x⌋₊ with Nat.Prime y,
      if
          match (motive := ℕ × ℕ → Prop) (k, y) with
          | (k, p) => p ≤ ⌊HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹⌋₊ then
        match (motive := ℕ × ℕ → R) (k, y) with
        | (k, p) => f (p ^ k)
      else 0)
    (∑ p ∈ Ioc 0 ⌊x ^ HDiv.hDiv (α := ℝ) 1 (↑k : ℝ)⌋₊ with Nat.Prime p, f (p ^ k))

Tactic:
simp only [sum_ite, not_le, sum_const_zero, add_zero]

Premises used: not_le, Finset.sum_const_zero, add_zero, Finset.sum_ite
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
R : Type u_1
inst : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
k : ℕ
h : k ∈ Icc 1 ⌊log x / log 2⌋₊
e_s :
  {x_1 ∈ filter Nat.Prime (Ioc 0 ⌊x⌋₊) | x_1 ≤ ⌊HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹⌋₊} =
    {p ∈ Ioc 0 ⌊x ^ HDiv.hDiv (α := ℝ) 1 (↑k : ℝ)⌋₊ | Nat.Prime p}
⊢ Eq.{u_1 + 1} (α := R) (∑ x ∈ filter Nat.Prime (Ioc 0 ⌊x⌋₊) with x ≤ ⌊HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹⌋₊, f (x ^ k))
    (∑ x ∈ Ioc 0 ⌊x ^ HDiv.hDiv (α := ℝ) 1 (↑k : ℝ)⌋₊ with Nat.Prime x, f (x ^ k))

Tactic:
congr 1
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
R : Type u_1
inst : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
k : ℕ
h : k ∈ Icc 1 ⌊log x / log 2⌋₊
e_s :
  ∀ (p : ℕ),
    p ∈ {x_1 ∈ filter Nat.Prime (Ioc 0 ⌊x⌋₊) | x_1 ≤ ⌊HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹⌋₊} ↔
      p ∈ {p ∈ Ioc 0 ⌊x ^ HDiv.hDiv (α := ℝ) 1 (↑k : ℝ)⌋₊ | Nat.Prime p}
⊢ {x_1 ∈ filter Nat.Prime (Ioc 0 ⌊x⌋₊) | x_1 ≤ ⌊HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹⌋₊} =
    {p ∈ Ioc 0 ⌊x ^ HDiv.hDiv (α := ℝ) 1 (↑k : ℝ)⌋₊ | Nat.Prime p}

Tactic:
ext p
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
R : Type u_1
inst : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
k : ℕ
h : k ∈ Icc 1 ⌊log x / log 2⌋₊
p : ℕ
e_s :
  ((0 < p ∧ p ≤ ⌊x⌋₊) ∧ Nat.Prime p) ∧ p ≤ ⌊HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹⌋₊ ↔
    (0 < p ∧ p ≤ ⌊x ^ HDiv.hDiv (α := ℝ) 1 (↑k : ℝ)⌋₊) ∧ Nat.Prime p
⊢ p ∈ {x_1 ∈ filter Nat.Prime (Ioc 0 ⌊x⌋₊) | x_1 ≤ ⌊HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹⌋₊} ↔
    p ∈ {p ∈ Ioc 0 ⌊x ^ HDiv.hDiv (α := ℝ) 1 (↑k : ℝ)⌋₊ | Nat.Prime p}

Tactic:
simp only [mem_filter, mem_Ioc]

Premises used: Finset.mem_filter, Finset.mem_Ioc
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
R : Type u_1
inst : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
k : ℕ
h : k ∈ Icc 1 ⌊log x / log 2⌋₊
p : ℕ
h_1 : ((0 < p ∧ p ≤ ⌊x⌋₊) ∧ Nat.Prime p) ∧ p ≤ ⌊HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹⌋₊
⊢ (0 < p ∧ p ≤ ⌊x ^ HDiv.hDiv (α := ℝ) 1 (↑k : ℝ)⌋₊) ∧ Nat.Prime p

Tactic:
simp_all
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
R : Type u_1
inst : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
k : ℕ
h : k ∈ Icc 1 ⌊log x / log 2⌋₊
p : ℕ
e_s :
  ∀ (h : (0 < p ∧ p ≤ ⌊x ^ HDiv.hDiv (α := ℝ) 1 (↑k : ℝ)⌋₊) ∧ Nat.Prime p),
    ((0 < p ∧ p ≤ ⌊x⌋₊) ∧ Nat.Prime p) ∧ p ≤ ⌊HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹⌋₊
⊢ ((0 < p ∧ p ≤ ⌊x⌋₊) ∧ Nat.Prime p) ∧ p ≤ ⌊HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹⌋₊ ↔
    (0 < p ∧ p ≤ ⌊x ^ HDiv.hDiv (α := ℝ) 1 (↑k : ℝ)⌋₊) ∧ Nat.Prime p

Tactic:
refine ⟨fun _ ↦ (by simp_all), fun h ↦ ?_⟩
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
R : Type u_1
inst : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
k : ℕ
h_1 : k ∈ Icc 1 ⌊log x / log 2⌋₊
p : ℕ
h : (0 < p ∧ p ≤ ⌊x ^ HDiv.hDiv (α := ℝ) 1 (↑k : ℝ)⌋₊) ∧ Nat.Prime p
e_s : 1 ≤ k ∧ k ≤ ⌊log x / log 2⌋₊ → ∀ (h : (0 < p ∧ p ≤ ⌊HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹⌋₊) ∧ Nat.Prime p), p ≤ ⌊x⌋₊
⊢ ((0 < p ∧ p ≤ ⌊x⌋₊) ∧ Nat.Prime p) ∧ p ≤ ⌊HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹⌋₊

Tactic:
simp_all only [mem_Icc, one_div, true_and, and_true]

Premises used: and_true, Finset.mem_Icc, one_div, true_and
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
R : Type u_1
inst : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
k p : ℕ
h_1 : 1 ≤ k ∧ k ≤ ⌊log x / log 2⌋₊
h : (0 < p ∧ p ≤ ⌊HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹⌋₊) ∧ Nat.Prime p
e_s : HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹ ≤ x
⊢ p ≤ ⌊x⌋₊

Tactic:
grw [h.1.2, floor_le_floor]

Premises used: Nat.floor_le_floor, And.right, And.left
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
R : Type u_1
inst : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
k p : ℕ
h_1 : 1 ≤ k ∧ k ≤ ⌊log x / log 2⌋₊
h : (0 < p ∧ p ≤ ⌊HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹⌋₊) ∧ Nat.Prime p
⊢ LE.le (α := ℝ) (↑k : ℝ)⁻¹ 1

Tactic:
bound
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
R : Type u_1
inst : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
k p : ℕ
h_1 : 1 ≤ k ∧ k ≤ ⌊log x / log 2⌋₊
h : (0 < p ∧ p ≤ ⌊HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹⌋₊) ∧ Nat.Prime p
apply : 1 ≤ x
⊢ HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹ ≤ x

Tactic:
apply rpow_le_self_of_one_le _ (by bound)

Premises used: Real.rpow_le_self_of_one_le
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
R : Type u_1
inst : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
k p : ℕ
h_1 : 1 ≤ k ∧ k ≤ ⌊log x / log 2⌋₊
h : (0 < p ∧ p ≤ ⌊HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹⌋₊) ∧ Nat.Prime p
⊢ 1 ≤ HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹

Tactic:
have := one_le_floor_iff _ |>.mp <| le_trans (one_le_cast.mp h.2.one_le) h.1.2
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
R : Type u_1
inst : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
k p : ℕ
h_1 : 1 ≤ k ∧ k ≤ ⌊log x / log 2⌋₊
h : (0 < p ∧ p ≤ ⌊HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹⌋₊) ∧ Nat.Prime p
this : 1 ≤ HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹
contrapose! : ∀ (this : x < 1), HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹ < 1
⊢ 1 ≤ x

Tactic:
contrapose! this
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
R : Type u_1
inst : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
k p : ℕ
h_1 : 1 ≤ k ∧ k ≤ ⌊log x / log 2⌋₊
h : (0 < p ∧ p ≤ ⌊HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹⌋₊) ∧ Nat.Prime p
this : x < 1
⊢ LT.lt (α := ℝ) 0 (↑k : ℝ)⁻¹

Tactic:
bound
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
R : Type u_1
inst : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
k p : ℕ
h_1 : 1 ≤ k ∧ k ≤ ⌊log x / log 2⌋₊
h : (0 < p ∧ p ≤ ⌊HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹⌋₊) ∧ Nat.Prime p
this : x < 1
⊢ HPow.hPow (β := ℝ) x (↑k : ℝ)⁻¹ < 1

Tactic:
apply rpow_lt_one hx this (by bound)

Premises used: Real.rpow_lt_one
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 0 ≤ x
simp_rw :
  Eq (α := ℝ)
    (∑ k ∈ Icc 1 ⌊log x / log 2⌋₊,
      ∑ p ∈ Ioc 0 ⌊x ^ HDiv.hDiv (α := ℝ) 1 (↑k : ℝ)⌋₊ with Nat.Prime p, log (↑(p ^ k).minFac : ℝ))
    (∑ n ∈ Icc 1 ⌊log x / log 2⌋₊, θ (x ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)))
⊢ ψ x = ∑ n ∈ Icc 1 ⌊log x / log 2⌋₊, θ (x ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))

Tactic:
simp_rw [psi, vonMangoldt_apply, ← sum_filter, sum_PrimePow_eq_sum_sum _ hx]

Premises used: Chebyshev.sum_PrimePow_eq_sum_sum, Chebyshev.psi, ArithmeticFunction.vonMangoldt_apply, Finset.sum_filter
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 0 ≤ x
apply :
  ∀ (x_1 : ℕ) (hk : x_1 ∈ Icc 1 ⌊log x / log 2⌋₊),
    ∀ x_2 ∈ {p ∈ Ioc 0 ⌊x ^ HDiv.hDiv (α := ℝ) 1 (↑x_1 : ℝ)⌋₊ | Nat.Prime p},
      log (↑(x_2 ^ x_1).minFac : ℝ) = log (↑x_2 : ℝ)
⊢ Eq (α := ℝ)
    (∑ k ∈ Icc 1 ⌊log x / log 2⌋₊,
      ∑ p ∈ Ioc 0 ⌊x ^ HDiv.hDiv (α := ℝ) 1 (↑k : ℝ)⌋₊ with Nat.Prime p, log (↑(p ^ k).minFac : ℝ))
    (∑ n ∈ Icc 1 ⌊log x / log 2⌋₊, θ (x ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)))

Tactic:
apply sum_congr rfl fun _ hk ↦ sum_congr rfl fun _ _ ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 0 ≤ x
x_1 : ℕ
hk : x_1 ∈ Icc 1 ⌊log x / log 2⌋₊
x_2 : ℕ
h : x_2 ∈ {p ∈ Ioc 0 ⌊x ^ HDiv.hDiv (α := ℝ) 1 (↑x_1 : ℝ)⌋₊ | Nat.Prime p}
linarith : x_1 = 0 → -1 + HSub.hSub (α := ℤ) (↑x_1 : ℤ) 0 + HSub.hSub (α := ℤ) 1 (↑x_1 : ℤ) = 0
⊢ x_1 ≠ 0

Tactic:
linarith [mem_Icc.mp hk]

Premises used: Finset.mem_Icc, Iff.mp
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 0 ≤ x
x_1 : ℕ
hk : x_1 ∈ Icc 1 ⌊log x / log 2⌋₊
x_2 : ℕ
h : x_2 ∈ {p ∈ Ioc 0 ⌊x ^ HDiv.hDiv (α := ℝ) 1 (↑x_1 : ℝ)⌋₊ | Nat.Prime p}
rw : Nat.Prime x_2
⊢ log (↑(x_2 ^ x_1).minFac : ℝ) = log (↑x_2 : ℝ)

Tactic:
rw [Prime.pow_minFac _ (by linarith [mem_Icc.mp hk])]

Premises used: Nat.Prime.pow_minFac
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 0 ≤ x
x_1 : ℕ
hk : x_1 ∈ Icc 1 ⌊log x / log 2⌋₊
x_2 : ℕ
h : x_2 ∈ {p ∈ Ioc 0 ⌊x ^ HDiv.hDiv (α := ℝ) 1 (↑x_1 : ℝ)⌋₊ | Nat.Prime p}
⊢ Nat.Prime x_2

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

Tactic:
linarith
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 2 ≤ x
rw :
  θ (x ^ HDiv.hDiv (α := ℝ) 1 (↑1 : ℝ)) + ∑ x_1 ∈ Ioc 1 ⌊log x / log 2⌋₊, θ (x ^ HDiv.hDiv (α := ℝ) 1 (↑x_1 : ℝ)) =
    θ x + ∑ n ∈ Icc 2 ⌊log x / log 2⌋₊, θ (x ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
rw₁ : 1 ≤ ⌊log x / log 2⌋₊
⊢ ψ x = θ x + ∑ n ∈ Icc 2 ⌊log x / log 2⌋₊, θ (x ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))

Tactic:
rw [psi_eq_sum_theta (by linarith), ← add_sum_Ioc_eq_sum_Icc]

Premises used: Chebyshev.psi_eq_sum_theta, Finset.add_sum_Ioc_eq_sum_Icc
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 2 ≤ x
e_a : x ^ HDiv.hDiv (α := ℝ) 1 (↑1 : ℝ) = x
⊢ θ (x ^ HDiv.hDiv (α := ℝ) 1 (↑1 : ℝ)) + ∑ x_1 ∈ Ioc 1 ⌊log x / log 2⌋₊, θ (x ^ HDiv.hDiv (α := ℝ) 1 (↑x_1 : ℝ)) =
    θ x + ∑ n ∈ Icc 2 ⌊log x / log 2⌋₊, θ (x ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))

Tactic:
congr
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 2 ≤ x
⊢ x ^ HDiv.hDiv (α := ℝ) 1 (↑1 : ℝ) = x

Tactic:
simp
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 2 ≤ x
⊢ 0 < log 2

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 2 ≤ x
rw : log 2 ≤ log x
⊢ 1 ≤ ⌊log x / log 2⌋₊

Tactic:
rw [le_floor_iff' one_ne_zero, le_div_iff₀ (by positivity), cast_one, one_mul]

Premises used: Nat.le_floor_iff', one_ne_zero, le_div_iff₀, Nat.cast_one, one_mul
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 2 ≤ x
hx₁ : LT.lt (α := ℝ) 0 2
⊢ log 2 ≤ log x

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
pos : ∀ (h : x < 2), θ x ≤ ψ x
neg : ∀ (h : 2 ≤ x), θ x ≤ ψ x
⊢ θ x ≤ ψ x

Tactic:
by_cases! h : x < 2
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
h : x < 2
pos : 0 ≤ ψ x
pos₁ pos₂ : LE.le (α := ℝ) 0 0
⊢ θ x ≤ ψ x

Tactic:
rw [theta_eq_zero_of_lt_two h, psi_eq_zero_of_lt_two h]

Premises used: Chebyshev.theta_eq_zero_of_lt_two, Chebyshev.psi_eq_zero_of_lt_two
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
h : 2 ≤ x
neg : θ x ≤ θ x + ∑ n ∈ Icc 2 ⌊log x / log 2⌋₊, θ (x ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))
⊢ θ x ≤ ψ x

Tactic:
rw [psi_eq_theta_add_sum_theta h]

Premises used: Chebyshev.psi_eq_theta_add_sum_theta
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
h : 2 ≤ x
neg : LE.le (α := ℝ) 0 (∑ n ∈ Icc 2 ⌊log x / log 2⌋₊, θ (x ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)))
⊢ θ x ≤ θ x + ∑ n ∈ Icc 2 ⌊log x / log 2⌋₊, θ (x ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))

Tactic:
simp only [le_add_iff_nonneg_right]

Premises used: le_add_iff_nonneg_right
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
h : 2 ≤ x
⊢ LE.le (α := ℝ) 0 (∑ n ∈ Icc 2 ⌊log x / log 2⌋₊, θ (x ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)))

Tactic:
sum_nonneg fun _ _ ↦ theta_nonneg _

Premises used: HDiv.hDiv, Finset.sum_nonneg, Nat.cast, HPow.hPow, Chebyshev.theta_nonneg, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
h : 2 ≤ x
⊢ LE.le (α := ℝ) 0 (∑ n ∈ Icc 2 ⌊log x / log 2⌋₊, θ (x ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ)))

Tactic:
exact sum_nonneg fun _ _ ↦ theta_nonneg _

Premises used: Finset.sum_nonneg, Chebyshev.theta_nonneg
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 1 ≤ x
pos : ∀ (hx : x < 2), |ψ x - θ x| ≤ 2 * √x * log x
neg : ∀ (hx : 2 ≤ x), |ψ x - θ x| ≤ 2 * √x * log x
⊢ |ψ x - θ x| ≤ 2 * √x * log x

Tactic:
by_cases! hx : x < 2
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx_1 : 1 ≤ x
hx : x < 2
pos : 0 ≤ 2 * √x * log x
⊢ |ψ x - θ x| ≤ 2 * √x * log x

Tactic:
rw [psi_eq_zero_of_lt_two hx, theta_eq_zero_of_lt_two hx, sub_zero, abs_zero]

Premises used: Chebyshev.theta_eq_zero_of_lt_two, sub_zero, Chebyshev.psi_eq_zero_of_lt_two, abs_zero
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx_1 : 1 ≤ x
hx : x < 2
⊢ 0 ≤ 2 * √x * log x

Tactic:
bound
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx_1 : 1 ≤ x
hx : 2 ≤ x
neg : |∑ n ∈ Icc 2 ⌊log x / log 2⌋₊, θ (x ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))| ≤ 2 * √x * log x
⊢ |ψ x - θ x| ≤ 2 * √x * log x

Tactic:
rw [psi_eq_theta_add_sum_theta hx, add_sub_cancel_left]

Premises used: add_sub_cancel_left, Chebyshev.psi_eq_theta_add_sum_theta
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx_1 : 1 ≤ x
hx : 2 ≤ x
neg : ∑ i ∈ Icc 2 ⌊log x / log 2⌋₊, |θ (x ^ HDiv.hDiv (α := ℝ) 1 (↑i : ℝ))| ≤ 2 * √x * log x
⊢ |∑ n ∈ Icc 2 ⌊log x / log 2⌋₊, θ (x ^ HDiv.hDiv (α := ℝ) 1 (↑n : ℝ))| ≤ 2 * √x * log x

Tactic:
apply le_trans <| abs_sum_le_sum_abs ..

Premises used: Finset.abs_sum_le_sum_abs, le_trans
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx_1 : 1 ≤ x
hx : 2 ≤ x
neg : ∑ x_1 ∈ Icc 2 ⌊log x / log 2⌋₊, θ (x ^ HDiv.hDiv (α := ℝ) 1 (↑x_1 : ℝ)) ≤ 2 * √x * log x
⊢ ∑ i ∈ Icc 2 ⌊log x / log 2⌋₊, |θ (x ^ HDiv.hDiv (α := ℝ) 1 (↑i : ℝ))| ≤ 2 * √x * log x

Tactic:
simp_rw [abs_of_nonneg <| theta_nonneg _]

Premises used: Chebyshev.theta_nonneg, abs_of_nonneg
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx_1 : 1 ≤ x
hx : 2 ≤ x
trans :
  LE.le (α := ℝ) (∑ x_1 ∈ Icc 2 ⌊log x / log 2⌋₊, θ (x ^ HDiv.hDiv (α := ℝ) 1 (↑x_1 : ℝ)))
    (∑ i ∈ Icc 2 ⌊log x / log 2⌋₊, log 4 * √x)
trans₁ : ∑ i ∈ Icc 2 ⌊log x / log 2⌋₊, log 4 * √x ≤ 2 * √x * log x
⊢ ∑ x_1 ∈ Icc 2 ⌊log x / log 2⌋₊, θ (x ^ HDiv.hDiv (α := ℝ) 1 (↑x_1 : ℝ)) ≤ 2 * √x * log x

Tactic:
trans ∑ i ∈ Icc 2 ⌊log x / log 2⌋₊, log 4 * x.sqrt

Premises used: HDiv.hDiv, Finset.Icc, Real.log, Nat.floor, Real.sqrt, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx_1 : 1 ≤ x
hx : 2 ≤ x
h : ∀ (i : ℕ) (hi : i ∈ Icc 2 ⌊log x / log 2⌋₊), θ (x ^ HDiv.hDiv (α := ℝ) 1 (↑i : ℝ)) ≤ log 4 * √x
⊢ LE.le (α := ℝ) (∑ x_1 ∈ Icc 2 ⌊log x / log 2⌋₊, θ (x ^ HDiv.hDiv (α := ℝ) 1 (↑x_1 : ℝ)))
    (∑ i ∈ Icc 2 ⌊log x / log 2⌋₊, log 4 * √x)

Tactic:
gcongr with i hi
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx_1 : 1 ≤ x
hx : 2 ≤ x
i : ℕ
hi : i ∈ Icc 2 ⌊log x / log 2⌋₊
linarith : x < 0 → HMul.hMul (α := ℝ) 2 (-1) + (2 - x) + (x - 0) = 0
linarith₁ : x < 0 → GT.gt (α := ℝ) 2 0
⊢ 0 ≤ x

Tactic:
linarith
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx_1 : 1 ≤ x
hx : 2 ≤ x
i : ℕ
hi : i ∈ Icc 2 ⌊log x / log 2⌋₊
h : log 4 * x ^ HDiv.hDiv (α := ℝ) 1 (↑i : ℝ) ≤ log 4 * √x
⊢ θ (x ^ HDiv.hDiv (α := ℝ) 1 (↑i : ℝ)) ≤ log 4 * √x

Tactic:
apply le_trans (theta_le_log4_mul_x (rpow_nonneg (by linarith) _))

Premises used: Chebyshev.theta_le_log4_mul_x, Real.rpow_nonneg, le_trans
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx_1 : 1 ≤ x
hx : 2 ≤ x
i : ℕ
hi : i ∈ Icc 2 ⌊log x / log 2⌋₊
h : log 4 * x ^ HDiv.hDiv (α := ℝ) 1 (↑i : ℝ) ≤ log 4 * x ^ (1 / 2)
⊢ log 4 * x ^ HDiv.hDiv (α := ℝ) 1 (↑i : ℝ) ≤ log 4 * √x

Tactic:
rw [sqrt_eq_rpow]

Premises used: Real.sqrt_eq_rpow
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx_1 : 1 ≤ x
hx : 2 ≤ x
i : ℕ
hi : i ∈ Icc 2 ⌊log x / log 2⌋₊
h : LE.le (α := ℝ) 2 (↑i : ℝ)
⊢ log 4 * x ^ HDiv.hDiv (α := ℝ) 1 (↑i : ℝ) ≤ log 4 * x ^ (1 / 2)

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx_1 : 1 ≤ x
hx : 2 ≤ x
i : ℕ
hi : i ∈ Icc 2 ⌊log x / log 2⌋₊
⊢ LE.le (α := ℝ) 2 (↑i : ℝ)

Tactic:
simp_all
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx_1 : 1 ≤ x
hx : 2 ≤ x
simp : (↑(⌊log x / log 2⌋₊ - 1) : ℝ) * (log 4 * √x) ≤ 2 * √x * log x
⊢ ∑ i ∈ Icc 2 ⌊log x / log 2⌋₊, log 4 * √x ≤ 2 * √x * log x

Tactic:
simp only [sum_const, card_Icc, reduceSubDiff, nsmul_eq_mul]

Premises used: Nat.reduceSubDiff, Nat.card_Icc, nsmul_eq_mul, Finset.sum_const
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx_1 : 1 ≤ x
hx : 2 ≤ x
hbc : (↑(⌊log x / log 2⌋₊ - 1) : ℝ) ≤ log x / log 2
⊢ (↑(⌊log x / log 2⌋₊ - 1) : ℝ) * (log 4 * √x) ≤ log x / log 2 * (log 4 * √x)

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx_1 : 1 ≤ x
hx : 2 ≤ x
hbc : HSub.hSub (α := ℝ) (↑⌊log x / log 2⌋₊ : ℝ) (↑1 : ℝ) ≤ log x / log 2
hbc₁ : 1 ≤ ⌊log x / log 2⌋₊
⊢ (↑(⌊log x / log 2⌋₊ - 1) : ℝ) ≤ log x / log 2

Tactic:
rw [cast_sub]

Premises used: Nat.cast_sub
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx_1 : 1 ≤ x
hx : 2 ≤ x
trans : HSub.hSub (α := ℝ) (↑⌊log x / log 2⌋₊ : ℝ) (↑1 : ℝ) ≤ (↑⌊log x / log 2⌋₊ : ℝ)
trans₁ : (↑⌊log x / log 2⌋₊ : ℝ) ≤ log x / log 2
⊢ HSub.hSub (α := ℝ) (↑⌊log x / log 2⌋₊ : ℝ) (↑1 : ℝ) ≤ log x / log 2

Tactic:
trans ↑⌊log x / log 2⌋₊

Premises used: Real.log, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx_1 : 1 ≤ x
hx : 2 ≤ x
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
⊢ HSub.hSub (α := ℝ) (↑⌊log x / log 2⌋₊ : ℝ) (↑1 : ℝ) ≤ (↑⌊log x / log 2⌋₊ : ℝ)

Tactic:
linarith
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx_1 : 1 ≤ x
hx : 2 ≤ x
⊢ 0 ≤ log x / log 2

Tactic:
bound
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx_1 : 1 ≤ x
hx : 2 ≤ x
⊢ (↑⌊log x / log 2⌋₊ : ℝ) ≤ log x / log 2

Tactic:
exact floor_le (by bound)

Premises used: Nat.floor_le
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx_1 : 1 ≤ x
hx : 2 ≤ x
hbc : (↑1 : ℝ) ≤ log x / log 2
⊢ 1 ≤ ⌊log x / log 2⌋₊

Tactic:
apply le_floor

Premises used: Nat.le_floor
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx_1 : 1 ≤ x
hx : 2 ≤ x
hbc : 1 ≤ log x / log 2
⊢ (↑1 : ℝ) ≤ log x / log 2

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx_1 : 1 ≤ x
hx : 2 ≤ x
hbc : log 2 ≤ log x
apply : 0 < log 2
⊢ 1 ≤ log x / log 2

Tactic:
apply one_le_div _ |>.mpr

Premises used: Iff.mpr, one_le_div
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx_1 : 1 ≤ x
hx : 2 ≤ x
⊢ log 2 ≤ log x

Tactic:
bound
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx_1 : 1 ≤ x
hx : 2 ≤ x
⊢ 0 < log 2

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

Tactic:
field
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx_1 : 1 ≤ x
hx : 2 ≤ x
e_a : log 4 / log 2 = 2
⊢ log 4 / log 2 * √x * log x = 2 * √x * log x

Tactic:
congr
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx_1 : 1 ≤ x
hx : 2 ≤ x
⊢ 4 = HPow.hPow (α := ℝ) (β := ℕ) 2 2

Tactic:
norm_num
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx_1 : 1 ≤ x
hx : 2 ≤ x
e_a : (↑2 : ℝ) * log 2 / log 2 = 2
⊢ log 4 / log 2 = 2

Tactic:
rw [(by norm_num : (4 : ℝ) = 2 ^ 2), Real.log_pow]

Premises used: Real.log_pow
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx_1 : 1 ≤ x
hx : 2 ≤ x
⊢ (↑2 : ℝ) * log 2 / log 2 = 2

Tactic:
field
-- Module: Mathlib.NumberTheory.Chebyshev
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 4 / log 2 * √x * log x = 2 * √x * log x
⊢ (↑(⌊log x / log 2⌋₊ - 1) : ℝ) * (log 4 * √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

Premises used: HMul.hMul, HDiv.hDiv, Real.log, Real.sqrt, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 1 ≤ x
⊢ ψ x = ψ x - θ x + θ x

Tactic:
ring
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 1 ≤ x
h₁ : ψ x - θ x ≤ 2 * √x * log x
h₂ : θ x ≤ log 4 * x
⊢ ψ x - θ x + θ x ≤ 2 * √x * log x + log 4 * x

Tactic:
gcongr