awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (goal)
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
⊢ f 512 ≤ 0
have refine_2 : 512 * HPow.hPow (β := ℝ) (HMul.hMul (α := ℝ) 2 512) 32 ≤ HPow.hPow (α := ℝ) 4 (512 / 3)
Tactic: rw [hf _ (by norm_num1), log_nonpos_iff (hf' _ (by norm_num1)).le, this,
        div_le_one (by positivity)]
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (goal)
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
⊢ 512 * HPow.hPow (β := ℝ) (HMul.hMul (α := ℝ) 2 512) 32 ≤ HPow.hPow (α := ℝ) 4 (512 / 3)
have refine_2 : HPow.hPow (α := ℝ) (β := ℕ) 2 9 * HPow.hPow (β := ℝ) (HMul.hMul (α := ℝ) 2 512) 32 ≤ HPow.hPow (α := ℝ) 4 (512 / 3)
Tactic: conv in 512 => equals 2 ^ 9 => norm_num1
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (goal)
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
⊢ HPow.hPow (α := ℝ) (β := ℕ) 2 9 * HPow.hPow (β := ℝ) (HMul.hMul (α := ℝ) 2 512) 32 ≤ HPow.hPow (α := ℝ) 4 (512 / 3)
have refine_2 : HPow.hPow (α := ℝ) (β := ℕ) 2 9 * HPow.hPow (β := ℝ) (HPow.hPow (α := ℝ) (β := ℕ) 2 10) 32 ≤
  HPow.hPow (α := ℝ) 4 (512 / 3)
Tactic: conv in 2 * 512 => equals 2 ^ 10 => norm_num1
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (goal)
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
⊢ HPow.hPow (α := ℝ) (β := ℕ) 2 9 * HPow.hPow (β := ℝ) (HPow.hPow (α := ℝ) (β := ℕ) 2 10) (↑32 : ℝ) ≤
    HPow.hPow (α := ℝ) 4 (512 / 3)
have refine_2 : HPow.hPow (α := ℝ) 2 (9 + HMul.hMul (α := ℕ) 10 32) ≤ HPow.hPow (α := ℝ) 4 (512 / 3)
Tactic: rw [rpow_natCast, ← pow_mul, ← pow_add]
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (goal)
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
⊢ 4 = HPow.hPow (α := ℝ) (β := ℝ) 2 2
have rw : 4 = HPow.hPow (α := ℝ) (β := ℕ) 2 2
Tactic: rw [rpow_two]
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (goal)
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
⊢ HPow.hPow (α := ℝ) 2 (9 + HMul.hMul (α := ℕ) 10 32) ≤ HPow.hPow (α := ℝ) 4 (512 / 3)
have refine_2 : HPow.hPow (α := ℝ) 2 (9 + HMul.hMul (α := ℕ) 10 32) ≤ HPow.hPow (α := ℝ) (β := ℝ) 2 2 ^ (512 / 3)
Tactic: conv in 4 => equals 2 ^ (2 : ℝ) => rw [rpow_two]; norm_num1
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (goal)
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
⊢ HPow.hPow (α := ℝ) 2 (9 + HMul.hMul (α := ℕ) 10 32) ≤ HPow.hPow (α := ℝ) (β := ℝ) 2 2 ^ (512 / 3)
have refine_2 : HPow.hPow (α := ℝ) (β := ℝ) 2 (↑(9 + HMul.hMul (α := ℕ) 10 32) : ℝ) ≤ HPow.hPow (α := ℝ) 2 (2 * (512 / 3))
Tactic: rw [← rpow_mul, ← rpow_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (goal)
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 : HPow.hPow (α := ℝ) (β := ℝ) 2 (↑(9 + HMul.hMul (α := ℕ) 10 32) : ℝ) ≤ HPow.hPow (α := ℝ) 2 (2 * (512 / 3))
⊢ HPow.hPow (α := ℝ) 2 (9 + HMul.hMul (α := ℕ) 10 32) ≤ HPow.hPow (α := ℝ) (β := ℝ) 2 2 ^ (512 / 3)
have refine_2₁ : LE.le (α := ℝ) 0 2
Tactic: rw [← rpow_mul, ← rpow_natCast]
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (goal)
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
⊢ HPow.hPow (α := ℝ) (β := ℝ) 2 (↑(9 + HMul.hMul (α := ℕ) 10 32) : ℝ) ≤ HPow.hPow (α := ℝ) 2 (2 * (512 / 3))
have refine_2 : LE.le (α := ℝ) 1 2
Tactic: apply rpow_le_rpow_of_exponent_le
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (goal)
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
⊢ HPow.hPow (α := ℝ) (β := ℝ) 2 (↑(9 + HMul.hMul (α := ℕ) 10 32) : ℝ) ≤ HPow.hPow (α := ℝ) 2 (2 * (512 / 3))
have refine_2₁ : (↑(9 + HMul.hMul (α := ℕ) 10 32) : ℝ) ≤ 2 * (512 / 3)
Tactic: apply rpow_le_rpow_of_exponent_le
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (goal)
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
⊢ HPow.hPow (α := ℝ) (β := ℝ) 2 (↑(9 + HMul.hMul (α := ℕ) 10 32) : ℝ) ≤ HPow.hPow (α := ℝ) 2 (2 * (512 / 3))
have refine_2 : LE.le (α := ℝ) 1 2
Tactic: on_goal 1 => apply rpow_le_rpow_of_exponent_le
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (goal)
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
⊢ HPow.hPow (α := ℝ) (β := ℝ) 2 (↑(9 + HMul.hMul (α := ℕ) 10 32) : ℝ) ≤ HPow.hPow (α := ℝ) 2 (2 * (512 / 3))
have refine_2₁ : (↑(9 + HMul.hMul (α := ℕ) 10 32) : ℝ) ≤ 2 * (512 / 3)
Tactic: on_goal 1 => apply rpow_le_rpow_of_exponent_le
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (goal)
Goal:
n : ℕ
n_large : 512 ≤ n
⊢ n * (2 * n) ^ (2 * n).sqrt * HPow.hPow (α := ℕ) 4 (2 * n / 3) ≤ HPow.hPow (α := ℕ) 4 n
have rw : LE.le (α := ℝ) (↑(n * (2 * n) ^ (2 * n).sqrt * HPow.hPow (α := ℕ) 4 (2 * n / 3)) : ℝ) (↑(HPow.hPow (α := ℕ) 4 n) : ℝ)
Tactic: rw [← @cast_le ℝ]
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (goal)
Goal:
n : ℕ
n_large : 512 ≤ n
⊢ LE.le (α := ℝ) (↑(n * (2 * n) ^ (2 * n).sqrt * HPow.hPow (α := ℕ) 4 (2 * n / 3)) : ℝ) (↑(HPow.hPow (α := ℕ) 4 n) : ℝ)
have simp : (↑n : ℝ) * HPow.hPow (β := ℝ) (HMul.hMul (α := ℝ) 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]
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (goal)
Goal:
n : ℕ
n_large : 512 ≤ n
⊢ (↑n : ℝ) * HPow.hPow (β := ℝ) (HMul.hMul (α := ℝ) 2 (↑n : ℝ)) (↑(2 * n).sqrt : ℝ) *
      HPow.hPow (α := ℝ) (β := ℝ) 4 (↑(2 * n / 3) : ℝ) ≤
    HPow.hPow (α := ℝ) (β := ℝ) 4 (↑n : ℝ)
have 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)
Tactic: refine _root_.trans ?_ (Bertrand.real_main_inequality (by exact_mod_cast n_large))
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (goal)
Goal:
n : ℕ
n_large : 512 ≤ n
⊢ (↑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)
have h₁ : 1 ≤ HMul.hMul (α := ℝ) 2 (↑n : ℝ)
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (goal)
Goal:
n : ℕ
n_large : 512 ≤ n
h₁ : 1 ≤ HMul.hMul (α := ℝ) 2 (↑n : ℝ)
⊢ (↑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)
have h₂ : (↑(2 * n).sqrt : ℝ) ≤ √(HMul.hMul (α := ℝ) 2 (↑n : ℝ))
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (goal)
Goal:
n : ℕ
n_large : 512 ≤ n
h₁ : 1 ≤ HMul.hMul (α := ℝ) 2 (↑n : ℝ)
h₂ : (↑(2 * n).sqrt : ℝ) ≤ √(HMul.hMul (α := ℝ) 2 (↑n : ℝ))
⊢ (↑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)
have h₃ : LE.le (α := ℝ) 1 4
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (goal)
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
⊢ (↑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)
have h₄ : (↑(2 * n / 3) : ℝ) ≤ HMul.hMul (α := ℝ) 2 (↑n : ℝ) / 3
Tactic: gcongr
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (hypothesis)
Goal:
n : ℕ
n_large : 512 ≤ n
⊢ 1 ≤ HMul.hMul (α := ℝ) 2 (↑n : ℝ)
have n2_pos : 0 < 2 * n
Tactic: have n2_pos : 0 < 2 * n := by positivity
-- Lean 4 proof step from Mathlib.NumberTheory.Bertrand (goal)
Goal:
n : ℕ
n_large : 512 ≤ n
⊢ HDiv.hDiv (α := ℝ) (↑(2 * n) : ℝ) (↑3 : ℝ) ≤ HMul.hMul (α := ℝ) 2 (↑n : ℝ) / 3
have norm_cast : HDiv.hDiv (α := ℝ) (↑(2 * n) : ℝ) 3 ≤ HDiv.hDiv (α := ℝ) (↑(2 * n) : ℝ) 3
Tactic: norm_cast
-- 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.centralBinom =
    ∏ p ∈ Finset.range (2 * n / 3 + 1), HPow.hPow (β := ℕ) p ((n.centralBinom.factorization : (a : ℕ) → ℕ) p : ℕ)
have 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 : ℕ))
Tactic: refine (Eq.trans ?_ n.prod_pow_factorization_centralBinom).symm
-- 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
⊢ 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 : ℕ))
have h : Finset.range (2 * n / 3 + 1) ⊆ Finset.range (2 * n + 1)
Tactic: apply Finset.prod_subset
-- 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
h : Finset.range (2 * n / 3 + 1) ⊆ Finset.range (2 * n + 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 : ℕ))
have hf : ∀ x ∈ Finset.range (2 * n + 1),
  x ∉ Finset.range (2 * n / 3 + 1) → HPow.hPow (β := ℕ) x ((n.centralBinom.factorization : (a : ℕ) → ℕ) x : ℕ) = 1
Tactic: apply Finset.prod_subset
-- 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
⊢ Finset.range (2 * n / 3 + 1) ⊆ Finset.range (2 * n + 1)
have h : Finset.range (2 * n + 1) ⊆ Finset.range (2 * n + 1)
Tactic: grw [Nat.div_le_self]
-- 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
x : ℕ
hx : x ∈ Finset.range (2 * n + 1)
h2x : x ∉ Finset.range (2 * n / 3 + 1)
⊢ HPow.hPow (β := ℕ) x ((n.centralBinom.factorization : (a : ℕ) → ℕ) x : ℕ) = 1
have hx₁ : x ≤ 2 * n
Tactic: rw [Finset.mem_range, Nat.lt_succ_iff] at hx h2x
Cleared hypotheses: hx, h2x
-- 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
x : ℕ
hx : x ∈ Finset.range (2 * n + 1)
h2x : x ∉ Finset.range (2 * n / 3 + 1)
hx₁ : x ≤ 2 * n
⊢ HPow.hPow (β := ℕ) x ((n.centralBinom.factorization : (a : ℕ) → ℕ) x : ℕ) = 1
have h2x₁ : ¬x ≤ 2 * n / 3
Tactic: rw [Finset.mem_range, Nat.lt_succ_iff] at hx h2x
Cleared hypotheses: hx, h2x
-- 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
x : ℕ
hx : x ≤ 2 * n
h2x : ¬x ≤ 2 * n / 3
⊢ HPow.hPow (β := ℕ) x ((n.centralBinom.factorization : (a : ℕ) → ℕ) x : ℕ) = 1
have h2x₁ : 2 * n < 3 * x
Tactic: rw [not_le, div_lt_iff_lt_mul three_pos, mul_comm x] at h2x
Cleared hypotheses: h2x
-- 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
x : ℕ
hx : x ≤ 2 * n
h2x : 2 * n < 3 * x
⊢ HPow.hPow (β := ℕ) x ((n.centralBinom.factorization : (a : ℕ) → ℕ) x : ℕ) = 1
have hf : ∀ (h : ¬Nat.Prime x), 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
-- 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
x : ℕ
hx : x ≤ 2 * n
h2x : 2 * n < 3 * x
hf : ∀ (h : ¬Nat.Prime x), HPow.hPow (β := ℕ) x ((n.centralBinom.factorization : (a : ℕ) → ℕ) x : ℕ) = 1
⊢ HPow.hPow (β := ℕ) x ((n.centralBinom.factorization : (a : ℕ) → ℕ) x : ℕ) = 1
have hf₁ : ∀ (h : x ≤ n), 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
-- 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
x : ℕ
hx : x ≤ 2 * n
h2x : 2 * n < 3 * x
h : ¬Nat.Prime x
⊢ HPow.hPow (β := ℕ) x ((n.centralBinom.factorization : (a : ℕ) → ℕ) x : ℕ) = 1
have hf : HPow.hPow (β := ℕ) x 0 = 1
Tactic: rw [factorization_eq_zero_of_not_prime n.centralBinom h, Nat.pow_zero]
-- 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
x : ℕ
hx : x ≤ 2 * n
h2x : 2 * n < 3 * x
h : ¬Nat.Prime x
hf : HPow.hPow (β := ℕ) x 0 = 1
⊢ HPow.hPow (β := ℕ) x ((n.centralBinom.factorization : (a : ℕ) → ℕ) x : ℕ) = 1
have hf₁ : Eq (α := ℕ) 1 1
Tactic: rw [factorization_eq_zero_of_not_prime n.centralBinom h, Nat.pow_zero]
-- 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
x : ℕ
hx : x ≤ 2 * n
h2x : 2 * n < 3 * x
h : x ≤ n
⊢ HPow.hPow (β := ℕ) x ((n.centralBinom.factorization : (a : ℕ) → ℕ) x : ℕ) = 1
have hf : HPow.hPow (β := ℕ) x 0 = 1
Tactic: rw [factorization_centralBinom_of_two_mul_self_lt_three_mul n_large h h2x, Nat.pow_zero]
-- 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
x : ℕ
hx : x ≤ 2 * n
h2x : 2 * n < 3 * x
h : x ≤ n
hf : HPow.hPow (β := ℕ) x 0 = 1
⊢ HPow.hPow (β := ℕ) x ((n.centralBinom.factorization : (a : ℕ) → ℕ) x : ℕ) = 1
have hf₁ : Eq (α := ℕ) 1 1
Tactic: rw [factorization_centralBinom_of_two_mul_self_lt_three_mul n_large h h2x, Nat.pow_zero]
-- 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.centralBinom ≤ (2 * n) ^ (2 * n).sqrt * HPow.hPow (α := ℕ) 4 (2 * n / 3)
have n_pos : 0 < n
Tactic: have n_pos : 0 < n := (Nat.zero_le _).trans_lt n_large
-- 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
⊢ n.centralBinom ≤ (2 * n) ^ (2 * n).sqrt * HPow.hPow (α := ℕ) 4 (2 * n / 3)
have n2_pos : 1 ≤ 2 * n
Tactic: have n2_pos : 1 ≤ 2 * n := mul_pos (zero_lt_two' ℕ) n_pos
-- 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 : ℕ)
⊢ Eq (α := ℕ) (∏ x ∈ S, f x) (∏ x ∈ Finset.range (2 * n / 3 + 1), f x)
have refine : ∀ p ∈ Finset.range (2 * n / 3 + 1), ∀ (h : f p ≠ 1), Nat.Prime p
Tactic: refine Finset.prod_filter_of_ne fun p _ h => ?_
-- 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 : ℕ)
p : ℕ
h_1 : p ∈ Finset.range (2 * n / 3 + 1)
h : f p ≠ 1
⊢ Nat.Prime p
have contrapose : ∀ (h : ¬Nat.Prime p), f p = 1
Tactic: contrapose h
Cleared hypotheses: h
-- 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 : ℕ)
p : ℕ
h_1 : p ∈ Finset.range (2 * n / 3 + 1)
h : ¬Nat.Prime p
⊢ HPow.hPow (β := ℕ) p ((n.centralBinom.factorization : (a : ℕ) → ℕ) p : ℕ) = 1
have rw : HPow.hPow (β := ℕ) p 0 = 1
Tactic: rw [factorization_eq_zero_of_not_prime n.centralBinom h, _root_.pow_zero]
-- 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 : ℕ)
p : ℕ
h_1 : p ∈ Finset.range (2 * n / 3 + 1)
h : ¬Nat.Prime p
rw : HPow.hPow (β := ℕ) p 0 = 1
⊢ HPow.hPow (β := ℕ) p ((n.centralBinom.factorization : (a : ℕ) → ℕ) p : ℕ) = 1
have rw₁ : Eq (α := ℕ) 1 1
Tactic: rw [factorization_eq_zero_of_not_prime n.centralBinom h, _root_.pow_zero]
-- 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 : ℕ)
⊢ n.centralBinom ≤ (2 * n) ^ (2 * n).sqrt * HPow.hPow (α := ℕ) 4 (2 * n / 3)
have this : 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]
-- 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)
⊢ n.centralBinom ≤ (2 * n) ^ (2 * n).sqrt * HPow.hPow (α := ℕ) 4 (2 * n / 3)
have 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)
Tactic: rw [centralBinom_factorization_small n n_large no_prime, ← this, ←
    Finset.prod_filter_mul_prod_filter_not S (· ≤ sqrt (2 * n))]
-- 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)
⊢ 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)
have h₁ : ∏ x ∈ S with x ≤ (2 * n).sqrt, f x ≤ (2 * n) ^ (2 * n).sqrt
Tactic: apply mul_le_mul'
-- 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₁ : ∏ x ∈ S with x ≤ (2 * n).sqrt, f x ≤ (2 * n) ^ (2 * n).sqrt
⊢ 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)
have h₂ : ∏ x ∈ S with ¬x ≤ (2 * n).sqrt, f x ≤ HPow.hPow (α := ℕ) 4 (2 * n / 3)
Tactic: apply mul_le_mul'