awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 0 ≤ x
⊢ log 4 * (↑⌊x⌋₊ : ℝ) ≤ log 4 * x
have hbc : (↑⌊x⌋₊ : ℝ) ≤ x
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
n p : ℕ
hp : Prime p
⊢ (n.lcmUpto.factorization : (a : ℕ) → ℕ) p = log p n
have rw : ((Icc 1 n).sup fun (a : ℕ) ↦ ((id a).factorization : (a : ℕ) → ℕ) p) = log p n
Tactic: rw [lcmUpto, Finset.factorization_lcm (fun _ _ ↦ by grind)]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (hypothesis)
Goal:
n p : ℕ
hp : Prime p
⊢ ((Icc 1 n).sup fun (a : ℕ) ↦ ((id a).factorization : (a : ℕ) → ℕ) p) = log p n
have this : 1 < p
Tactic: have := hp.one_lt
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
n p : ℕ
hp : Prime p
this : 1 < p
⊢ ((Icc 1 n).sup fun (a : ℕ) ↦ ((id a).factorization : (a : ℕ) → ℕ) p) = log p n
have refine_1 : ((Icc 1 n).sup fun (a : ℕ) ↦ ((id a).factorization : (a : ℕ) → ℕ) p) ≤ log p n
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
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
⊢ ((Icc 1 n).sup fun (a : ℕ) ↦ ((id a).factorization : (a : ℕ) → ℕ) p) = log p n
have refine_2 : log p n ≤ (Icc 1 n).sup fun (a : ℕ) ↦ ((id a).factorization : (a : ℕ) → ℕ) p
Tactic: refine le_antisymm ?_ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
n p : ℕ
hp : Prime p
this : 1 < p
⊢ ((Icc 1 n).sup fun (a : ℕ) ↦ ((id a).factorization : (a : ℕ) → ℕ) p) ≤ log p n
have refine_1 : ∀ (b : ℕ), 1 ≤ b → b ≤ n → ((id b).factorization : (a : ℕ) → ℕ) p ≤ log p n
Tactic: simp only [Finset.sup_le_iff, mem_Icc, and_imp]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
n p : ℕ
hp : Prime p
this : 1 < p
⊢ log p n ≤ (Icc 1 n).sup fun (a : ℕ) ↦ ((id a).factorization : (a : ℕ) → ℕ) p
have refine_2 : p ≤ n → log p n ≤ (Icc 1 n).sup fun (a : ℕ) ↦ ((id a).factorization : (a : ℕ) → ℕ) p
Tactic: rcases le_or_gt p n with _ | h
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
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
⊢ log p n ≤ (Icc 1 n).sup fun (a : ℕ) ↦ ((id a).factorization : (a : ℕ) → ℕ) p
have refine_2₁ : ∀ (h : n < p), log p n ≤ (Icc 1 n).sup fun (a : ℕ) ↦ ((id a).factorization : (a : ℕ) → ℕ) p
Tactic: rcases le_or_gt p n with _ | h
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
n p : ℕ
hp : Prime p
this : 1 < p
h : p ≤ n
⊢ n ≠ 0
have linarith : n = 0 →
  HMul.hMul (α := ℤ) 2 (-1) + (HAdd.hAdd (α := ℤ) 1 1 - (↑p : ℤ)) + HSub.hSub (α := ℤ) (↑p : ℤ) (↑n : ℤ) +
      HSub.hSub (α := ℤ) (↑n : ℤ) 0 =
    0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
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
⊢ n ≠ 0
have linarith₁ : n = 0 → GT.gt (α := ℤ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (hypothesis)
Goal:
n p : ℕ
hp : Prime p
this : 1 < p
h : p ≤ n
⊢ log p n ≤ (Icc 1 n).sup fun (a : ℕ) ↦ ((id a).factorization : (a : ℕ) → ℕ) p
have this₁ : p ^ log p n ≤ n
Tactic: have := pow_log_le_self p (x := n) (by linarith)
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
n p : ℕ
hp : Prime p
this_1 : 1 < p
h : p ≤ n
this : p ^ log p n ≤ n
⊢ log p n ≤ (Icc 1 n).sup fun (a : ℕ) ↦ ((id a).factorization : (a : ℕ) → ℕ) p
have refine_2 : log p n ≤ ((id (p ^ log p n)).factorization : (a : ℕ) → ℕ) p
Tactic: grw [← le_sup (b := p ^ p.log n) (by grind)]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
n : ℕ
⊢ n.lcmUpto.primeFactors = n.primesLE
have h : ∀ (p : ℕ), p ∈ n.lcmUpto.primeFactors ↔ p ∈ n.primesLE
Tactic: ext p
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
n p : ℕ
⊢ p ∈ n.lcmUpto.primeFactors ↔ p ∈ n.primesLE
have h : ∀ (h : p ∈ n.lcmUpto.primeFactors), p ∈ n.primesLE
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
n p : ℕ
h : ∀ (h : p ∈ n.lcmUpto.primeFactors), p ∈ n.primesLE
⊢ p ∈ n.lcmUpto.primeFactors ↔ p ∈ n.primesLE
have h₁ : ∀ (h : p ∈ n.primesLE), p ∈ n.lcmUpto.primeFactors
Tactic: refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (hypothesis)
Goal:
n p : ℕ
h : p ∈ n.lcmUpto.primeFactors
⊢ p ∈ n.primesLE
have this : Prime p
Tactic: have := prime_of_mem_primeFactors h
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (hypothesis)
Goal:
n p : ℕ
h : p ∈ n.lcmUpto.primeFactors
this : Prime p
⊢ p ∈ n.primesLE
have h₁ : log p n ≠ 0
Tactic: rw [← support_factorization, Finsupp.mem_support_iff, factorization_lcmUpto _ this] at h
Cleared hypotheses: h, this
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
n p : ℕ
h : p ∈ n.primesLE
⊢ p ∈ n.lcmUpto.primeFactors
have h₁ : p ∈ Icc 1 n
Tactic: refine Prime.mem_primeFactors (prime_of_mem_primesLE h) (dvd_lcm ?_) <| lcmUpto_ne_zero n
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
n : ℕ
⊢ ∏ p ∈ range (n + 1) with Prime p, p ∣ n.lcmUpto
have rw : ∏ p ∈ n.lcmUpto.primeFactors, p ∣ n.lcmUpto
Tactic: rw [← primesLE_eq_filter_range, ← primeFactors_lcmUpto]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
n : ℕ
| n.lcmUpto
have rw : n.lcmUpto.factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2
Tactic: rw [← prod_factorization_pow_eq_self (lcmUpto_ne_zero n)]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
n : ℕ
⊢ n.lcmUpto = ∏ p ∈ n.primesLE, HPow.hPow (β := ℕ) p ((n.lcmUpto.factorization : (a : ℕ) → ℕ) p : ℕ)
have conv_lhs : Eq (α := ℕ) (n.lcmUpto.factorization.prod fun (x1 x2 : ℕ) ↦ x1 ^ x2)
  (∏ p ∈ n.primesLE, HPow.hPow (β := ℕ) p ((n.lcmUpto.factorization : (a : ℕ) → ℕ) p : ℕ))
Tactic: conv_lhs => rw [← prod_factorization_pow_eq_self (lcmUpto_ne_zero n)]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
n : ℕ
⊢ Eq (α := ℕ) (∏ p ∈ n.lcmUpto.primeFactors, HPow.hPow (β := ℕ) p ((n.lcmUpto.factorization : (a : ℕ) → ℕ) p : ℕ))
    (∏ p ∈ n.primesLE, HPow.hPow (β := ℕ) p ((n.lcmUpto.factorization : (a : ℕ) → ℕ) p : ℕ))
have e_s : n.lcmUpto.primeFactors = n.primesLE
Tactic: congr
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
n : ℕ
⊢ n.lcmUpto = ∏ p ∈ n.primesLE, p ^ log p n
have rw : Eq (α := ℕ) (∏ p ∈ n.primesLE, HPow.hPow (β := ℕ) p ((n.lcmUpto.factorization : (a : ℕ) → ℕ) p : ℕ))
  (∏ p ∈ n.primesLE, p ^ log p n)
Tactic: rw [lcmUpto_eq_prod]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
n : ℕ
⊢ n.lcmUpto = ∏ p ∈ n.primesLE, p ^ ⌊Real.log (↑n : ℝ) / Real.log (↑p : ℝ)⌋₊
have simp_rw : Eq (α := ℕ) (∏ p ∈ n.primesLE, p ^ log p n) (∏ p ∈ n.primesLE, p ^ ⌊Real.log (↑n : ℝ) / Real.log (↑p : ℝ)⌋₊)
Tactic: simp_rw [lcmUpto_eq_prod_pow_log, ← natFloor_logb_natCast, ← log_div_log]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
n : ℕ
simp_rw : Eq (α := ℕ) (∏ p ∈ n.primesLE, p ^ log p n) (∏ p ∈ n.primesLE, p ^ ⌊Real.log (↑n : ℝ) / Real.log (↑p : ℝ)⌋₊)
⊢ n.lcmUpto = ∏ p ∈ n.primesLE, p ^ ⌊Real.log (↑n : ℝ) / Real.log (↑p : ℝ)⌋₊
have simp_rw₁ : Eq (α := ℕ) (∏ x ∈ n.primesLE, x ^ ⌊logb (↑x : ℝ) (↑n : ℝ)⌋₊)
  (∏ p ∈ n.primesLE, p ^ ⌊Real.log (↑n : ℝ) / Real.log (↑p : ℝ)⌋₊)
Tactic: simp_rw [lcmUpto_eq_prod_pow_log, ← natFloor_logb_natCast, ← log_div_log]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
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)
have 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
Tactic: refine (sum_subset (fun q hq ↦ ?_) fun x hx ↦ ?_).symm
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
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
⊢ 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)
have 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 : ℝ)
Tactic: refine (sum_subset (fun q hq ↦ ?_) fun x hx ↦ ?_).symm
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
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
⊢ q ∈ Icc 1 n
have 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
Tactic: simp only [mem_biUnion, mem_filter, mem_Icc, mem_image] at hq ⊢
Cleared hypotheses: hq
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
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
⊢ 1 ≤ q ∧ q ≤ n
have 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
Tactic: obtain ⟨p, _, k, ⟨_, hk⟩, rfl⟩ := hq
Cleared hypotheses: q, hq
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
n p : ℕ
left : (1 ≤ p ∧ p ≤ n) ∧ Nat.Prime p
k : ℕ
left_1 : 1 ≤ k
hk : k ≤ Nat.log p n
⊢ n ≠ 0
have linarith : n = 0 → -1 + HSub.hSub (α := ℤ) 1 (↑p : ℤ) + HSub.hSub (α := ℤ) (↑p : ℤ) (↑n : ℤ) + HSub.hSub (α := ℤ) (↑n : ℤ) 0 = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
n 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 : ℝ)
have 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
Tactic: simp only [mem_biUnion, mem_filter, mem_Icc, mem_image, not_exists, not_and, and_imp,
        vonMangoldt_eq_zero_iff, isPrimePow_nat_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
n x : ℕ
hx : x ∈ Icc 1 n
⊢ (∀ (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
have 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
Tactic: contrapose!
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (hypothesis)
Goal:
n p k : ℕ
hp : Nat.Prime p
hk : 0 < k
hx : p ^ k ∈ Icc 1 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
have hx₁ : 1 ≤ p ^ k ∧ p ^ k ≤ n
Tactic: simp only [mem_Icc] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (hypothesis)
Goal:
n p k : ℕ
hp : Nat.Prime p
hk : 0 < k
hx : 1 ≤ p ^ k ∧ p ^ k ≤ 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
have hpn : p ≤ n
Tactic: have hpn : p ≤ n := (le_of_dvd (by lia) (dvd_pow_self p hk.ne')).trans hx.2
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
n : ℕ
⊢ (↑(filter Nat.Prime (Icc 1 n)) : Set ℕ).PairwiseDisjoint (α := Finset ℕ) fun (p : ℕ) ↦
    image (fun (x : ℕ) ↦ p ^ x) (Icc 1 (Nat.log p n))
have 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
Tactic: rw [pairwiseDisjoint_iff]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
n : ℕ
⊢ 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)
have 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)
Tactic: rw [sum_biUnion <| by rw [pairwiseDisjoint_iff]; grind [Prime.pow_inj']]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
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))
have 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))
Tactic: refine sum_congr (primesLE_eq_filter_Icc_one n).symm fun p hp ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
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 : ℝ))
have refine : ∀ (p : ℕ) (hp : p ∈ n.primesLE) (k : ℕ) (hk : k ∈ Icc 1 (Nat.log p n)), (Λ : (a : ℕ) → ℝ) (p ^ k) = log (↑p : ℝ)
Tactic: refine sum_congr rfl fun p hp ↦ sum_congr rfl fun k hk ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
n p : ℕ
hp : p ∈ n.primesLE
k : ℕ
hk : k ∈ Icc 1 (Nat.log p n)
⊢ (Λ : (a : ℕ) → ℝ) (p ^ k) = log (↑p : ℝ)
have rw : (Λ : (a : ℕ) → ℝ) p = log (↑p : ℝ)
Tactic: rw [vonMangoldt_apply_pow (by grind), vonMangoldt_apply_prime <| prime_of_mem_primesLE hp]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
n p : ℕ
hp : p ∈ n.primesLE
k : ℕ
hk : k ∈ Icc 1 (Nat.log p n)
rw : (Λ : (a : ℕ) → ℝ) p = log (↑p : ℝ)
⊢ (Λ : (a : ℕ) → ℝ) (p ^ k) = log (↑p : ℝ)
have rw₁ : log (↑p : ℝ) = log (↑p : ℝ)
Tactic: rw [vonMangoldt_apply_pow (by grind), vonMangoldt_apply_prime <| prime_of_mem_primesLE hp]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
n : ℕ
⊢ ψ (↑n : ℝ) ≤ (↑(π n) : ℝ) * log (↑n : ℝ)
have rw : LE.le (α := ℝ) (∑ p ∈ n.primesLE, (↑(Nat.log p n) : ℝ) * log (↑p : ℝ)) (∑ _x ∈ n.primesLE, log (↑n : ℝ))
Tactic: rw [psi_eq_sum_mul_log_prime, ← primesLE_card_eq_primeCounting, ← nsmul_eq_mul, ← sum_const]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
n : ℕ
⊢ LE.le (α := ℝ) (∑ p ∈ n.primesLE, (↑(Nat.log p n) : ℝ) * log (↑p : ℝ)) (∑ _x ∈ n.primesLE, log (↑n : ℝ))
have inl : LE.le (α := ℝ) (∑ p ∈ primesLE 0, (↑(Nat.log p 0) : ℝ) * log (↑p : ℝ)) (∑ _x ∈ primesLE 0, log (↑0 : ℝ))
Tactic: rcases eq_or_ne n 0 with rfl | hn
Cleared hypotheses: n
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
n : ℕ
inl : LE.le (α := ℝ) (∑ p ∈ primesLE 0, (↑(Nat.log p 0) : ℝ) * log (↑p : ℝ)) (∑ _x ∈ primesLE 0, log (↑0 : ℝ))
⊢ LE.le (α := ℝ) (∑ p ∈ n.primesLE, (↑(Nat.log p n) : ℝ) * log (↑p : ℝ)) (∑ _x ∈ n.primesLE, log (↑n : ℝ))
have inr : ∀ (hn : n ≠ 0), 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
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
n : ℕ
hn : n ≠ 0
⊢ LE.le (α := ℝ) (∑ p ∈ n.primesLE, (↑(Nat.log p n) : ℝ) * log (↑p : ℝ)) (∑ _x ∈ n.primesLE, log (↑n : ℝ))
have inr : ∀ (p : ℕ) (hp : p ∈ n.primesLE), (↑(Nat.log p n) : ℝ) * log (↑p : ℝ) ≤ log (↑n : ℝ)
Tactic: gcongr with p hp
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
n : ℕ
hn : n ≠ 0
p : ℕ
hp : p ∈ n.primesLE
⊢ (↑(Nat.log p n) : ℝ) * log (↑p : ℝ) ≤ log (↑n : ℝ)
have inr : HPow.hPow (α := ℝ) (↑p : ℝ) (Nat.log p n) ≤ (↑n : ℝ)
Tactic: refine le_log_of_pow_le (mod_cast (prime_of_mem_primesLE hp).pos) ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
⊢ ψ x ≤ (↑(π ⌊x⌋₊) : ℝ) * log x
have grw : (↑(π ⌊x⌋₊) : ℝ) * log (↑⌊x⌋₊ : ℝ) ≤ (↑(π ⌊x⌋₊) : ℝ) * log x
Tactic: grw [psi_eq_psi_coe_floor, psi_le_primeCounting_mul_log]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
⊢ (↑(π ⌊x⌋₊) : ℝ) * log (↑⌊x⌋₊ : ℝ) ≤ (↑(π ⌊x⌋₊) : ℝ) * log x
have inl : ∀ (h : x < 1), (↑(π ⌊x⌋₊) : ℝ) * log (↑⌊x⌋₊ : ℝ) ≤ (↑(π ⌊x⌋₊) : ℝ) * log x
Tactic: rcases lt_or_ge x 1 with h | h
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
inl : ∀ (h : x < 1), (↑(π ⌊x⌋₊) : ℝ) * log (↑⌊x⌋₊ : ℝ) ≤ (↑(π ⌊x⌋₊) : ℝ) * log x
⊢ (↑(π ⌊x⌋₊) : ℝ) * log (↑⌊x⌋₊ : ℝ) ≤ (↑(π ⌊x⌋₊) : ℝ) * log x
have inr : ∀ (h : 1 ≤ x), (↑(π ⌊x⌋₊) : ℝ) * log (↑⌊x⌋₊ : ℝ) ≤ (↑(π ⌊x⌋₊) : ℝ) * log x
Tactic: rcases lt_or_ge x 1 with h | h
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
h : 1 ≤ x
⊢ (↑(π ⌊x⌋₊) : ℝ) * log (↑⌊x⌋₊ : ℝ) ≤ (↑(π ⌊x⌋₊) : ℝ) * log x
have inr : LT.lt (α := ℝ) 0 (↑⌊x⌋₊ : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
h : 1 ≤ x
inr : LT.lt (α := ℝ) 0 (↑⌊x⌋₊ : ℝ)
⊢ (↑(π ⌊x⌋₊) : ℝ) * log (↑⌊x⌋₊ : ℝ) ≤ (↑(π ⌊x⌋₊) : ℝ) * log x
have inr₁ : (↑⌊x⌋₊ : ℝ) ≤ x
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
n : ℕ
⊢ ψ (↑n : ℝ) = log (↑n.lcmUpto : ℝ)
have rw : ψ (↑n : ℝ) = ∑ i ∈ n.primesLE, log (↑(i ^ Nat.log i n) : ℝ)
Tactic: rw [lcmUpto_eq_prod_pow_log, cast_prod, log_prod (by simp +contextual)]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
n k : ℕ
hkn : k ≤ n
⊢ n.choose k ∣ n.lcmUpto
have rw : ∀ (p : ℕ),
  Nat.Prime p →
    LE.le (α := ℕ) (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ) ((n.lcmUpto.factorization : (a : ℕ) → ℕ) p : ℕ)
Tactic: rw [← factorization_prime_le_iff_dvd (choose_ne_zero hkn) (lcmUpto_ne_zero n)]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
n k : ℕ
hkn : k ≤ n
p : ℕ
hp : Nat.Prime p
⊢ LE.le (α := ℕ) (((n.choose k).factorization : (a : ℕ) → ℕ) p : ℕ) ((n.lcmUpto.factorization : (a : ℕ) → ℕ) p : ℕ)
have rw : ((n.choose k).factorization : (a : ℕ) → ℕ) p ≤ Nat.log p n
Tactic: rw [factorization_lcmUpto n hp]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
n : ℕ
⊢ LE.le (α := ℕ) (∑ m ∈ range (n + 1), n.choose m) (∑ k ∈ range (n + 1), n.lcmUpto)
have h : ∀ (k : ℕ) (hk : k ∈ range (n + 1)), n.choose k ≤ n.lcmUpto
Tactic: gcongr with k hk
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
R : Type u_1
inst : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
⊢ Eq.{u_1 + 1} (α := R) (∑ n ∈ Ioc 0 ⌊x⌋₊ with IsPrimePow n, f n)
    (∑ k ∈ Icc 1 ⌊log x / log 2⌋₊, ∑ p ∈ Ioc 0 ⌊x ^ HDiv.hDiv (α := ℝ) 1 (↑k : ℝ)⌋₊ with Nat.Prime p, f (p ^ k))
have trans : Eq.{u_1 + 1} (α := R) (∑ n ∈ Ioc 0 ⌊x⌋₊ with IsPrimePow n, f n)
  (∑ 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))
Tactic: trans ∑ ⟨k, p⟩ ∈ Icc 1 ⌊log x / log 2⌋₊ ×ˢ (Ioc 0 ⌊x⌋₊).filter Nat.Prime
    with p ≤ ⌊x ^ (k : ℝ)⁻¹⌋₊, f (p ^ k)
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
R : Type u_1
inst : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
trans :
  Eq.{u_1 + 1} (α := R) (∑ n ∈ Ioc 0 ⌊x⌋₊ with IsPrimePow n, f n)
    (∑ 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))
⊢ Eq.{u_1 + 1} (α := R) (∑ n ∈ Ioc 0 ⌊x⌋₊ with IsPrimePow n, f n)
    (∑ k ∈ Icc 1 ⌊log x / log 2⌋₊, ∑ p ∈ Ioc 0 ⌊x ^ HDiv.hDiv (α := ℝ) 1 (↑k : ℝ)⌋₊ with Nat.Prime p, f (p ^ k))
have trans₁ : 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: trans ∑ ⟨k, p⟩ ∈ Icc 1 ⌊log x / log 2⌋₊ ×ˢ (Ioc 0 ⌊x⌋₊).filter Nat.Prime
    with p ≤ ⌊x ^ (k : ℝ)⁻¹⌋₊, f (p ^ k)
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
R : Type u_1
inst : AddCommMonoid R
f : ℕ → R
x : ℝ
hx : 0 ≤ x
⊢ Eq.{u_1 + 1} (α := R) (∑ n ∈ Ioc 0 ⌊x⌋₊ with IsPrimePow n, f n)
    (∑ 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))
have refine_1 : ∀ (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 : ℝ)⁻¹⌋₊}),
  (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 ∈
    {n ∈ Ioc 0 ⌊x⌋₊ | IsPrimePow n}
Tactic: refine (sum_bij (i := fun ⟨k, p⟩ _ ↦ p ^ k) ?_ ?_ ?_ ?_).symm