-- Mathlib/NumberTheory/Bertrand.lean
theorem centralBinom_le_of_no_bertrand_prime (n : ℕ) (n_large : 2 < n)
    (no_prime : ¬∃ p : ℕ, Nat.Prime p ∧ n < p ∧ p ≤ 2 * n) :
    centralBinom n ≤ (2 * n) ^ sqrt (2 * n) * 4 ^ (2 * n / 3)

Proof state:
case h₁.refine_1
n : ℕ
n_large : 2 < n
no_prime : ¬∃ p, Nat.Prime p ∧ n < p ∧ p ≤ 2 * n
n_pos : 0 < n
n2_pos : 1 ≤ 2 * n
S : Finset ℕ := Finset.filter Nat.Prime (Finset.range (2 * n / 3 + 1))
f : ℕ → ℕ := fun x => x ^ n.centralBinom.factorization x
this : ∏ x ∈ S, f x = ∏ x ∈ Finset.range (2 * n / 3 + 1), f x
p : ℕ
x✝ : p ∈ Finset.filter (fun x => x ≤ (2 * n).sqrt) S
⊢ f p ≤ 2 * n

Tactic:
exact pow_factorization_choose_le (mul_pos two_pos n_pos)

Result:
no goals

Proof state:
n : ℕ
n_large : 2 < n
no_prime : ¬∃ p, Nat.Prime p ∧ n < p ∧ p ≤ 2 * n
n_pos : 0 < n
n2_pos : 1 ≤ 2 * n
S : Finset ℕ := Finset.filter Nat.Prime (Finset.range (2 * n / 3 + 1))
f : ℕ → ℕ := fun x => x ^ n.centralBinom.factorization x
p : ℕ
x✝ : p ∈ Finset.range (2 * n / 3 + 1)
h : ¬Nat.Prime p
⊢ f p = 1

Tactic:
dsimp only [f]

Result:
n : ℕ
n_large : 2 < n
no_prime : ¬∃ p, Nat.Prime p ∧ n < p ∧ p ≤ 2 * n
n_pos : 0 < n
n2_pos : 1 ≤ 2 * n
S : Finset ℕ := Finset.filter Nat.Prime (Finset.range (2 * n / 3 + 1))
f : ℕ → ℕ := fun x => x ^ n.centralBinom.factorization x
p : ℕ
x✝ : p ∈ Finset.range (2 * n / 3 + 1)
h : ¬Nat.Prime p
⊢ p ^ n.centralBinom.factorization p = 1

Proof state:
n : ℕ
n_large : 2 < n
no_prime : ¬∃ p, Nat.Prime p ∧ n < p ∧ p ≤ 2 * n
⊢ n.centralBinom ≤ (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3)

Tactic:
have n_pos : 0 < n := (Nat.zero_le _).trans_lt n_large

Result:
n : ℕ
n_large : 2 < n
no_prime : ¬∃ p, Nat.Prime p ∧ n < p ∧ p ≤ 2 * n
n_pos : 0 < n
⊢ n.centralBinom ≤ (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3)

Proof state:
n : ℕ
n_large : 2 < n
no_prime : ¬∃ p, Nat.Prime p ∧ n < p ∧ p ≤ 2 * n
n_pos : 0 < n
n2_pos : 1 ≤ 2 * n
⊢ n.centralBinom ≤ (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3)

Tactic:
let S := (Finset.range (2 * n / 3 + 1)).filter Nat.Prime

Result:
n : ℕ
n_large : 2 < n
no_prime : ¬∃ p, Nat.Prime p ∧ n < p ∧ p ≤ 2 * n
n_pos : 0 < n
n2_pos : 1 ≤ 2 * n
S : Finset ℕ := Finset.filter Nat.Prime (Finset.range (2 * n / 3 + 1))
⊢ n.centralBinom ≤ (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3)

Proof state:
case h₂.refine_1
n : ℕ
n_large : 2 < n
no_prime : ¬∃ p, Nat.Prime p ∧ n < p ∧ p ≤ 2 * n
n_pos : 0 < n
n2_pos : 1 ≤ 2 * n
S : Finset ℕ := Finset.filter Nat.Prime (Finset.range (2 * n / 3 + 1))
f : ℕ → ℕ := fun x => x ^ n.centralBinom.factorization x
this : ∏ x ∈ S, f x = ∏ x ∈ Finset.range (2 * n / 3 + 1), f x
p : ℕ
hp : p ∈ Finset.filter (fun x => ¬x ≤ (2 * n).sqrt) S
⊢ f p ≤ p

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

Result:
case h₂.refine_1.intro
n : ℕ
n_large : 2 < n
no_prime : ¬∃ p, Nat.Prime p ∧ n < p ∧ p ≤ 2 * n
n_pos : 0 < n
n2_pos : 1 ≤ 2 * n
S : Finset ℕ := Finset.filter Nat.Prime (Finset.range (2 * n / 3 + 1))
f : ℕ → ℕ := fun x => x ^ n.centralBinom.factorization x
this : ∏ x ∈ S, f x = ∏ x ∈ Finset.range (2 * n / 3 + 1), f x
p : ℕ
hp : p ∈ Finset.filter (fun x => ¬x ≤ (2 * n).sqrt) S
h1 : p ∈ S
h2 : ¬p ≤ (2 * n).sqrt
⊢ f p ≤ p

Proof state:
case h₂
n : ℕ
n_large : 2 < n
no_prime : ¬∃ p, Nat.Prime p ∧ n < p ∧ p ≤ 2 * n
n_pos : 0 < n
n2_pos : 1 ≤ 2 * n
S : Finset ℕ := Finset.filter Nat.Prime (Finset.range (2 * n / 3 + 1))
f : ℕ → ℕ := fun x => x ^ n.centralBinom.factorization x
this : ∏ x ∈ S, f x = ∏ x ∈ Finset.range (2 * n / 3 + 1), f x
⊢ ∏ x ∈ Finset.filter (fun x => ¬x ≤ (2 * n).sqrt) S, f x ≤ 4 ^ (2 * n / 3)

Tactic:
refine le_trans ?_ (primorial_le_4_pow (2 * n / 3))

Result:
case h₂
n : ℕ
n_large : 2 < n
no_prime : ¬∃ p, Nat.Prime p ∧ n < p ∧ p ≤ 2 * n
n_pos : 0 < n
n2_pos : 1 ≤ 2 * n
S : Finset ℕ := Finset.filter Nat.Prime (Finset.range (2 * n / 3 + 1))
f : ℕ → ℕ := fun x => x ^ n.centralBinom.factorization x
this : ∏ x ∈ S, f x = ∏ x ∈ Finset.range (2 * n / 3 + 1), f x
⊢ ∏ x ∈ Finset.filter (fun x => ¬x ≤ (2 * n).sqrt) S, f x ≤ primorial (2 * n / 3)

Proof state:
case h₁.refine_2.intro
n : ℕ
n_large : 2 < n
no_prime : ¬∃ p, Nat.Prime p ∧ n < p ∧ p ≤ 2 * n
n_pos : 0 < n
n2_pos : 1 ≤ 2 * n
S : Finset ℕ := Finset.filter Nat.Prime (Finset.range (2 * n / 3 + 1))
f : ℕ → ℕ := fun x => x ^ n.centralBinom.factorization x
this✝ : ∏ 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 ∈ Finset.filter (fun x => x ≤ (2 * n).sqrt) S
h1 : x ∈ S
h2 : x ≤ (2 * n).sqrt
⊢ x ∈ Finset.Icc 1 (2 * n).sqrt

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

Result:
no goals