awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 0 ≤ x
trans : log (↑(primorial ⌊x⌋₊) : ℝ) ≤ log (HPow.hPow (α := ℝ) 4 ⌊x⌋₊)
trans₁ : log (HPow.hPow (α := ℝ) 4 ⌊x⌋₊) ≤ log 4 * x
⊢ log (↑(primorial ⌊x⌋₊) : ℝ) ≤ log 4 * x

Tactic:
trans log (4 ^ ⌊x⌋₊)

Premises used: Real.log, HPow.hPow, Nat.floor, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 0 ≤ x
hx₁ : LT.lt (α := ℝ) 0 (↑(primorial ⌊x⌋₊) : ℝ)
hxy : (↑(primorial ⌊x⌋₊) : ℝ) ≤ HPow.hPow (α := ℝ) 4 ⌊x⌋₊
⊢ log (↑(primorial ⌊x⌋₊) : ℝ) ≤ log (HPow.hPow (α := ℝ) 4 ⌊x⌋₊)

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 0 ≤ x
hx₁ : 0 < primorial ⌊x⌋₊
⊢ LT.lt (α := ℝ) 0 (↑(primorial ⌊x⌋₊) : ℝ)

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 0 ≤ x
hxy : primorial ⌊x⌋₊ ≤ HPow.hPow (α := ℕ) 4 ⌊x⌋₊
⊢ (↑(primorial ⌊x⌋₊) : ℝ) ≤ HPow.hPow (α := ℝ) 4 ⌊x⌋₊

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 0 ≤ x
⊢ 0 < primorial ⌊x⌋₊

Tactic:
primorial_pos _

Premises used: primorial_pos
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 0 ≤ x
⊢ primorial ⌊x⌋₊ ≤ HPow.hPow (α := ℕ) 4 ⌊x⌋₊

Tactic:
primorial_le_four_pow _

Premises used: primorial_le_four_pow
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 0 ≤ x
⊢ 0 < primorial ⌊x⌋₊

Tactic:
exacts [primorial_pos _, primorial_le_four_pow _]

Premises used: primorial_le_four_pow, primorial_pos
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 0 ≤ x
rw : log 4 * (↑⌊x⌋₊ : ℝ) ≤ log 4 * x
⊢ log (HPow.hPow (α := ℝ) 4 ⌊x⌋₊) ≤ log 4 * x

Tactic:
rw [Real.log_pow, mul_comm]

Premises used: mul_comm, Real.log_pow
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 0 ≤ x
hbc : (↑⌊x⌋₊ : ℝ) ≤ x
⊢ log 4 * (↑⌊x⌋₊ : ℝ) ≤ log 4 * x

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

Tactic:
floor_le hx

Premises used: Nat.floor_le
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
x : ℝ
hx : 0 ≤ x
⊢ (↑⌊x⌋₊ : ℝ) ≤ x

Tactic:
exact floor_le hx

Premises used: Nat.floor_le
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n : ℕ
⊢ n.lcmUpto ≠ 0

Tactic:
simp [lcmUpto]

Premises used: Nat.lcmUpto
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n : ℕ
⊢ 0 < n.lcmUpto

Tactic:
pos_of_ne_zero <| lcmUpto_ne_zero n

Premises used: Nat.lcmUpto_ne_zero, pos_of_ne_zero
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n p : ℕ
hp : Prime p
x : ℕ
h : x ∈ Icc 1 n
⊢ id x ≠ 0

Tactic:
grind
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n p : ℕ
hp : Prime p
rw : ((Icc 1 n).sup fun (a : ℕ) ↦ ((id a).factorization : (a : ℕ) → ℕ) p) = log p n
⊢ (n.lcmUpto.factorization : (a : ℕ) → ℕ) p = log p n

Tactic:
rw [lcmUpto, Finset.factorization_lcm (fun _ _ ↦ by grind)]

Premises used: Nat.lcmUpto, Finset.factorization_lcm
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n p : ℕ
hp : Prime p
⊢ 1 < p

Tactic:
have := hp.one_lt
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n p : ℕ
hp : Prime p
this : 1 < p
⊢ ((Icc 1 n).sup fun (a : ℕ) ↦ ((id a).factorization : (a : ℕ) → ℕ) p) = log p n

Tactic:
le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n p : ℕ
hp : Prime p
this : 1 < p
refine_1 : ((Icc 1 n).sup fun (a : ℕ) ↦ ((id a).factorization : (a : ℕ) → ℕ) p) ≤ log p n
refine_2 : log p n ≤ (Icc 1 n).sup fun (a : ℕ) ↦ ((id a).factorization : (a : ℕ) → ℕ) p
⊢ ((Icc 1 n).sup fun (a : ℕ) ↦ ((id a).factorization : (a : ℕ) → ℕ) p) = log p n

Tactic:
refine le_antisymm ?_ ?_

Premises used: le_antisymm
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n p : ℕ
hp : Prime p
this : 1 < p
refine_1 : ∀ (b : ℕ), 1 ≤ b → b ≤ n → ((id b).factorization : (a : ℕ) → ℕ) p ≤ log p n
⊢ ((Icc 1 n).sup fun (a : ℕ) ↦ ((id a).factorization : (a : ℕ) → ℕ) p) ≤ log p n

Tactic:
simp only [Finset.sup_le_iff, mem_Icc, and_imp]

Premises used: and_imp, Finset.mem_Icc, Finset.sup_le_iff
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n p : ℕ
hp : Prime p
this : 1 < p
m : ℕ
h_1 : 1 ≤ m
h : m ≤ n
⊢ 0 < m

Tactic:
grind
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n p : ℕ
hp : Prime p
this : 1 < p
⊢ ∀ (b : ℕ), 1 ≤ b → b ≤ n → ((id b).factorization : (a : ℕ) → ℕ) p ≤ log p n

Tactic:
exact fun m _ h ↦ le_log_of_pow_le this (le_of_dvd (by grind) (ordProj_dvd m p) |>.trans h)

Premises used: Nat.le_log_of_pow_le, Nat.ordProj_dvd, LE.le.trans, Nat.le_of_dvd
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n p : ℕ
hp : Prime p
this : 1 < p
refine_2 : p ≤ n → log p n ≤ (Icc 1 n).sup fun (a : ℕ) ↦ ((id a).factorization : (a : ℕ) → ℕ) p
refine_2₁ : ∀ (h : n < p), log p n ≤ (Icc 1 n).sup fun (a : ℕ) ↦ ((id a).factorization : (a : ℕ) → ℕ) p
⊢ log p n ≤ (Icc 1 n).sup fun (a : ℕ) ↦ ((id a).factorization : (a : ℕ) → ℕ) p

Tactic:
rcases le_or_gt p n with _ | h

Premises used: le_or_gt
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n p : ℕ
hp : Prime p
this : 1 < p
h : p ≤ n
linarith :
  n = 0 →
    HMul.hMul (α := ℤ) 2 (-1) + (HAdd.hAdd (α := ℤ) 1 1 - (↑p : ℤ)) + HSub.hSub (α := ℤ) (↑p : ℤ) (↑n : ℤ) +
        HSub.hSub (α := ℤ) (↑n : ℤ) 0 =
      0
linarith₁ : n = 0 → GT.gt (α := ℤ) 2 0
⊢ n ≠ 0

Tactic:
linarith
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n p : ℕ
hp : Prime p
this : 1 < p
h : p ≤ n
⊢ p ^ log p n ≤ n

Tactic:
have := pow_log_le_self p (x := n) (by linarith)
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n p : ℕ
hp : Prime p
this_1 : 1 < p
h : p ≤ n
this : p ^ log p n ≤ n
⊢ p ^ log p n ∈ Icc 1 n

Tactic:
grind
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n p : ℕ
hp : Prime p
this_1 : 1 < p
h : p ≤ n
this : p ^ log p n ≤ n
refine_2 : log p n ≤ ((id (p ^ log p n)).factorization : (a : ℕ) → ℕ) p
⊢ log p n ≤ (Icc 1 n).sup fun (a : ℕ) ↦ ((id a).factorization : (a : ℕ) → ℕ) p

Tactic:
grw [← le_sup (b := p ^ p.log n) (by grind)]

Premises used: Finset.le_sup
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n p : ℕ
hp : Prime p
this_1 : 1 < p
h : p ≤ n
this : p ^ log p n ≤ n
⊢ log p n ≤ ((id (p ^ log p n)).factorization : (a : ℕ) → ℕ) p

Tactic:
simp [hp]
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n p : ℕ
hp : Prime p
this : 1 < p
h : n < p
⊢ log p n ≤ (Icc 1 n).sup fun (a : ℕ) ↦ ((id a).factorization : (a : ℕ) → ℕ) p

Tactic:
simp [log_of_lt h]

Premises used: Nat.log_of_lt
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n : ℕ
⊢ n.lcmUpto ∣ n !

Tactic:
simp +contextual [lcmUpto, dvd_factorial, Order.one_le_iff_pos]

Premises used: Nat.dvd_factorial, Nat.lcmUpto, Order.one_le_iff_pos
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n : ℕ
h : ∀ (p : ℕ), p ∈ n.lcmUpto.primeFactors ↔ p ∈ n.primesLE
⊢ n.lcmUpto.primeFactors = n.primesLE

Tactic:
ext p
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n p : ℕ
⊢ p ∈ n.lcmUpto.primeFactors ↔ p ∈ n.primesLE

Tactic:
⟨fun h ↦ ?_, fun h ↦ ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n p : ℕ
h : ∀ (h : p ∈ n.lcmUpto.primeFactors), p ∈ n.primesLE
h₁ : ∀ (h : p ∈ n.primesLE), p ∈ n.lcmUpto.primeFactors
⊢ p ∈ n.lcmUpto.primeFactors ↔ p ∈ n.primesLE

Tactic:
refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n p : ℕ
h : p ∈ n.lcmUpto.primeFactors
⊢ Prime p

Tactic:
have := prime_of_mem_primeFactors h
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n p : ℕ
h : p ∈ n.lcmUpto.primeFactors
this : Prime p
⊢ log p n ≠ 0

Tactic:
rw [← support_factorization, Finsupp.mem_support_iff, factorization_lcmUpto _ this] at h

Premises used: Finsupp.mem_support_iff, Nat.factorization_lcmUpto, Nat.support_factorization
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n p : ℕ
h : p ∈ n.lcmUpto.primeFactors
this : Prime p
h₁ : log p n ≠ 0
⊢ Prime p

Tactic:
rw [← support_factorization, Finsupp.mem_support_iff, factorization_lcmUpto _ this] at h

Premises used: Finsupp.mem_support_iff, Nat.factorization_lcmUpto, Nat.support_factorization
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n p : ℕ
h : log p n ≠ 0
this : Prime p
⊢ p ∈ n.primesLE

Tactic:
simp_all [mem_primesLE]

Premises used: Nat.mem_primesLE
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n p : ℕ
h : p ∈ n.primesLE
⊢ p ∈ n.lcmUpto.primeFactors

Tactic:
Prime.mem_primeFactors (prime_of_mem_primesLE h) (dvd_lcm ?_) <| lcmUpto_ne_zero n

Premises used: Nat.lcmUpto_ne_zero, Nat.prime_of_mem_primesLE, Nat.Prime.mem_primeFactors, Finset.dvd_lcm
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n p : ℕ
h : p ∈ n.primesLE
h₁ : p ∈ Icc 1 n
⊢ p ∈ n.lcmUpto.primeFactors

Tactic:
refine Prime.mem_primeFactors (prime_of_mem_primesLE h) (dvd_lcm ?_) <| lcmUpto_ne_zero n

Premises used: Nat.lcmUpto_ne_zero, Nat.prime_of_mem_primesLE, Nat.Prime.mem_primeFactors
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n p : ℕ
h : p ∈ n.primesLE
⊢ p ∈ Icc 1 n

Tactic:
mem_Icc.mpr ⟨(prime_of_mem_primesLE h).one_le, le_of_mem_primesLE h⟩

Premises used: Iff.mpr, Finset.mem_Icc, Nat.Prime.one_le, Nat.prime_of_mem_primesLE, And.intro, Nat.le_of_mem_primesLE
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n p : ℕ
h : p ∈ n.primesLE
⊢ p ∈ Icc 1 n

Tactic:
exact mem_Icc.mpr ⟨(prime_of_mem_primesLE h).one_le, le_of_mem_primesLE h⟩

Premises used: Iff.mpr, Finset.mem_Icc, Nat.Prime.one_le, Nat.prime_of_mem_primesLE, And.intro, Nat.le_of_mem_primesLE
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n : ℕ
rw : ∏ p ∈ n.lcmUpto.primeFactors, p ∣ n.lcmUpto
⊢ ∏ p ∈ range (n + 1) with Prime p, p ∣ n.lcmUpto

Tactic:
rw [← primesLE_eq_filter_range, ← primeFactors_lcmUpto]

Premises used: Nat.primeFactors_lcmUpto, Nat.primesLE_eq_filter_range
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n : ℕ
⊢ ∏ p ∈ n.lcmUpto.primeFactors, p ∣ n.lcmUpto

Tactic:
prod_primeFactors_dvd _

Premises used: Nat.prod_primeFactors_dvd
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n : ℕ
⊢ ∏ p ∈ n.lcmUpto.primeFactors, p ∣ n.lcmUpto

Tactic:
exact prod_primeFactors_dvd _

Premises used: Nat.prod_primeFactors_dvd
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n : ℕ
rw : n.lcmUpto.factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2
| n.lcmUpto

Tactic:
rw [← prod_factorization_pow_eq_self (lcmUpto_ne_zero n)]

Premises used: Nat.lcmUpto_ne_zero, Nat.prod_factorization_pow_eq_self
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n : ℕ
conv_lhs :
  Eq (α := ℕ) (n.lcmUpto.factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2)
    (∏ p ∈ n.primesLE, HPow.hPow (β := ℕ) p ((n.lcmUpto.factorization : (a : ℕ) → ℕ) p : ℕ))
⊢ n.lcmUpto = ∏ p ∈ n.primesLE, HPow.hPow (β := ℕ) p ((n.lcmUpto.factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
conv_lhs => rw [← prod_factorization_pow_eq_self (lcmUpto_ne_zero n)]

Premises used: Nat.lcmUpto_ne_zero, Nat.prod_factorization_pow_eq_self
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n : ℕ
e_s : n.lcmUpto.primeFactors = n.primesLE
⊢ Eq (α := ℕ) (∏ p ∈ n.lcmUpto.primeFactors, HPow.hPow (β := ℕ) p ((n.lcmUpto.factorization : (a : ℕ) → ℕ) p : ℕ))
    (∏ p ∈ n.primesLE, HPow.hPow (β := ℕ) p ((n.lcmUpto.factorization : (a : ℕ) → ℕ) p : ℕ))

Tactic:
congr
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n : ℕ
⊢ n.lcmUpto.primeFactors = n.primesLE

Tactic:
primeFactors_lcmUpto n

Premises used: Nat.primeFactors_lcmUpto
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n : ℕ
⊢ n.lcmUpto.primeFactors = n.primesLE

Tactic:
exact primeFactors_lcmUpto n

Premises used: Nat.primeFactors_lcmUpto
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n : ℕ
rw :
  Eq (α := ℕ) (∏ p ∈ n.primesLE, HPow.hPow (β := ℕ) p ((n.lcmUpto.factorization : (a : ℕ) → ℕ) p : ℕ))
    (∏ p ∈ n.primesLE, p ^ log p n)
⊢ n.lcmUpto = ∏ p ∈ n.primesLE, p ^ log p n

Tactic:
rw [lcmUpto_eq_prod]

Premises used: Nat.lcmUpto_eq_prod
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n : ℕ
⊢ Eq (α := ℕ) (∏ p ∈ n.primesLE, HPow.hPow (β := ℕ) p ((n.lcmUpto.factorization : (a : ℕ) → ℕ) p : ℕ))
    (∏ p ∈ n.primesLE, p ^ log p n)

Tactic:
Finset.prod_congr rfl fun p hp ↦ congrArg (p ^ ·) <|
    factorization_lcmUpto n <| prime_of_mem_primesLE hp

Premises used: congrArg, Nat.factorization_lcmUpto, Finset.prod_congr, Nat.prime_of_mem_primesLE, HPow.hPow, rfl
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n : ℕ
⊢ Eq (α := ℕ) (∏ p ∈ n.primesLE, HPow.hPow (β := ℕ) p ((n.lcmUpto.factorization : (a : ℕ) → ℕ) p : ℕ))
    (∏ p ∈ n.primesLE, p ^ log p n)

Tactic:
exact Finset.prod_congr rfl fun p hp ↦ congrArg (p ^ ·) <|
    factorization_lcmUpto n <| prime_of_mem_primesLE hp

Premises used: congrArg, Nat.factorization_lcmUpto, Finset.prod_congr, Nat.prime_of_mem_primesLE, HPow.hPow, rfl
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n : ℕ
simp_rw : Eq (α := ℕ) (∏ p ∈ n.primesLE, p ^ log p n) (∏ p ∈ n.primesLE, p ^ ⌊Real.log (↑n : ℝ) / Real.log (↑p : ℝ)⌋₊)
simp_rw₁ :
  Eq (α := ℕ) (∏ x ∈ n.primesLE, x ^ ⌊logb (↑x : ℝ) (↑n : ℝ)⌋₊)
    (∏ p ∈ n.primesLE, p ^ ⌊Real.log (↑n : ℝ) / Real.log (↑p : ℝ)⌋₊)
⊢ n.lcmUpto = ∏ p ∈ n.primesLE, p ^ ⌊Real.log (↑n : ℝ) / Real.log (↑p : ℝ)⌋₊

Tactic:
simp_rw [lcmUpto_eq_prod_pow_log, ← natFloor_logb_natCast, ← log_div_log]

Premises used: Real.natFloor_logb_natCast, Real.log_div_log, Nat.lcmUpto_eq_prod_pow_log
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n : ℕ
⊢ ψ (↑n : ℝ) = ∑ m ∈ Icc 1 n, (Λ : (a : ℕ) → ℝ) m

Tactic:
simp [psi, ← Icc_add_one_left_eq_Ioc]

Premises used: Finset.Icc_add_one_left_eq_Ioc, Chebyshev.psi
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n : ℕ
⊢ Eq (α := ℝ) (∑ m ∈ Icc 1 n, (Λ : (a : ℕ) → ℝ) m)
    (∑ m ∈ (filter Nat.Prime (Icc 1 n)).biUnion fun (p : ℕ) ↦ image (fun (x : ℕ) ↦ p ^ x) (Icc 1 (Nat.log p n)),
      (Λ : (a : ℕ) → ℝ) m)

Tactic:
(sum_subset (fun q hq ↦ ?_) fun x hx ↦ ?_).symm

Premises used: Finset.sum_subset, Eq.symm
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n : ℕ
refine_1 :
  ∀ (q : ℕ)
    (hq :
      Membership.mem (γ := Finset ℕ)
        ((filter Nat.Prime (Icc 1 n)).biUnion fun (p : ℕ) ↦ image (fun (x : ℕ) ↦ p ^ x) (Icc 1 (Nat.log p n))) q),
    q ∈ Icc 1 n
refine_2 :
  ∀ (x : ℕ) (hx : x ∈ Icc 1 n),
    (x ∉ (filter Nat.Prime (Icc 1 n)).biUnion fun (p : ℕ) ↦ image (fun (x : ℕ) ↦ p ^ x) (Icc 1 (Nat.log p n))) →
      Eq (α := ℝ) ((Λ : (a : ℕ) → ℝ) x : ℝ) (0 : ℝ)
⊢ Eq (α := ℝ) (∑ m ∈ Icc 1 n, (Λ : (a : ℕ) → ℝ) m)
    (∑ m ∈ (filter Nat.Prime (Icc 1 n)).biUnion fun (p : ℕ) ↦ image (fun (x : ℕ) ↦ p ^ x) (Icc 1 (Nat.log p n)),
      (Λ : (a : ℕ) → ℝ) m)

Tactic:
refine (sum_subset (fun q hq ↦ ?_) fun x hx ↦ ?_).symm

Premises used: Finset.sum_subset, Eq.symm
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n q : ℕ
hq :
  Membership.mem (γ := Finset ℕ)
    ((filter Nat.Prime (Icc 1 n)).biUnion fun (p : ℕ) ↦ image (fun (x : ℕ) ↦ p ^ x) (Icc 1 (Nat.log p n))) q
refine_1 :
  ∀ (hq : ∃ (a : ℕ), ((1 ≤ a ∧ a ≤ n) ∧ Nat.Prime a) ∧ ∃ (a_1 : ℕ), (1 ≤ a_1 ∧ a_1 ≤ Nat.log a n) ∧ a ^ a_1 = q),
    1 ≤ q ∧ q ≤ n
⊢ q ∈ Icc 1 n

Tactic:
simp only [mem_biUnion, mem_filter, mem_Icc, mem_image] at hq ⊢

Premises used: Finset.mem_image, Finset.mem_Icc, Finset.mem_filter, Finset.mem_biUnion
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n q : ℕ
hq : ∃ (a : ℕ), ((1 ≤ a ∧ a ≤ n) ∧ Nat.Prime a) ∧ ∃ (a_1 : ℕ), (1 ≤ a_1 ∧ a_1 ≤ Nat.log a n) ∧ a ^ a_1 = q
refine_1 : ∀ (p : ℕ), (1 ≤ p ∧ p ≤ n) ∧ Nat.Prime p → ∀ (k : ℕ), 1 ≤ k → ∀ (hk : k ≤ Nat.log p n), 1 ≤ p ^ k ∧ p ^ k ≤ n
⊢ 1 ≤ q ∧ q ≤ n

Tactic:
obtain ⟨p, _, k, ⟨_, hk⟩, rfl⟩ := hq

Premises used: rfl
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n p : ℕ
left : (1 ≤ p ∧ p ≤ n) ∧ Nat.Prime p
k : ℕ
left_1 : 1 ≤ k
hk : k ≤ Nat.log p n
⊢ 1 ≤ p ^ k

Tactic:
grind
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n p : ℕ
left : (1 ≤ p ∧ p ≤ n) ∧ Nat.Prime p
k : ℕ
left_1 : 1 ≤ k
hk : k ≤ Nat.log p n
linarith :
  n = 0 → -1 + HSub.hSub (α := ℤ) 1 (↑p : ℤ) + HSub.hSub (α := ℤ) (↑p : ℤ) (↑n : ℤ) + HSub.hSub (α := ℤ) (↑n : ℤ) 0 = 0
⊢ n ≠ 0

Tactic:
linarith
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n p : ℕ
left : (1 ≤ p ∧ p ≤ n) ∧ Nat.Prime p
k : ℕ
left_1 : 1 ≤ k
hk : k ≤ Nat.log p n
⊢ 1 ≤ p ^ k ∧ p ^ k ≤ n

Tactic:
exact ⟨by grind, pow_le_of_le_log (by linarith) hk⟩
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n x : ℕ
hx : x ∈ Icc 1 n
refine_2 :
  (∀ (x_1 : ℕ), 1 ≤ x_1 → x_1 ≤ n → Nat.Prime x_1 → ∀ (x_2 : ℕ), 1 ≤ x_2 → x_2 ≤ Nat.log x_1 n → ¬x_1 ^ x_2 = x) →
    ∀ (x_1 x_2 : ℕ), Nat.Prime x_1 → 0 < x_2 → ¬x_1 ^ x_2 = x
⊢ (x ∉ (filter Nat.Prime (Icc 1 n)).biUnion fun (p : ℕ) ↦ image (fun (x : ℕ) ↦ p ^ x) (Icc 1 (Nat.log p n))) →
    Eq (α := ℝ) ((Λ : (a : ℕ) → ℝ) x : ℝ) (0 : ℝ)

Tactic:
simp only [mem_biUnion, mem_filter, mem_Icc, mem_image, not_exists, not_and, and_imp,
        vonMangoldt_eq_zero_iff, isPrimePow_nat_iff]

Premises used: Finset.mem_image, and_imp, isPrimePow_nat_iff, not_exists, Finset.mem_Icc, Finset.mem_filter, ArithmeticFunction.vonMangoldt_eq_zero_iff, not_and, Finset.mem_biUnion
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n x : ℕ
hx : x ∈ Icc 1 n
refine_2 :
  (∃ (x_1 : ℕ) (x_2 : ℕ), Nat.Prime x_1 ∧ 0 < x_2 ∧ x_1 ^ x_2 = x) →
    ∃ (x_1 : ℕ), 1 ≤ x_1 ∧ x_1 ≤ n ∧ Nat.Prime x_1 ∧ ∃ (x_2 : ℕ), 1 ≤ x_2 ∧ x_2 ≤ Nat.log x_1 n ∧ x_1 ^ x_2 = x
⊢ (∀ (x_1 : ℕ), 1 ≤ x_1 → x_1 ≤ n → Nat.Prime x_1 → ∀ (x_2 : ℕ), 1 ≤ x_2 → x_2 ≤ Nat.log x_1 n → ¬x_1 ^ x_2 = x) →
    ∀ (x_1 x_2 : ℕ), Nat.Prime x_1 → 0 < x_2 → ¬x_1 ^ x_2 = x

Tactic:
contrapose!
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n p k : ℕ
hp : Nat.Prime p
hk : 0 < k
hx : p ^ k ∈ Icc 1 n
⊢ 1 ≤ p ^ k ∧ p ^ k ≤ n

Tactic:
simp only [mem_Icc] at hx

Premises used: Finset.mem_Icc
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n p k : ℕ
hp : Nat.Prime p
hk : 0 < k
hx : 1 ≤ p ^ k ∧ p ^ k ≤ n
⊢ 0 < p ^ k

Tactic:
lia
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n p k : ℕ
hp : Nat.Prime p
hk : 0 < k
hx : 1 ≤ p ^ k ∧ p ^ k ≤ n
⊢ p ≤ n

Tactic:
have hpn : p ≤ n := (le_of_dvd (by lia) (dvd_pow_self p hk.ne')).trans hx.2
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n p k : ℕ
hp : Nat.Prime p
hk : 0 < k
hx : 1 ≤ p ^ k ∧ p ^ k ≤ n
hpn : p ≤ n
⊢ 1 ≤ k

Tactic:
lia
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n p k : ℕ
hp : Nat.Prime p
hk : 0 < k
hx : 1 ≤ p ^ k ∧ p ^ k ≤ n
hpn : p ≤ n
⊢ ∃ (x : ℕ), 1 ≤ x ∧ x ≤ n ∧ Nat.Prime x ∧ ∃ (x_1 : ℕ), 1 ≤ x_1 ∧ x_1 ≤ Nat.log x n ∧ x ^ x_1 = p ^ k

Tactic:
exact ⟨p, ⟨hp.one_le, hpn, hp, ⟨k, ⟨by lia, le_log_of_pow_le hp.one_lt hx.2, rfl⟩⟩⟩⟩
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n : ℕ
rw :
  ∀ ⦃i : ℕ⦄,
    i ∈ (↑(filter Nat.Prime (Icc 1 n)) : Set ℕ) →
      ∀ ⦃j : ℕ⦄,
        j ∈ (↑(filter Nat.Prime (Icc 1 n)) : Set ℕ) →
          Finset.Nonempty (α := ℕ)
              (image (fun (x : ℕ) ↦ i ^ x) (Icc 1 (Nat.log i n)) ∩ image (fun (x : ℕ) ↦ j ^ x) (Icc 1 (Nat.log j n))) →
            i = j
⊢ (↑(filter Nat.Prime (Icc 1 n)) : Set ℕ).PairwiseDisjoint (α := Finset ℕ) fun (p : ℕ) ↦
    image (fun (x : ℕ) ↦ p ^ x) (Icc 1 (Nat.log p n))

Tactic:
rw [pairwiseDisjoint_iff]

Premises used: Finset.pairwiseDisjoint_iff
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n : ℕ
⊢ ∀ ⦃i : ℕ⦄,
    i ∈ (↑(filter Nat.Prime (Icc 1 n)) : Set ℕ) →
      ∀ ⦃j : ℕ⦄,
        j ∈ (↑(filter Nat.Prime (Icc 1 n)) : Set ℕ) →
          Finset.Nonempty (α := ℕ)
              (image (fun (x : ℕ) ↦ i ^ x) (Icc 1 (Nat.log i n)) ∩ image (fun (x : ℕ) ↦ j ^ x) (Icc 1 (Nat.log j n))) →
            i = j

Tactic:
grind [Prime.pow_inj']

Premises used: Nat.Prime.pow_inj'
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n : ℕ
rw rw₁ :
  Eq (α := ℝ)
    (∑ x ∈ Icc 1 n with Nat.Prime x, ∑ i ∈ image (fun (x_1 : ℕ) ↦ x ^ x_1) (Icc 1 (Nat.log x n)), (Λ : (a : ℕ) → ℝ) i)
    (∑ p ∈ Icc 1 n with Nat.Prime p, ∑ q ∈ image (fun (k : ℕ) ↦ p ^ k) (Icc 1 (Nat.log p n)), (Λ : (a : ℕ) → ℝ) q)
⊢ Eq (α := ℝ)
    (∑ m ∈ (filter Nat.Prime (Icc 1 n)).biUnion fun (p : ℕ) ↦ image (fun (x : ℕ) ↦ p ^ x) (Icc 1 (Nat.log p n)),
      (Λ : (a : ℕ) → ℝ) m)
    (∑ p ∈ Icc 1 n with Nat.Prime p, ∑ q ∈ image (fun (k : ℕ) ↦ p ^ k) (Icc 1 (Nat.log p n)), (Λ : (a : ℕ) → ℝ) q)

Tactic:
rw [sum_biUnion <| by rw [pairwiseDisjoint_iff]; grind [Prime.pow_inj']]

Premises used: Finset.sum_biUnion
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n : ℕ
⊢ Eq (α := ℝ)
    (∑ p ∈ Icc 1 n with Nat.Prime p, ∑ q ∈ image (fun (k : ℕ) ↦ p ^ k) (Icc 1 (Nat.log p n)), (Λ : (a : ℕ) → ℝ) q)
    (∑ p ∈ n.primesLE, ∑ k ∈ Icc 1 (Nat.log p n), (Λ : (a : ℕ) → ℝ) (p ^ k))

Tactic:
sum_congr (primesLE_eq_filter_Icc_one n).symm fun p hp ↦ ?_

Premises used: Nat.primesLE_eq_filter_Icc_one, Eq.symm, Finset.sum_congr
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n : ℕ
refine :
  ∀ (p : ℕ) (hp : p ∈ n.primesLE),
    Eq (α := ℝ) (∑ q ∈ image (fun (k : ℕ) ↦ p ^ k) (Icc 1 (Nat.log p n)), (Λ : (a : ℕ) → ℝ) q)
      (∑ k ∈ Icc 1 (Nat.log p n), (Λ : (a : ℕ) → ℝ) (p ^ k))
⊢ Eq (α := ℝ)
    (∑ p ∈ Icc 1 n with Nat.Prime p, ∑ q ∈ image (fun (k : ℕ) ↦ p ^ k) (Icc 1 (Nat.log p n)), (Λ : (a : ℕ) → ℝ) q)
    (∑ p ∈ n.primesLE, ∑ k ∈ Icc 1 (Nat.log p n), (Λ : (a : ℕ) → ℝ) (p ^ k))

Tactic:
refine sum_congr (primesLE_eq_filter_Icc_one n).symm fun p hp ↦ ?_

Premises used: Nat.primesLE_eq_filter_Icc_one, Eq.symm, Finset.sum_congr
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n p : ℕ
hp : p ∈ n.primesLE
⊢ Eq (α := ℝ) (∑ q ∈ image (fun (k : ℕ) ↦ p ^ k) (Icc 1 (Nat.log p n)), (Λ : (a : ℕ) → ℝ) q)
    (∑ k ∈ Icc 1 (Nat.log p n), (Λ : (a : ℕ) → ℝ) (p ^ k))

Tactic:
sum_image fun a _ b _ hab ↦ Nat.pow_right_injective (two_le_of_mem_primesLE hp) hab

Premises used: Nat.two_le_of_mem_primesLE, Nat.pow_right_injective, Finset.sum_image
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n p : ℕ
hp : p ∈ n.primesLE
⊢ Eq (α := ℝ) (∑ q ∈ image (fun (k : ℕ) ↦ p ^ k) (Icc 1 (Nat.log p n)), (Λ : (a : ℕ) → ℝ) q)
    (∑ k ∈ Icc 1 (Nat.log p n), (Λ : (a : ℕ) → ℝ) (p ^ k))

Tactic:
exact sum_image fun a _ b _ hab ↦ Nat.pow_right_injective (two_le_of_mem_primesLE hp) hab

Premises used: Nat.two_le_of_mem_primesLE, Nat.pow_right_injective, Finset.sum_image
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n : ℕ
⊢ Eq (α := ℝ) (∑ p ∈ n.primesLE, ∑ k ∈ Icc 1 (Nat.log p n), (Λ : (a : ℕ) → ℝ) (p ^ k))
    (∑ p ∈ n.primesLE, ∑ k ∈ Icc 1 (Nat.log p n), log (↑p : ℝ))

Tactic:
sum_congr rfl fun p hp ↦ sum_congr rfl fun k hk ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n : ℕ
refine :
  ∀ (p : ℕ) (hp : p ∈ n.primesLE) (k : ℕ) (hk : k ∈ Icc 1 (Nat.log p n)), (Λ : (a : ℕ) → ℝ) (p ^ k) = log (↑p : ℝ)
⊢ Eq (α := ℝ) (∑ p ∈ n.primesLE, ∑ k ∈ Icc 1 (Nat.log p n), (Λ : (a : ℕ) → ℝ) (p ^ k))
    (∑ p ∈ n.primesLE, ∑ k ∈ Icc 1 (Nat.log p n), log (↑p : ℝ))

Tactic:
refine sum_congr rfl fun p hp ↦ sum_congr rfl fun k hk ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n p : ℕ
hp : p ∈ n.primesLE
k : ℕ
hk : k ∈ Icc 1 (Nat.log p n)
⊢ k ≠ 0

Tactic:
grind
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n p : ℕ
hp : p ∈ n.primesLE
k : ℕ
hk : k ∈ Icc 1 (Nat.log p n)
rw : (Λ : (a : ℕ) → ℝ) p = log (↑p : ℝ)
rw₁ rw₂ : log (↑p : ℝ) = log (↑p : ℝ)
⊢ (Λ : (a : ℕ) → ℝ) (p ^ k) = log (↑p : ℝ)

Tactic:
rw [vonMangoldt_apply_pow (by grind), vonMangoldt_apply_prime <| prime_of_mem_primesLE hp]

Premises used: Nat.prime_of_mem_primesLE, ArithmeticFunction.vonMangoldt_apply_prime, ArithmeticFunction.vonMangoldt_apply_pow
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n : ℕ
⊢ Eq (α := ℝ) (∑ p ∈ n.primesLE, ∑ k ∈ Icc 1 (Nat.log p n), log (↑p : ℝ))
    (∑ p ∈ n.primesLE, (↑(Nat.log p n) : ℝ) * log (↑p : ℝ))

Tactic:
simp
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n : ℕ
rw : LE.le (α := ℝ) (∑ p ∈ n.primesLE, (↑(Nat.log p n) : ℝ) * log (↑p : ℝ)) (∑ _x ∈ n.primesLE, log (↑n : ℝ))
⊢ ψ (↑n : ℝ) ≤ (↑(π n) : ℝ) * log (↑n : ℝ)

Tactic:
rw [psi_eq_sum_mul_log_prime, ← primesLE_card_eq_primeCounting, ← nsmul_eq_mul, ← sum_const]

Premises used: Nat.primesLE_card_eq_primeCounting, Chebyshev.psi_eq_sum_mul_log_prime, nsmul_eq_mul, Finset.sum_const
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
n : ℕ
inl : LE.le (α := ℝ) (∑ p ∈ primesLE 0, (↑(Nat.log p 0) : ℝ) * log (↑p : ℝ)) (∑ _x ∈ primesLE 0, log (↑0 : ℝ))
inr :
  ∀ (hn : n ≠ 0),
    LE.le (α := ℝ) (∑ p ∈ n.primesLE, (↑(Nat.log p n) : ℝ) * log (↑p : ℝ)) (∑ _x ∈ n.primesLE, log (↑n : ℝ))
⊢ LE.le (α := ℝ) (∑ p ∈ n.primesLE, (↑(Nat.log p n) : ℝ) * log (↑p : ℝ)) (∑ _x ∈ n.primesLE, log (↑n : ℝ))

Tactic:
rcases eq_or_ne n 0 with rfl | hn

Premises used: eq_or_ne, OfNat.ofNat, rfl
-- Module: Mathlib.NumberTheory.Chebyshev
Goal:
⊢ LE.le (α := ℝ) (∑ p ∈ primesLE 0, (↑(Nat.log p 0) : ℝ) * log (↑p : ℝ)) (∑ _x ∈ primesLE 0, log (↑0 : ℝ))

Tactic:
simp