awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : √(HMul.hMul (α := ℝ) 2 512) = 32
refine_2 : LE.le (α := ℝ) 1 2
refine_2₁ : (↑(9 + HMul.hMul (α := ℕ) 10 32) : ℝ) ≤ 2 * (512 / 3)
⊢ HPow.hPow (α := ℝ) (β := ℝ) 2 (↑(9 + HMul.hMul (α := ℕ) 10 32) : ℝ) ≤ HPow.hPow (α := ℝ) 2 (2 * (512 / 3))

Tactic:
on_goal 1 => apply rpow_le_rpow_of_exponent_le

Premises used: Real.rpow_le_rpow_of_exponent_le
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : √(HMul.hMul (α := ℝ) 2 512) = 32
⊢ LE.le (α := ℝ) 1 2

Tactic:
norm_num1
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : √(HMul.hMul (α := ℝ) 2 512) = 32
⊢ (↑(9 + HMul.hMul (α := ℕ) 10 32) : ℝ) ≤ 2 * (512 / 3)

Tactic:
norm_num1
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
x : ℝ
x_large : 512 ≤ x
f : ℝ → ℝ := fun (x : ℝ) ↦ log x + √(2 * x) * log (2 * x) - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = log (x * (2 * x) ^ √(2 * x) / HPow.hPow (α := ℝ) 4 (x / 3))
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : √(HMul.hMul (α := ℝ) 2 512) = 32
⊢ LE.le (α := ℝ) 0 2

Tactic:
norm_num1
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
n : ℕ
n_large : 512 ≤ n
rw :
  LE.le (α := ℝ) (↑(n * (2 * n) ^ (2 * n).sqrt * HPow.hPow (α := ℕ) 4 (2 * n / 3)) : ℝ) (↑(HPow.hPow (α := ℕ) 4 n) : ℝ)
⊢ n * (2 * n) ^ (2 * n).sqrt * HPow.hPow (α := ℕ) 4 (2 * n / 3) ≤ HPow.hPow (α := ℕ) 4 n

Tactic:
rw [← @cast_le ℝ]

Premises used: Nat.cast_le
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
n : ℕ
n_large : 512 ≤ n
simp :
  (↑n : ℝ) * HPow.hPow (β := ℝ) (HMul.hMul (α := ℝ) 2 (↑n : ℝ)) (↑(2 * n).sqrt : ℝ) *
      HPow.hPow (α := ℝ) (β := ℝ) 4 (↑(2 * n / 3) : ℝ) ≤
    HPow.hPow (α := ℝ) (β := ℝ) 4 (↑n : ℝ)
⊢ LE.le (α := ℝ) (↑(n * (2 * n) ^ (2 * n).sqrt * HPow.hPow (α := ℕ) 4 (2 * n / 3)) : ℝ) (↑(HPow.hPow (α := ℕ) 4 n) : ℝ)

Tactic:
simp only [cast_mul, cast_pow, ← Real.rpow_natCast, cast_ofNat]

Premises used: Nat.cast_ofNat, Nat.cast_mul, Nat.cast_pow, Real.rpow_natCast
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
n : ℕ
n_large : 512 ≤ n
⊢ LE.le (α := ℝ) 512 (↑n : ℝ)

Tactic:
exact_mod_cast n_large
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
n : ℕ
n_large : 512 ≤ n
refine :
  (↑n : ℝ) * HPow.hPow (β := ℝ) (HMul.hMul (α := ℝ) 2 (↑n : ℝ)) (↑(2 * n).sqrt : ℝ) *
      HPow.hPow (α := ℝ) (β := ℝ) 4 (↑(2 * n / 3) : ℝ) ≤
    (↑n : ℝ) * HMul.hMul (α := ℝ) 2 (↑n : ℝ) ^ √(HMul.hMul (α := ℝ) 2 (↑n : ℝ)) *
      HPow.hPow (α := ℝ) 4 (HMul.hMul (α := ℝ) 2 (↑n : ℝ) / 3)
⊢ (↑n : ℝ) * HPow.hPow (β := ℝ) (HMul.hMul (α := ℝ) 2 (↑n : ℝ)) (↑(2 * n).sqrt : ℝ) *
      HPow.hPow (α := ℝ) (β := ℝ) 4 (↑(2 * n / 3) : ℝ) ≤
    HPow.hPow (α := ℝ) (β := ℝ) 4 (↑n : ℝ)

Tactic:
refine _root_.trans ?_ (Bertrand.real_main_inequality (by exact_mod_cast n_large))

Premises used: trans, Bertrand.real_main_inequality
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
n : ℕ
n_large : 512 ≤ n
h₁ : 1 ≤ HMul.hMul (α := ℝ) 2 (↑n : ℝ)
h₂ : (↑(2 * n).sqrt : ℝ) ≤ √(HMul.hMul (α := ℝ) 2 (↑n : ℝ))
h₃ : LE.le (α := ℝ) 1 4
h₄ : (↑(2 * n / 3) : ℝ) ≤ HMul.hMul (α := ℝ) 2 (↑n : ℝ) / 3
⊢ (↑n : ℝ) * HPow.hPow (β := ℝ) (HMul.hMul (α := ℝ) 2 (↑n : ℝ)) (↑(2 * n).sqrt : ℝ) *
      HPow.hPow (α := ℝ) (β := ℝ) 4 (↑(2 * n / 3) : ℝ) ≤
    (↑n : ℝ) * HMul.hMul (α := ℝ) 2 (↑n : ℝ) ^ √(HMul.hMul (α := ℝ) 2 (↑n : ℝ)) *
      HPow.hPow (α := ℝ) 4 (HMul.hMul (α := ℝ) 2 (↑n : ℝ) / 3)

Tactic:
gcongr
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
n : ℕ
n_large : 512 ≤ n
⊢ 0 < 2 * n

Tactic:
positivity
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
n : ℕ
n_large : 512 ≤ n
⊢ 0 < 2 * n

Tactic:
have n2_pos : 0 < 2 * n := by positivity
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
n : ℕ
n_large : 512 ≤ n
n2_pos : 0 < 2 * n
⊢ 1 ≤ HMul.hMul (α := ℝ) 2 (↑n : ℝ)

Tactic:
mod_cast n2_pos

Premises used: Nat.cast_mul._simp_1, HMul.hMul, congrArg, cast, Nat.cast_le._simp_1, LE.le, Nat.cast, congrFun', OfNat.ofNat, Eq.symm, Nat.cast_one, Eq.trans
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
n : ℕ
n_large : 512 ≤ n
n2_pos : 0 < 2 * n
⊢ 1 ≤ HMul.hMul (α := ℝ) 2 (↑n : ℝ)

Tactic:
exact mod_cast n2_pos
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
n : ℕ
n_large : 512 ≤ n
⊢ (↑(2 * n).sqrt : ℝ) ≤ √(HMul.hMul (α := ℝ) 2 (↑n : ℝ))

Tactic:
exact_mod_cast Real.nat_sqrt_le_real_sqrt

Premises used: Real.nat_sqrt_le_real_sqrt
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
n : ℕ
n_large : 512 ≤ n
⊢ LE.le (α := ℝ) 1 4

Tactic:
norm_num1
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
n : ℕ
n_large : 512 ≤ n
norm_cast norm_cast₁ norm_cast₂ norm_cast₃ : HDiv.hDiv (α := ℝ) (↑(2 * n) : ℝ) 3 ≤ HDiv.hDiv (α := ℝ) (↑(2 * n) : ℝ) 3
⊢ HDiv.hDiv (α := ℝ) (↑(2 * n) : ℝ) (↑3 : ℝ) ≤ HMul.hMul (α := ℝ) 2 (↑n : ℝ) / 3

Tactic:
norm_cast
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
n : ℕ
n_large : 512 ≤ n
⊢ (↑(2 * n / 3) : ℝ) ≤ HMul.hMul (α := ℝ) 2 (↑n : ℝ) / 3

Tactic:
exact cast_div_le.trans (by norm_cast)

Premises used: Nat.cast_div_le, LE.le.trans
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
n : ℕ
n_large : 2 < n
no_prime : ∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p
⊢ n.centralBinom =
    ∏ p ∈ Finset.range (2 * n / 3 + 1), HPow.hPow (β := ℕ) p ((n.centralBinom.factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
(Eq.trans ?_ n.prod_pow_factorization_centralBinom).symm

Premises used: Eq.symm, Nat.prod_pow_factorization_centralBinom, Eq.trans
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
n : ℕ
n_large : 2 < n
no_prime : ∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p
refine :
  Eq (α := ℕ)
    (∏ p ∈ Finset.range (2 * n / 3 + 1), HPow.hPow (β := ℕ) p ((n.centralBinom.factorization : (a : ℕ) → ℕ) p : ℕ))
    (∏ p ∈ Finset.range (2 * n + 1), HPow.hPow (β := ℕ) p ((n.centralBinom.factorization : (a : ℕ) → ℕ) p : ℕ))
⊢ n.centralBinom =
    ∏ p ∈ Finset.range (2 * n / 3 + 1), HPow.hPow (β := ℕ) p ((n.centralBinom.factorization : (a : ℕ) → ℕ) p : ℕ)

Tactic:
refine (Eq.trans ?_ n.prod_pow_factorization_centralBinom).symm

Premises used: Eq.symm, Nat.prod_pow_factorization_centralBinom, Eq.trans
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
n : ℕ
n_large : 2 < n
no_prime : ∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p
h : Finset.range (2 * n / 3 + 1) ⊆ Finset.range (2 * n + 1)
hf :
  ∀ x ∈ Finset.range (2 * n + 1),
    x ∉ Finset.range (2 * n / 3 + 1) → HPow.hPow (β := ℕ) x ((n.centralBinom.factorization : (a : ℕ) → ℕ) x : ℕ) = 1
⊢ Eq (α := ℕ)
    (∏ p ∈ Finset.range (2 * n / 3 + 1), HPow.hPow (β := ℕ) p ((n.centralBinom.factorization : (a : ℕ) → ℕ) p : ℕ))
    (∏ p ∈ Finset.range (2 * n + 1), HPow.hPow (β := ℕ) p ((n.centralBinom.factorization : (a : ℕ) → ℕ) p : ℕ))

Tactic:
apply Finset.prod_subset

Premises used: Finset.prod_subset
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
n : ℕ
n_large : 2 < n
no_prime : ∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p
h h₁ : Finset.range (2 * n + 1) ⊆ Finset.range (2 * n + 1)
⊢ Finset.range (2 * n / 3 + 1) ⊆ Finset.range (2 * n + 1)

Tactic:
grw [Nat.div_le_self]

Premises used: Nat.div_le_self
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
n : ℕ
n_large : 2 < n
no_prime : ∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p
x : ℕ
hx : x ∈ Finset.range (2 * n + 1)
h2x : x ∉ Finset.range (2 * n / 3 + 1)
⊢ x ≤ 2 * n

Tactic:
rw [Finset.mem_range, Nat.lt_succ_iff] at hx h2x

Premises used: Finset.mem_range, Nat.lt_succ_iff
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
n : ℕ
n_large : 2 < n
no_prime : ∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p
x : ℕ
hx : x ∈ Finset.range (2 * n + 1)
h2x : x ∉ Finset.range (2 * n / 3 + 1)
hx₁ : x ≤ 2 * n
⊢ ¬x ≤ 2 * n / 3

Tactic:
rw [Finset.mem_range, Nat.lt_succ_iff] at hx h2x

Premises used: Finset.mem_range, Nat.lt_succ_iff
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
n : ℕ
n_large : 2 < n
no_prime : ∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p
x : ℕ
hx : x ≤ 2 * n
h2x : ¬x ≤ 2 * n / 3
⊢ 2 * n < 3 * x

Tactic:
rw [not_le, div_lt_iff_lt_mul three_pos, mul_comm x] at h2x

Premises used: not_le, three_pos, Nat.div_lt_iff_lt_mul, mul_comm
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
n : ℕ
n_large : 2 < n
no_prime : ∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p
x : ℕ
hx : x ≤ 2 * n
h2x : 2 * n < 3 * x
⊢ ¬Nat.Prime x ∨ x ≤ n

Tactic:
simpa [imp_iff_not_or, hx.not_gt] using no_prime x

Premises used: imp_iff_not_or, LE.le.not_gt
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
n : ℕ
n_large : 2 < n
no_prime : ∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p
x : ℕ
hx : x ≤ 2 * n
h2x : 2 * n < 3 * x
hf : ∀ (h : ¬Nat.Prime x), HPow.hPow (β := ℕ) x ((n.centralBinom.factorization : (a : ℕ) → ℕ) x : ℕ) = 1
hf₁ : ∀ (h : x ≤ n), HPow.hPow (β := ℕ) x ((n.centralBinom.factorization : (a : ℕ) → ℕ) x : ℕ) = 1
⊢ HPow.hPow (β := ℕ) x ((n.centralBinom.factorization : (a : ℕ) → ℕ) x : ℕ) = 1

Tactic:
obtain h | h : ¬ x.Prime ∨ x ≤ n := by simpa [imp_iff_not_or, hx.not_gt] using no_prime x

Premises used: Nat.Prime
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
n : ℕ
n_large : 2 < n
no_prime : ∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p
x : ℕ
hx : x ≤ 2 * n
h2x : 2 * n < 3 * x
h : ¬Nat.Prime x
hf : HPow.hPow (β := ℕ) x 0 = 1
hf₁ hf₂ : Eq (α := ℕ) 1 1
⊢ HPow.hPow (β := ℕ) x ((n.centralBinom.factorization : (a : ℕ) → ℕ) x : ℕ) = 1

Tactic:
rw [factorization_eq_zero_of_not_prime n.centralBinom h, Nat.pow_zero]

Premises used: Nat.centralBinom, Nat.pow_zero, Nat.factorization_eq_zero_of_not_prime
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
n : ℕ
n_large : 2 < n
no_prime : ∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p
x : ℕ
hx : x ≤ 2 * n
h2x : 2 * n < 3 * x
h : x ≤ n
hf : HPow.hPow (β := ℕ) x 0 = 1
hf₁ hf₂ : Eq (α := ℕ) 1 1
⊢ HPow.hPow (β := ℕ) x ((n.centralBinom.factorization : (a : ℕ) → ℕ) x : ℕ) = 1

Tactic:
rw [factorization_centralBinom_of_two_mul_self_lt_three_mul n_large h h2x, Nat.pow_zero]

Premises used: Nat.pow_zero, Nat.factorization_centralBinom_of_two_mul_self_lt_three_mul
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
n : ℕ
n_large : 2 < n
no_prime : ∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p
⊢ 0 < n

Tactic:
have n_pos : 0 < n := (Nat.zero_le _).trans_lt n_large
-- Module: Mathlib.NumberTheory.Bertrand
Goal:
n : ℕ
n_large : 2 < n
no_prime : ∀ (p : ℕ), Nat.Prime p → n < p → 2 * n < p
n_pos : 0 < n
⊢ 1 ≤ 2 * n

Tactic:
have n2_pos : 1 ≤ 2 * n := mul_pos (zero_lt_two' ℕ) n_pos
-- Module: Mathlib.NumberTheory.Bertrand
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 : ℕ)
⊢ Eq (α := ℕ) (∏ x ∈ S, f x) (∏ x ∈ Finset.range (2 * n / 3 + 1), f x)

Tactic:
Finset.prod_filter_of_ne fun p _ h => ?_

Premises used: Finset.prod_filter_of_ne
-- Module: Mathlib.NumberTheory.Bertrand
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 : ℕ)
refine : ∀ p ∈ Finset.range (2 * n / 3 + 1), ∀ (h : f p ≠ 1), Nat.Prime p
⊢ Eq (α := ℕ) (∏ x ∈ S, f x) (∏ x ∈ Finset.range (2 * n / 3 + 1), f x)

Tactic:
refine Finset.prod_filter_of_ne fun p _ h => ?_

Premises used: Finset.prod_filter_of_ne
-- Module: Mathlib.NumberTheory.Bertrand
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 : ℕ)
p : ℕ
h_1 : p ∈ Finset.range (2 * n / 3 + 1)
h : f p ≠ 1
contrapose : ∀ (h : ¬Nat.Prime p), f p = 1
⊢ Nat.Prime p

Tactic:
contrapose h
-- Module: Mathlib.NumberTheory.Bertrand
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 : ℕ)
p : ℕ
h_1 : p ∈ Finset.range (2 * n / 3 + 1)
h : ¬Nat.Prime p
dsimp : HPow.hPow (β := ℕ) p ((n.centralBinom.factorization : (a : ℕ) → ℕ) p : ℕ) = 1
⊢ f p = 1

Tactic:
dsimp only [f]
-- Module: Mathlib.NumberTheory.Bertrand
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 : ℕ)
p : ℕ
h_1 : p ∈ Finset.range (2 * n / 3 + 1)
h : ¬Nat.Prime p
rw : HPow.hPow (β := ℕ) p 0 = 1
rw₁ rw₂ : Eq (α := ℕ) 1 1
⊢ HPow.hPow (β := ℕ) p ((n.centralBinom.factorization : (a : ℕ) → ℕ) p : ℕ) = 1

Tactic:
rw [factorization_eq_zero_of_not_prime n.centralBinom h, _root_.pow_zero]

Premises used: Nat.centralBinom, pow_zero, Nat.factorization_eq_zero_of_not_prime
-- Module: Mathlib.NumberTheory.Bertrand
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 : ℕ)
⊢ Eq (α := ℕ) (∏ x ∈ S, f x) (∏ x ∈ Finset.range (2 * n / 3 + 1), f x)

Tactic:
have : ∏ x ∈ S, f x = ∏ x ∈ Finset.range (2 * n / 3 + 1), f x := by
    refine Finset.prod_filter_of_ne fun p _ h => ?_
    contrapose h; dsimp only [f]
    rw [factorization_eq_zero_of_not_prime n.centralBinom h, _root_.pow_zero]
-- Module: Mathlib.NumberTheory.Bertrand
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 :
  HMul.hMul (α := ℕ) (∏ x ∈ S with x ≤ (2 * n).sqrt, f x) (∏ x ∈ S with ¬x ≤ (2 * n).sqrt, f x) ≤
    (2 * n) ^ (2 * n).sqrt * HPow.hPow (α := ℕ) 4 (2 * n / 3)
⊢ n.centralBinom ≤ (2 * n) ^ (2 * n).sqrt * HPow.hPow (α := ℕ) 4 (2 * n / 3)

Tactic:
rw [centralBinom_factorization_small n n_large no_prime, ← this, ←
    Finset.prod_filter_mul_prod_filter_not S (· ≤ sqrt (2 * n))]

Premises used: HMul.hMul, Nat.sqrt, LE.le, centralBinom_factorization_small, Finset.prod_filter_mul_prod_filter_not, OfNat.ofNat
-- Module: Mathlib.NumberTheory.Bertrand
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₁ : ∏ x ∈ S with x ≤ (2 * n).sqrt, f x ≤ (2 * n) ^ (2 * n).sqrt
h₂ : ∏ x ∈ S with ¬x ≤ (2 * n).sqrt, f x ≤ HPow.hPow (α := ℕ) 4 (2 * n / 3)
⊢ HMul.hMul (α := ℕ) (∏ x ∈ S with x ≤ (2 * n).sqrt, f x) (∏ x ∈ S with ¬x ≤ (2 * n).sqrt, f x) ≤
    (2 * n) ^ (2 * n).sqrt * HPow.hPow (α := ℕ) 4 (2 * n / 3)

Tactic:
apply mul_le_mul'

Premises used: mul_le_mul'
-- Module: Mathlib.NumberTheory.Bertrand
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

Tactic:
(Finset.prod_le_prod' fun p _ => (?_ : f p ≤ 2 * n)).trans ?_

Premises used: Finset.prod_le_prod', LE.le.trans
-- Module: Mathlib.NumberTheory.Bertrand
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
h₂ : ∏ i ∈ S with i ≤ (2 * n).sqrt, 2 * n ≤ (2 * n) ^ (2 * n).sqrt
⊢ ∏ x ∈ S with x ≤ (2 * n).sqrt, f x ≤ (2 * n) ^ (2 * n).sqrt

Tactic:
refine (Finset.prod_le_prod' fun p _ => (?_ : f p ≤ 2 * n)).trans ?_

Premises used: Finset.prod_le_prod', LE.le.trans
-- Module: Mathlib.NumberTheory.Bertrand
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 : ℕ
h : p ∈ {x ∈ S | x ≤ (2 * n).sqrt}
⊢ f p ≤ 2 * n

Tactic:
pow_factorization_choose_le (mul_pos two_pos n_pos)

Premises used: two_pos, Nat.centralBinom, mul_pos, Nat.pow_factorization_choose_le
-- Module: Mathlib.NumberTheory.Bertrand
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 : ℕ
h : p ∈ {x ∈ S | x ≤ (2 * n).sqrt}
⊢ f p ≤ 2 * n

Tactic:
exact pow_factorization_choose_le (mul_pos two_pos n_pos)

Premises used: two_pos, mul_pos, Nat.pow_factorization_choose_le
-- Module: Mathlib.NumberTheory.Bertrand
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
rw₁ rw₂ : (2 * n).sqrt = (2 * n).sqrt
⊢ (Finset.Icc 1 (2 * n).sqrt).card = (2 * n).sqrt

Tactic:
rw [card_Icc, Nat.add_sub_cancel]

Premises used: Nat.card_Icc, Nat.add_sub_cancel
-- Module: Mathlib.NumberTheory.Bertrand
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

Tactic:
have : (Finset.Icc 1 (sqrt (2 * n))).card = sqrt (2 * n) := by rw [card_Icc, Nat.add_sub_cancel]
-- Module: Mathlib.NumberTheory.Bertrand
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
h₁ : (2 * n) ^ {x ∈ S | x ≤ (2 * n).sqrt}.card ≤ (2 * n) ^ (2 * n).sqrt
⊢ ∏ i ∈ S with i ≤ (2 * n).sqrt, 2 * n ≤ (2 * n) ^ (2 * n).sqrt

Tactic:
rw [Finset.prod_const]

Premises used: Finset.prod_const
-- Module: Mathlib.NumberTheory.Bertrand
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

Tactic:
pow_right_mono₀ n2_pos ((Finset.card_le_card fun x hx => ?_).trans this.le)

Premises used: Finset.card_le_card, Eq.le, pow_right_mono₀, LE.le.trans
-- Module: Mathlib.NumberTheory.Bertrand
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
h₁ : ∀ (x : ℕ) (hx : x ∈ {x ∈ S | x ≤ (2 * n).sqrt}), x ∈ Finset.Icc 1 (2 * n).sqrt
⊢ (2 * n) ^ {x ∈ S | x ≤ (2 * n).sqrt}.card ≤ (2 * n) ^ (2 * n).sqrt

Tactic:
refine pow_right_mono₀ n2_pos ((Finset.card_le_card fun x hx => ?_).trans this.le)

Premises used: Finset.card_le_card, Eq.le, pow_right_mono₀, LE.le.trans
-- Module: Mathlib.NumberTheory.Bertrand
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 ∈ S

Tactic:
obtain ⟨h1, h2⟩ := Finset.mem_filter.1 hx

Premises used: Iff.mp, Finset.mem_filter
-- Module: Mathlib.NumberTheory.Bertrand
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 ≤ (2 * n).sqrt

Tactic:
obtain ⟨h1, h2⟩ := Finset.mem_filter.1 hx

Premises used: Iff.mp, Finset.mem_filter
-- Module: Mathlib.NumberTheory.Bertrand
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
h2 : x ≤ (2 * n).sqrt
⊢ x ∈ Finset.Icc 1 (2 * n).sqrt

Tactic:
Finset.mem_Icc.mpr ⟨(Finset.mem_filter.1 h1).2.one_lt.le, h2⟩

Premises used: Iff.mpr, Nat.Prime.one_lt, Finset.mem_Icc, LT.lt.le, And.right, And.intro, Iff.mp, Finset.mem_filter