awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (goal)
Goal:
n : ℕ
n_large : 2 < n
no_prime : ∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p
n_pos : 0 < n
n2_pos : 1 ≤ 2 * n
S : Finset ℕ := {p ∈ Finset.range (2 * n / 3 + 1) | Nat.Prime p}
f : (x : ℕ) → ℕ := fun (x : ℕ) ↦ HPow.hPow (β := ℕ) x ((n.centralBinom.factorization : (a : ℕ) → ℕ) x : ℕ)
this : Eq (α := ℕ) (∏ x ∈ S, f x) (∏ x ∈ Finset.range (2 * n / 3 + 1), f x)
⊢ ∏ x ∈ S with x ≤ (2 * n).sqrt, f x ≤ (2 * n) ^ (2 * n).sqrt
have h₁ : ∀ p ∈ {x ∈ S | x ≤ (2 * n).sqrt}, f p ≤ 2 * n
Tactic: refine (Finset.prod_le_prod' fun p _ => (?_ : f p ≤ 2 * n)).trans ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (goal)
Goal:
n : ℕ
n_large : 2 < n
no_prime : ∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p
n_pos : 0 < n
n2_pos : 1 ≤ 2 * n
S : Finset ℕ := {p ∈ Finset.range (2 * n / 3 + 1) | Nat.Prime p}
f : (x : ℕ) → ℕ := fun (x : ℕ) ↦ HPow.hPow (β := ℕ) x ((n.centralBinom.factorization : (a : ℕ) → ℕ) x : ℕ)
this : Eq (α := ℕ) (∏ x ∈ S, f x) (∏ x ∈ Finset.range (2 * n / 3 + 1), f x)
h₁ : ∀ p ∈ {x ∈ S | x ≤ (2 * n).sqrt}, f p ≤ 2 * n
⊢ ∏ x ∈ S with x ≤ (2 * n).sqrt, f x ≤ (2 * n) ^ (2 * n).sqrt
have h₂ : ∏ i ∈ S with i ≤ (2 * n).sqrt, 2 * n ≤ (2 * n) ^ (2 * n).sqrt
Tactic: refine (Finset.prod_le_prod' fun p _ => (?_ : f p ≤ 2 * n)).trans ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (goal)
Goal:
n : ℕ
n_large : 2 < n
no_prime : ∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p
n_pos : 0 < n
n2_pos : 1 ≤ 2 * n
S : Finset ℕ := {p ∈ Finset.range (2 * n / 3 + 1) | Nat.Prime p}
f : (x : ℕ) → ℕ := fun (x : ℕ) ↦ HPow.hPow (β := ℕ) x ((n.centralBinom.factorization : (a : ℕ) → ℕ) x : ℕ)
this : Eq (α := ℕ) (∏ x ∈ S, f x) (∏ x ∈ Finset.range (2 * n / 3 + 1), f x)
⊢ (Finset.Icc 1 (2 * n).sqrt).card = (2 * n).sqrt
have rw : (2 * n).sqrt + 1 - 1 = (2 * n).sqrt
Tactic: rw [card_Icc, Nat.add_sub_cancel]
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (goal)
Goal:
n : ℕ
n_large : 2 < n
no_prime : ∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p
n_pos : 0 < n
n2_pos : 1 ≤ 2 * n
S : Finset ℕ := {p ∈ Finset.range (2 * n / 3 + 1) | Nat.Prime p}
f : (x : ℕ) → ℕ := fun (x : ℕ) ↦ HPow.hPow (β := ℕ) x ((n.centralBinom.factorization : (a : ℕ) → ℕ) x : ℕ)
this : Eq (α := ℕ) (∏ x ∈ S, f x) (∏ x ∈ Finset.range (2 * n / 3 + 1), f x)
rw : (2 * n).sqrt + 1 - 1 = (2 * n).sqrt
⊢ (Finset.Icc 1 (2 * n).sqrt).card = (2 * n).sqrt
have rw₁ : (2 * n).sqrt = (2 * n).sqrt
Tactic: rw [card_Icc, Nat.add_sub_cancel]
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (hypothesis)
Goal:
n : ℕ
n_large : 2 < n
no_prime : ∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p
n_pos : 0 < n
n2_pos : 1 ≤ 2 * n
S : Finset ℕ := {p ∈ Finset.range (2 * n / 3 + 1) | Nat.Prime p}
f : (x : ℕ) → ℕ := fun (x : ℕ) ↦ HPow.hPow (β := ℕ) x ((n.centralBinom.factorization : (a : ℕ) → ℕ) x : ℕ)
this : Eq (α := ℕ) (∏ x ∈ S, f x) (∏ x ∈ Finset.range (2 * n / 3 + 1), f x)
⊢ ∏ i ∈ S with i ≤ (2 * n).sqrt, 2 * n ≤ (2 * n) ^ (2 * n).sqrt
have this₁ : (Finset.Icc 1 (2 * n).sqrt).card = (2 * n).sqrt
Tactic: have : (Finset.Icc 1 (sqrt (2 * n))).card = sqrt (2 * n) := by rw [card_Icc, Nat.add_sub_cancel]
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (goal)
Goal:
n : ℕ
n_large : 2 < n
no_prime : ∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p
n_pos : 0 < n
n2_pos : 1 ≤ 2 * n
S : Finset ℕ := {p ∈ Finset.range (2 * n / 3 + 1) | Nat.Prime p}
f : (x : ℕ) → ℕ := fun (x : ℕ) ↦ HPow.hPow (β := ℕ) x ((n.centralBinom.factorization : (a : ℕ) → ℕ) x : ℕ)
this_1 : Eq (α := ℕ) (∏ x ∈ S, f x) (∏ x ∈ Finset.range (2 * n / 3 + 1), f x)
this : (Finset.Icc 1 (2 * n).sqrt).card = (2 * n).sqrt
⊢ ∏ i ∈ S with i ≤ (2 * n).sqrt, 2 * n ≤ (2 * n) ^ (2 * n).sqrt
have h₁ : (2 * n) ^ {x ∈ S | x ≤ (2 * n).sqrt}.card ≤ (2 * n) ^ (2 * n).sqrt
Tactic: rw [Finset.prod_const]
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (goal)
Goal:
n : ℕ
n_large : 2 < n
no_prime : ∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p
n_pos : 0 < n
n2_pos : 1 ≤ 2 * n
S : Finset ℕ := {p ∈ Finset.range (2 * n / 3 + 1) | Nat.Prime p}
f : (x : ℕ) → ℕ := fun (x : ℕ) ↦ HPow.hPow (β := ℕ) x ((n.centralBinom.factorization : (a : ℕ) → ℕ) x : ℕ)
this_1 : Eq (α := ℕ) (∏ x ∈ S, f x) (∏ x ∈ Finset.range (2 * n / 3 + 1), f x)
this : (Finset.Icc 1 (2 * n).sqrt).card = (2 * n).sqrt
⊢ (2 * n) ^ {x ∈ S | x ≤ (2 * n).sqrt}.card ≤ (2 * n) ^ (2 * n).sqrt
have h₁ : ∀ (x : ℕ) (hx : x ∈ {x ∈ S | x ≤ (2 * n).sqrt}), x ∈ Finset.Icc 1 (2 * n).sqrt
Tactic: refine pow_right_mono₀ n2_pos ((Finset.card_le_card fun x hx => ?_).trans this.le)
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (hypothesis)
Goal:
n : ℕ
n_large : 2 < n
no_prime : ∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p
n_pos : 0 < n
n2_pos : 1 ≤ 2 * n
S : Finset ℕ := {p ∈ Finset.range (2 * n / 3 + 1) | Nat.Prime p}
f : (x : ℕ) → ℕ := fun (x : ℕ) ↦ HPow.hPow (β := ℕ) x ((n.centralBinom.factorization : (a : ℕ) → ℕ) x : ℕ)
this_1 : Eq (α := ℕ) (∏ x ∈ S, f x) (∏ x ∈ Finset.range (2 * n / 3 + 1), f x)
this : (Finset.Icc 1 (2 * n).sqrt).card = (2 * n).sqrt
x : ℕ
hx : x ∈ {x ∈ S | x ≤ (2 * n).sqrt}
⊢ x ∈ Finset.Icc 1 (2 * n).sqrt
have h1 : x ∈ S
Tactic: obtain ⟨h1, h2⟩ := Finset.mem_filter.1 hx
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (hypothesis)
Goal:
n : ℕ
n_large : 2 < n
no_prime : ∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p
n_pos : 0 < n
n2_pos : 1 ≤ 2 * n
S : Finset ℕ := {p ∈ Finset.range (2 * n / 3 + 1) | Nat.Prime p}
f : (x : ℕ) → ℕ := fun (x : ℕ) ↦ HPow.hPow (β := ℕ) x ((n.centralBinom.factorization : (a : ℕ) → ℕ) x : ℕ)
this_1 : Eq (α := ℕ) (∏ x ∈ S, f x) (∏ x ∈ Finset.range (2 * n / 3 + 1), f x)
this : (Finset.Icc 1 (2 * n).sqrt).card = (2 * n).sqrt
x : ℕ
hx : x ∈ {x ∈ S | x ≤ (2 * n).sqrt}
h1 : x ∈ S
⊢ x ∈ Finset.Icc 1 (2 * n).sqrt
have h2 : x ≤ (2 * n).sqrt
Tactic: obtain ⟨h1, h2⟩ := Finset.mem_filter.1 hx
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (goal)
Goal:
n : ℕ
n_large : 2 < n
no_prime : ∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p
n_pos : 0 < n
n2_pos : 1 ≤ 2 * n
S : Finset ℕ := {p ∈ Finset.range (2 * n / 3 + 1) | Nat.Prime p}
f : (x : ℕ) → ℕ := fun (x : ℕ) ↦ HPow.hPow (β := ℕ) x ((n.centralBinom.factorization : (a : ℕ) → ℕ) x : ℕ)
this : Eq (α := ℕ) (∏ x ∈ S, f x) (∏ x ∈ Finset.range (2 * n / 3 + 1), f x)
⊢ ∏ x ∈ S with ¬x ≤ (2 * n).sqrt, f x ≤ HPow.hPow (α := ℕ) 4 (2 * n / 3)
have h₂ : ∏ x ∈ S with ¬x ≤ (2 * n).sqrt, f x ≤ primorial (2 * n / 3)
Tactic: refine le_trans ?_ (primorial_le_four_pow (2 * n / 3))
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (goal)
Goal:
n : ℕ
n_large : 2 < n
no_prime : ∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p
n_pos : 0 < n
n2_pos : 1 ≤ 2 * n
S : Finset ℕ := {p ∈ Finset.range (2 * n / 3 + 1) | Nat.Prime p}
f : (x : ℕ) → ℕ := fun (x : ℕ) ↦ HPow.hPow (β := ℕ) x ((n.centralBinom.factorization : (a : ℕ) → ℕ) x : ℕ)
this : Eq (α := ℕ) (∏ x ∈ S, f x) (∏ x ∈ Finset.range (2 * n / 3 + 1), f x)
⊢ ∏ x ∈ S with ¬x ≤ (2 * n).sqrt, f x ≤ primorial (2 * n / 3)
have h₂ : ∀ (p : ℕ) (hp : p ∈ {x ∈ S | ¬x ≤ (2 * n).sqrt}), f p ≤ p
Tactic: refine (Finset.prod_le_prod' fun p hp => (?_ : f p ≤ p)).trans ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (goal)
Goal:
n : ℕ
n_large : 2 < n
no_prime : ∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p
n_pos : 0 < n
n2_pos : 1 ≤ 2 * n
S : Finset ℕ := {p ∈ Finset.range (2 * n / 3 + 1) | Nat.Prime p}
f : (x : ℕ) → ℕ := fun (x : ℕ) ↦ HPow.hPow (β := ℕ) x ((n.centralBinom.factorization : (a : ℕ) → ℕ) x : ℕ)
this : Eq (α := ℕ) (∏ x ∈ S, f x) (∏ x ∈ Finset.range (2 * n / 3 + 1), f x)
h₂ : ∀ (p : ℕ) (hp : p ∈ {x ∈ S | ¬x ≤ (2 * n).sqrt}), f p ≤ p
⊢ ∏ x ∈ S with ¬x ≤ (2 * n).sqrt, f x ≤ primorial (2 * n / 3)
have h₃ : ∏ i ∈ S with ¬i ≤ (2 * n).sqrt, i ≤ primorial (2 * n / 3)
Tactic: refine (Finset.prod_le_prod' fun p hp => (?_ : f p ≤ p)).trans ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (hypothesis)
Goal:
n : ℕ
n_large : 2 < n
no_prime : ∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p
n_pos : 0 < n
n2_pos : 1 ≤ 2 * n
S : Finset ℕ := {p ∈ Finset.range (2 * n / 3 + 1) | Nat.Prime p}
f : (x : ℕ) → ℕ := fun (x : ℕ) ↦ HPow.hPow (β := ℕ) x ((n.centralBinom.factorization : (a : ℕ) → ℕ) x : ℕ)
this : Eq (α := ℕ) (∏ x ∈ S, f x) (∏ x ∈ Finset.range (2 * n / 3 + 1), f x)
p : ℕ
hp : p ∈ {x ∈ S | ¬x ≤ (2 * n).sqrt}
⊢ f p ≤ p
have h1 : p ∈ S
Tactic: obtain ⟨h1, h2⟩ := Finset.mem_filter.1 hp
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (hypothesis)
Goal:
n : ℕ
n_large : 2 < n
no_prime : ∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p
n_pos : 0 < n
n2_pos : 1 ≤ 2 * n
S : Finset ℕ := {p ∈ Finset.range (2 * n / 3 + 1) | Nat.Prime p}
f : (x : ℕ) → ℕ := fun (x : ℕ) ↦ HPow.hPow (β := ℕ) x ((n.centralBinom.factorization : (a : ℕ) → ℕ) x : ℕ)
this : Eq (α := ℕ) (∏ x ∈ S, f x) (∏ x ∈ Finset.range (2 * n / 3 + 1), f x)
p : ℕ
hp : p ∈ {x ∈ S | ¬x ≤ (2 * n).sqrt}
h1 : p ∈ S
⊢ f p ≤ p
have h2 : ¬p ≤ (2 * n).sqrt
Tactic: obtain ⟨h1, h2⟩ := Finset.mem_filter.1 hp
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (goal)
Goal:
n : ℕ
n_large : 2 < n
no_prime : ∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p
n_pos : 0 < n
n2_pos : 1 ≤ 2 * n
S : Finset ℕ := {p ∈ Finset.range (2 * n / 3 + 1) | Nat.Prime p}
f : (x : ℕ) → ℕ := fun (x : ℕ) ↦ HPow.hPow (β := ℕ) x ((n.centralBinom.factorization : (a : ℕ) → ℕ) x : ℕ)
this : Eq (α := ℕ) (∏ x ∈ S, f x) (∏ x ∈ Finset.range (2 * n / 3 + 1), f x)
p : ℕ
hp : p ∈ {x ∈ S | ¬x ≤ (2 * n).sqrt}
h1 : p ∈ S
h2 : ¬p ≤ (2 * n).sqrt
⊢ f p ≤ p
have h₂ : LE.le (α := ℕ) ((n.centralBinom.factorization : (a : ℕ) → ℕ) p : ℕ) (1 : ℕ)
Tactic: refine (pow_right_mono₀ (Finset.mem_filter.1 h1).2.one_lt.le ?_).trans (pow_one p).le
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (goal)
Goal:
n : ℕ
n_large : 2 < n
no_prime : ∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p
n_pos : 0 < n
n2_pos : 1 ≤ 2 * n
S : Finset ℕ := {p ∈ Finset.range (2 * n / 3 + 1) | Nat.Prime p}
f : (x : ℕ) → ℕ := fun (x : ℕ) ↦ HPow.hPow (β := ℕ) x ((n.centralBinom.factorization : (a : ℕ) → ℕ) x : ℕ)
this : Eq (α := ℕ) (∏ x ∈ S, f x) (∏ x ∈ Finset.range (2 * n / 3 + 1), f x)
⊢ ∏ i ∈ S with ¬i ≤ (2 * n).sqrt, i ≤ primorial (2 * n / 3)
have h₂ : ∀ i ∈ {p ∈ Finset.range (2 * n / 3 + 1) | Nat.Prime p}, i ∉ {x ∈ S | ¬x ≤ (2 * n).sqrt} → 1 ≤ i
Tactic: refine Finset.prod_le_prod_of_subset_of_one_le' (Finset.filter_subset _ _) ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (hypothesis)
Goal:
n : ℕ
n_large : 512 ≤ n
⊢ ∃ (p : ℕ), Prime p ∧ n < p ∧ p ≤ 2 * n
have no_prime : HPow.hPow (α := ℕ) 4 n < n * n.centralBinom
Tactic: have no_prime : 4 ^ n < n * n.centralBinom :=
    Nat.four_pow_lt_mul_centralBinom n (le_trans (by norm_num1) n_large)
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (goal)
Goal:
n : ℕ
n_large : 512 ≤ n
no_prime : HPow.hPow (α := ℕ) 4 n < n * n.centralBinom
⊢ ∃ (p : ℕ), Prime p ∧ n < p ∧ p ≤ 2 * n
have contrapose! : ∀ (no_prime : ∀ (p : ℕ) (_ : Prime p) (_ : n < p), 2 * n < p), n * n.centralBinom ≤ HPow.hPow (α := ℕ) 4 n
Tactic: contrapose! no_prime
Cleared hypotheses: no_prime
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (hypothesis)
Goal:
n : ℕ
n_large : 512 ≤ n
no_prime : ∀ (p : ℕ) (_ : Prime p) (_ : n < p), 2 * n < p
⊢ n * n.centralBinom ≤ HPow.hPow (α := ℕ) 4 n
have this : n.centralBinom ≤ (2 * n) ^ (2 * n).sqrt * HPow.hPow (α := ℕ) 4 (2 * n / 3)
Tactic: have : n.centralBinom ≤ (2 * n) ^ sqrt (2 * n) * 4 ^ (2 * n / 3) :=
    centralBinom_le_of_no_bertrand_prime n (lt_of_lt_of_le (by norm_num1) n_large) no_prime
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (goal)
Goal:
n : ℕ
n_large : 512 ≤ n
no_prime : ∀ (p : ℕ) (_ : Prime p) (_ : n < p), 2 * n < p
this : n.centralBinom ≤ (2 * n) ^ (2 * n).sqrt * HPow.hPow (α := ℕ) 4 (2 * n / 3)
⊢ n * n.centralBinom ≤ HPow.hPow (α := ℕ) 4 n
have grw : n * ((2 * n) ^ (2 * n).sqrt * HPow.hPow (α := ℕ) 4 (2 * n / 3)) ≤ HPow.hPow (α := ℕ) 4 n
Tactic: grw [this, ← mul_assoc, bertrand_main_inequality n_large]
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (goal)
Goal:
n : ℕ
n_large : 512 ≤ n
no_prime : ∀ (p : ℕ) (_ : Prime p) (_ : n < p), 2 * n < p
this : n.centralBinom ≤ (2 * n) ^ (2 * n).sqrt * HPow.hPow (α := ℕ) 4 (2 * n / 3)
grw : n * ((2 * n) ^ (2 * n).sqrt * HPow.hPow (α := ℕ) 4 (2 * n / 3)) ≤ HPow.hPow (α := ℕ) 4 n
⊢ n * n.centralBinom ≤ HPow.hPow (α := ℕ) 4 n
have grw₁ : n * (2 * n) ^ (2 * n).sqrt * HPow.hPow (α := ℕ) 4 (2 * n / 3) ≤ HPow.hPow (α := ℕ) 4 n
Tactic: grw [this, ← mul_assoc, bertrand_main_inequality n_large]
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (goal)
Goal:
n : ℕ
n_large : 512 ≤ n
no_prime : ∀ (p : ℕ) (_ : Prime p) (_ : n < p), 2 * n < p
this : n.centralBinom ≤ (2 * n) ^ (2 * n).sqrt * HPow.hPow (α := ℕ) 4 (2 * n / 3)
grw : n * ((2 * n) ^ (2 * n).sqrt * HPow.hPow (α := ℕ) 4 (2 * n / 3)) ≤ HPow.hPow (α := ℕ) 4 n
grw₁ : n * (2 * n) ^ (2 * n).sqrt * HPow.hPow (α := ℕ) 4 (2 * n / 3) ≤ HPow.hPow (α := ℕ) 4 n
⊢ n * n.centralBinom ≤ HPow.hPow (α := ℕ) 4 n
have grw₂ : HPow.hPow (α := ℕ) 4 n ≤ HPow.hPow (α := ℕ) 4 n
Tactic: grw [this, ← mul_assoc, bertrand_main_inequality n_large]
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (goal)
Goal:
n : ℕ
hn0 : n ≠ 0
⊢ ∃ (p : ℕ), Prime p ∧ n < p ∧ p ≤ 2 * n
have inl : ∀ (h : 511 < n), ∃ (p : ℕ), Prime p ∧ n < p ∧ p ≤ 2 * n
Tactic: rcases lt_or_ge 511 n with h | h
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (goal)
Goal:
n : ℕ
hn0 : n ≠ 0
inl : ∀ (h : 511 < n), ∃ (p : ℕ), Prime p ∧ n < p ∧ p ≤ 2 * n
⊢ ∃ (p : ℕ), Prime p ∧ n < p ∧ p ≤ 2 * n
have inr : ∀ (h : n ≤ 511), ∃ (p : ℕ), Prime p ∧ n < p ∧ p ≤ 2 * n
Tactic: rcases lt_or_ge 511 n with h | h
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (hypothesis)
Goal:
n : ℕ
hn0 : n ≠ 0
h : n ≤ 511
⊢ ∃ (p : ℕ), Prime p ∧ n < p ∧ p ≤ 2 * n
have h₁ : n < 521
Tactic: replace h : n < 521 := h.trans_lt (by norm_num1)
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (goal)
Goal:
n : ℕ
hn0 : n ≠ 0
h : n < 521
⊢ ∃ (p : ℕ), Prime p ∧ n < p ∧ p ≤ 2 * n
have inr : ∀ (h : n < 521), ∃ (p : ℕ), Prime p ∧ n < p ∧ p ≤ 2 * n
Tactic: revert h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hy : 2 ≤ x
⊢ 0 < θ x
have refine_1 : ∀ (n : ℕ) (hn : n ∈ {p ∈ Ioc 0 ⌊x⌋₊ | Nat.Prime p}), LT.lt (α := ℝ) 1 (↑n : ℝ)
Tactic: refine sum_pos (fun n hn ↦ log_pos ?_) ⟨2, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hy : 2 ≤ x
refine_1 : ∀ (n : ℕ) (hn : n ∈ {p ∈ Ioc 0 ⌊x⌋₊ | Nat.Prime p}), LT.lt (α := ℝ) 1 (↑n : ℝ)
⊢ 0 < θ x
have refine_2 : 2 ∈ {p ∈ Ioc 0 ⌊x⌋₊ | Nat.Prime p}
Tactic: refine sum_pos (fun n hn ↦ log_pos ?_) ⟨2, ?_⟩
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (hypothesis)
Goal:
x : ℝ
hy : 2 ≤ x
n : ℕ
hn : n ∈ {p ∈ Ioc 0 ⌊x⌋₊ | Nat.Prime p}
⊢ LT.lt (α := ℝ) 1 (↑n : ℝ)
have hn₁ : n ∈ Ioc 0 ⌊x⌋₊ ∧ Nat.Prime n
Tactic: simp only [mem_filter] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (hypothesis)
Goal:
x : ℝ
hy : 2 ≤ x
⊢ 2 ∈ {p ∈ Ioc 0 ⌊x⌋₊ | Nat.Prime p}
have this : 0 ≤ x
Tactic: have : 0 ≤ x := by grind
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
⊢ ψ x = ∑ n ∈ Icc 0 ⌊x⌋₊, (Λ : (a : ℕ) → ℝ) n
have rw : ∑ n ∈ Ioc 0 ⌊x⌋₊, (Λ : (a : ℕ) → ℝ) n =
  HAdd.hAdd (α := ℝ) (β := ℝ) ((Λ : (a : ℕ) → ℝ) 0 : ℝ) (∑ x ∈ Ioc 0 ⌊x⌋₊, (Λ : (a : ℕ) → ℝ) x : ℝ)
Tactic: rw [psi, ← add_sum_Ioc_eq_sum_Icc]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
rw :
  ∑ n ∈ Ioc 0 ⌊x⌋₊, (Λ : (a : ℕ) → ℝ) n =
    HAdd.hAdd (α := ℝ) (β := ℝ) ((Λ : (a : ℕ) → ℝ) 0 : ℝ) (∑ x ∈ Ioc 0 ⌊x⌋₊, (Λ : (a : ℕ) → ℝ) x : ℝ)
⊢ ψ x = ∑ n ∈ Icc 0 ⌊x⌋₊, (Λ : (a : ℕ) → ℝ) n
have rw₁ : 0 ≤ ⌊x⌋₊
Tactic: rw [psi, ← add_sum_Ioc_eq_sum_Icc]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
⊢ θ x = ∑ p ∈ Icc 0 ⌊x⌋₊ with Nat.Prime p, log (↑p : ℝ)
have rw : (∑ a ∈ Ioc 0 ⌊x⌋₊, if Nat.Prime a then log (↑a : ℝ) else 0) =
  (if Nat.Prime 0 then log (↑0 : ℝ) else 0) + ∑ x ∈ Ioc 0 ⌊x⌋₊, if Nat.Prime x then log (↑x : ℝ) else 0
Tactic: rw [theta, sum_filter, sum_filter, ← add_sum_Ioc_eq_sum_Icc]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
rw :
  (∑ a ∈ Ioc 0 ⌊x⌋₊, if Nat.Prime a then log (↑a : ℝ) else 0) =
    (if Nat.Prime 0 then log (↑0 : ℝ) else 0) + ∑ x ∈ Ioc 0 ⌊x⌋₊, if Nat.Prime x then log (↑x : ℝ) else 0
⊢ θ x = ∑ p ∈ Icc 0 ⌊x⌋₊ with Nat.Prime p, log (↑p : ℝ)
have rw₁ : 0 ≤ ⌊x⌋₊
Tactic: rw [theta, sum_filter, sum_filter, ← add_sum_Ioc_eq_sum_Icc]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : x < 2
⊢ ψ x = 0
have apply : ∀ (n : ℕ) (hn : n ∈ Ioc 0 ⌊x⌋₊), Eq (α := ℝ) ((Λ : (a : ℕ) → ℝ) n : ℝ) (0 : ℝ)
Tactic: apply sum_eq_zero fun n hn ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (hypothesis)
Goal:
x : ℝ
hx : x < 2
n : ℕ
hn : n ∈ Ioc 0 ⌊x⌋₊
⊢ Eq (α := ℝ) ((Λ : (a : ℕ) → ℝ) n : ℝ) (0 : ℝ)
have hn₁ : 0 < n ∧ n ≤ ⌊x⌋₊
Tactic: simp only [mem_Ioc] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : x < 2
n : ℕ
hn : 0 < n ∧ n ≤ ⌊x⌋₊
⊢ Eq (α := ℝ) ((Λ : (a : ℕ) → ℝ) n : ℝ) (0 : ℝ)
have h : n = 1
Tactic: convert! vonMangoldt_apply_one
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (hypothesis)
Goal:
x : ℝ
hx : x < 2
n : ℕ
hn : 0 < n ∧ n ≤ ⌊x⌋₊
⊢ n = 1
have this : LT.lt (α := ℝ) (↑n : ℝ) 2
Tactic: have := lt_of_le_of_lt (le_floor_iff' hn.1.ne' |>.mp hn.2) hx
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (hypothesis)
Goal:
x : ℝ
hx : x < 2
n : ℕ
hn : 0 < n ∧ n ≤ ⌊x⌋₊
this : LT.lt (α := ℝ) (↑n : ℝ) 2
⊢ n = 1
have this₁ : n < 2
Tactic: norm_cast at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : x < 2
n : ℕ
hn : 0 < n ∧ n ≤ ⌊x⌋₊
this : n < 2
⊢ n = 1
have linarith : n < 1 → -1 + (HAdd.hAdd (α := ℤ) 0 1 - (↑n : ℤ)) + (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 1) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : x < 2
n : ℕ
hn : 0 < n ∧ n ≤ ⌊x⌋₊
this : n < 2
linarith : n < 1 → -1 + (HAdd.hAdd (α := ℤ) 0 1 - (↑n : ℤ)) + (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 1) = 0
⊢ n = 1
have linarith₁ : 1 < n → -1 + (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 2) + (HAdd.hAdd (α := ℤ) 1 1 - (↑n : ℤ)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : x < 2
⊢ θ x = 0
have apply : ∀ (n : ℕ) (hn : n ∈ {p ∈ Ioc 0 ⌊x⌋₊ | Nat.Prime p}), log (↑n : ℝ) = 0
Tactic: apply sum_eq_zero fun n hn ↦ ?_
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : x < 2
n : ℕ
hn : n ∈ {p ∈ Ioc 0 ⌊x⌋₊ | Nat.Prime p}
⊢ log (↑n : ℝ) = 0
have h : Eq (α := ℝ) (↑n : ℝ) 1
Tactic: convert! log_one
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (hypothesis)
Goal:
x : ℝ
hx : x < 2
n : ℕ
hn : n ∈ {p ∈ Ioc 0 ⌊x⌋₊ | Nat.Prime p}
⊢ Eq (α := ℝ) (↑n : ℝ) 1
have hn₁ : (0 < n ∧ n ≤ ⌊x⌋₊) ∧ Nat.Prime n
Tactic: simp only [mem_filter, mem_Ioc] at hn
Cleared hypotheses: hn
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (hypothesis)
Goal:
x : ℝ
hx : x < 2
n : ℕ
hn : (0 < n ∧ n ≤ ⌊x⌋₊) ∧ Nat.Prime n
⊢ Eq (α := ℝ) (↑n : ℝ) 1
have this : LT.lt (α := ℝ) (↑n : ℝ) 2
Tactic: have := lt_of_le_of_lt (le_floor_iff' hn.1.1.ne' |>.mp hn.1.2) hx
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : x < 2
n : ℕ
hn : (0 < n ∧ n ≤ ⌊x⌋₊) ∧ Nat.Prime n
this : LT.lt (α := ℝ) (↑n : ℝ) 2
⊢ Eq (α := ℝ) (↑n : ℝ) 1
have h : ∀ (this : n < 2), n = 1
Tactic: norm_cast at ⊢ this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : x < 2
n : ℕ
hn : (0 < n ∧ n ≤ ⌊x⌋₊) ∧ Nat.Prime n
this : n < 2
⊢ n = 1
have linarith : n < 1 → -1 + (HAdd.hAdd (α := ℤ) 0 1 - (↑n : ℤ)) + (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 1) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : x < 2
n : ℕ
hn : (0 < n ∧ n ≤ ⌊x⌋₊) ∧ Nat.Prime n
this : n < 2
linarith : n < 1 → -1 + (HAdd.hAdd (α := ℤ) 0 1 - (↑n : ℤ)) + (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 1) = 0
⊢ n = 1
have linarith₁ : 1 < n → -1 + (HAdd.hAdd (α := ℤ) (↑n : ℤ) 1 - 2) + (HAdd.hAdd (α := ℤ) 1 1 - (↑n : ℤ)) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
⊢ Eq (α := ℝ) (∑ n ∈ Ioc 0 ⌊x⌋₊, (Λ : (a : ℕ) → ℝ) n) (∑ n ∈ Ioc 0 (floor (α := ℝ) (↑⌊x⌋₊ : ℝ)), (Λ : (a : ℕ) → ℝ) n)
have rw : Eq (α := ℝ) (∑ n ∈ Ioc 0 ⌊x⌋₊, (Λ : (a : ℕ) → ℝ) n) (∑ n ∈ Ioc 0 ⌊x⌋₊, (Λ : (a : ℕ) → ℝ) n)
Tactic: rw [floor_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
⊢ Eq (α := ℝ) (∑ p ∈ Ioc 0 ⌊x⌋₊ with Nat.Prime p, log (↑p : ℝ))
    (∑ p ∈ Ioc 0 (floor (α := ℝ) (↑⌊x⌋₊ : ℝ)) with Nat.Prime p, log (↑p : ℝ))
have rw : Eq (α := ℝ) (∑ p ∈ Ioc 0 ⌊x⌋₊ with Nat.Prime p, log (↑p : ℝ)) (∑ p ∈ Ioc 0 ⌊x⌋₊ with Nat.Prime p, log (↑p : ℝ))
Tactic: rw [floor_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x y : ℝ
hxy : x ≤ y
⊢ ψ x ≤ ψ y
have h : Ioc 0 ⌊x⌋₊ ⊆ Ioc 0 ⌊y⌋₊
Tactic: apply sum_le_sum_of_subset_of_nonneg
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x y : ℝ
hxy : x ≤ y
h : Ioc 0 ⌊x⌋₊ ⊆ Ioc 0 ⌊y⌋₊
⊢ ψ x ≤ ψ y
have hf : ∀ i ∈ Ioc 0 ⌊y⌋₊, i ∉ Ioc 0 ⌊x⌋₊ → LE.le (α := ℝ) (0 : ℝ) ((Λ : (a : ℕ) → ℝ) i : ℝ)
Tactic: apply sum_le_sum_of_subset_of_nonneg
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x y : ℝ
hxy : x ≤ y
⊢ θ x ≤ θ y
have h : {p ∈ Ioc 0 ⌊x⌋₊ | Nat.Prime p} ⊆ {p ∈ Ioc 0 ⌊y⌋₊ | Nat.Prime p}
Tactic: apply sum_le_sum_of_subset_of_nonneg
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x y : ℝ
hxy : x ≤ y
h : {p ∈ Ioc 0 ⌊x⌋₊ | Nat.Prime p} ⊆ {p ∈ Ioc 0 ⌊y⌋₊ | Nat.Prime p}
⊢ θ x ≤ θ y
have hf : ∀ i ∈ {p ∈ Ioc 0 ⌊y⌋₊ | Nat.Prime p}, i ∉ {p ∈ Ioc 0 ⌊x⌋₊ | Nat.Prime p} → 0 ≤ log (↑i : ℝ)
Tactic: apply sum_le_sum_of_subset_of_nonneg
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
⊢ ∑ p ∈ Ioc 0 ⌊x⌋₊ with Nat.Prime p, log (↑p : ℝ) = log (↑(∏ p ∈ range (⌊x⌋₊ + 1) with Nat.Prime p, p) : ℝ)
have rw : Eq (α := ℝ) (∑ p ∈ Ioc 0 ⌊x⌋₊ with Nat.Prime p, log (↑p : ℝ)) (∑ i ∈ range (⌊x⌋₊ + 1) with Nat.Prime i, log (↑i : ℝ))
Tactic: rw [cast_prod, log_prod (fun p hp ↦ mod_cast (mem_filter.mp hp).2.pos.ne')]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
⊢ Eq (α := ℝ) (∑ p ∈ Ioc 0 ⌊x⌋₊ with Nat.Prime p, log (↑p : ℝ)) (∑ i ∈ range (⌊x⌋₊ + 1) with Nat.Prime i, log (↑i : ℝ))
have e_s : ∀ (p : ℕ), p ∈ {p ∈ Ioc 0 ⌊x⌋₊ | Nat.Prime p} ↔ p ∈ {p ∈ range (⌊x⌋₊ + 1) | Nat.Prime p}
Tactic: congr 1 with p
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 0 ≤ x
⊢ θ x ≤ log 4 * x
have rw : log (↑(primorial ⌊x⌋₊) : ℝ) ≤ log 4 * x
Tactic: rw [theta_eq_log_primorial]
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 0 ≤ x
⊢ log (↑(primorial ⌊x⌋₊) : ℝ) ≤ log 4 * x
have trans : log (↑(primorial ⌊x⌋₊) : ℝ) ≤ log (HPow.hPow (α := ℝ) 4 ⌊x⌋₊)
Tactic: trans log (4 ^ ⌊x⌋₊)
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 0 ≤ x
trans : log (↑(primorial ⌊x⌋₊) : ℝ) ≤ log (HPow.hPow (α := ℝ) 4 ⌊x⌋₊)
⊢ log (↑(primorial ⌊x⌋₊) : ℝ) ≤ log 4 * x
have trans₁ : log (HPow.hPow (α := ℝ) 4 ⌊x⌋₊) ≤ log 4 * x
Tactic: trans log (4 ^ ⌊x⌋₊)
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 0 ≤ x
⊢ log (↑(primorial ⌊x⌋₊) : ℝ) ≤ log (HPow.hPow (α := ℝ) 4 ⌊x⌋₊)
have hx₁ : LT.lt (α := ℝ) 0 (↑(primorial ⌊x⌋₊) : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 0 ≤ x
hx₁ : LT.lt (α := ℝ) 0 (↑(primorial ⌊x⌋₊) : ℝ)
⊢ log (↑(primorial ⌊x⌋₊) : ℝ) ≤ log (HPow.hPow (α := ℝ) 4 ⌊x⌋₊)
have hxy : (↑(primorial ⌊x⌋₊) : ℝ) ≤ HPow.hPow (α := ℝ) 4 ⌊x⌋₊
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 0 ≤ x
⊢ LT.lt (α := ℝ) 0 (↑(primorial ⌊x⌋₊) : ℝ)
have hx₁ : 0 < primorial ⌊x⌋₊
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 0 ≤ x
⊢ (↑(primorial ⌊x⌋₊) : ℝ) ≤ HPow.hPow (α := ℝ) 4 ⌊x⌋₊
have hxy : primorial ⌊x⌋₊ ≤ HPow.hPow (α := ℕ) 4 ⌊x⌋₊
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.NumberTheory.Chebyshev (goal)
Goal:
x : ℝ
hx : 0 ≤ x
⊢ log (HPow.hPow (α := ℝ) 4 ⌊x⌋₊) ≤ log 4 * x
have rw : log 4 * (↑⌊x⌋₊ : ℝ) ≤ log 4 * x
Tactic: rw [Real.log_pow, mul_comm]