-- Mathlib/NumberTheory/Bertrand.lean
theorem centralBinom_factorization_small (n : ℕ) (n_large : 2 < n)
    (no_prime : ¬∃ p : ℕ, p.Prime ∧ n < p ∧ p ≤ 2 * n) :
    centralBinom n = ∏ p ∈ Finset.range (2 * n / 3 + 1), p ^ (centralBinom n).factorization p

Proof state:
case hf
n : ℕ
n_large : 2 < n
no_prime : ¬∃ p, Nat.Prime p ∧ n < p ∧ p ≤ 2 * n
x : ℕ
hx : x ≤ 2 * n
h2x : ¬x ≤ 2 * n / 3
⊢ x ^ n.centralBinom.factorization x = 1

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

Result:
case hf
n : ℕ
n_large : 2 < n
no_prime : ¬∃ p, Nat.Prime p ∧ n < p ∧ p ≤ 2 * n
x : ℕ
hx : x ≤ 2 * n
h2x : 2 * n < 3 * x
⊢ x ^ n.centralBinom.factorization x = 1

Proof state:
case hf
n : ℕ
n_large : 2 < n
no_prime : ¬∃ p, Nat.Prime p ∧ n < p ∧ p ≤ 2 * n
⊢ ∀ x ∈ Finset.range (2 * n + 1), x ∉ Finset.range (2 * n / 3 + 1) → x ^ n.centralBinom.factorization x = 1

Tactic:
intro x hx h2x

Result:
case hf
n : ℕ
n_large : 2 < n
no_prime : ¬∃ p, Nat.Prime p ∧ n < p ∧ p ≤ 2 * n
x : ℕ
hx : x ∈ Finset.range (2 * n + 1)
h2x : x ∉ Finset.range (2 * n / 3 + 1)
⊢ x ^ n.centralBinom.factorization x = 1

Proof state:
case hf.inr
n : ℕ
n_large : 2 < n
x : ℕ
hx : x ≤ 2 * n
h2x : 2 * n < 3 * x
no_prime : x ≤ 2 * n → ¬Nat.Prime x ∨ x ≤ n
h : x ≤ n
⊢ x ^ n.centralBinom.factorization x = 1

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

Result:
no goals

Proof state:
case hf
n : ℕ
n_large : 2 < n
no_prime : ¬∃ p, Nat.Prime p ∧ n < p ∧ p ≤ 2 * n
x : ℕ
hx : x ≤ 2 * n
h2x : 2 * n < 3 * x
⊢ x ^ n.centralBinom.factorization x = 1

Tactic:
replace no_prime := not_exists.mp no_prime x

Result:
case hf
n : ℕ
n_large : 2 < n
x : ℕ
hx : x ≤ 2 * n
h2x : 2 * n < 3 * x
no_prime : ¬(Nat.Prime x ∧ n < x ∧ x ≤ 2 * n)
⊢ x ^ n.centralBinom.factorization x = 1

Proof state:
n : ℕ
n_large : 2 < n
no_prime : ¬∃ p, Nat.Prime p ∧ n < p ∧ p ≤ 2 * n
⊢ ∏ p ∈ Finset.range (2 * n / 3 + 1), p ^ n.centralBinom.factorization p =
    ∏ p ∈ Finset.range (2 * n + 1), p ^ n.centralBinom.factorization p

Tactic:
apply Finset.prod_subset

Result:
case h
n : ℕ
n_large : 2 < n
no_prime : ¬∃ p, Nat.Prime p ∧ n < p ∧ p ≤ 2 * n
⊢ Finset.range (2 * n / 3 + 1) ⊆ Finset.range (2 * n + 1)

case hf
n : ℕ
n_large : 2 < n
no_prime : ¬∃ p, Nat.Prime p ∧ n < p ∧ p ≤ 2 * n
⊢ ∀ x ∈ Finset.range (2 * n + 1), x ∉ Finset.range (2 * n / 3 + 1) → x ^ n.centralBinom.factorization x = 1

Proof state:
case hf
n : ℕ
n_large : 2 < n
x : ℕ
hx : x ≤ 2 * n
h2x : 2 * n < 3 * x
no_prime : x ≤ 2 * n → ¬Nat.Prime x ∨ x ≤ n
⊢ x ^ n.centralBinom.factorization x = 1

Tactic:
rcases no_prime hx with h | h

Result:
case hf.inl
n : ℕ
n_large : 2 < n
x : ℕ
hx : x ≤ 2 * n
h2x : 2 * n < 3 * x
no_prime : x ≤ 2 * n → ¬Nat.Prime x ∨ x ≤ n
h : ¬Nat.Prime x
⊢ x ^ n.centralBinom.factorization x = 1

case hf.inr
n : ℕ
n_large : 2 < n
x : ℕ
hx : x ≤ 2 * n
h2x : 2 * n < 3 * x
no_prime : x ≤ 2 * n → ¬Nat.Prime x ∨ x ≤ n
h : x ≤ n
⊢ x ^ n.centralBinom.factorization x = 1

Proof state:
case hf
n : ℕ
n_large : 2 < n
no_prime : ¬∃ p, Nat.Prime p ∧ n < p ∧ p ≤ 2 * n
x : ℕ
hx : x ∈ Finset.range (2 * n + 1)
h2x : x ∉ Finset.range (2 * n / 3 + 1)
⊢ x ^ n.centralBinom.factorization x = 1

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

Result:
case hf
n : ℕ
n_large : 2 < n
no_prime : ¬∃ p, Nat.Prime p ∧ n < p ∧ p ≤ 2 * n
x : ℕ
hx : x ≤ 2 * n
h2x : ¬x ≤ 2 * n / 3
⊢ x ^ n.centralBinom.factorization x = 1

Proof state:
n : ℕ
n_large : 2 < n
no_prime : ¬∃ p, Nat.Prime p ∧ n < p ∧ p ≤ 2 * n
⊢ n.centralBinom = ∏ p ∈ Finset.range (2 * n / 3 + 1), p ^ n.centralBinom.factorization p

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

Result:
n : ℕ
n_large : 2 < n
no_prime : ¬∃ p, Nat.Prime p ∧ n < p ∧ p ≤ 2 * n
⊢ ∏ p ∈ Finset.range (2 * n / 3 + 1), p ^ n.centralBinom.factorization p =
    ∏ p ∈ Finset.range (2 * n + 1), p ^ n.centralBinom.factorization p

Proof state:
case hf
n : ℕ
n_large : 2 < n
x : ℕ
hx : x ≤ 2 * n
h2x : 2 * n < 3 * x
no_prime : ¬(Nat.Prime x ∧ n < x ∧ x ≤ 2 * n)
⊢ x ^ n.centralBinom.factorization x = 1

Tactic:
rw [← and_assoc, not_and', not_and_or, not_lt] at no_prime

Result:
case hf
n : ℕ
n_large : 2 < n
x : ℕ
hx : x ≤ 2 * n
h2x : 2 * n < 3 * x
no_prime : x ≤ 2 * n → ¬Nat.Prime x ∨ x ≤ n
⊢ x ^ n.centralBinom.factorization x = 1

Proof state:
case hf.inl
n : ℕ
n_large : 2 < n
x : ℕ
hx : x ≤ 2 * n
h2x : 2 * n < 3 * x
no_prime : x ≤ 2 * n → ¬Nat.Prime x ∨ x ≤ n
h : ¬Nat.Prime x
⊢ x ^ n.centralBinom.factorization x = 1

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

Result:
no goals

Proof state:
case h
n : ℕ
n_large : 2 < n
no_prime : ¬∃ p, Nat.Prime p ∧ n < p ∧ p ≤ 2 * n
⊢ Finset.range (2 * n / 3 + 1) ⊆ Finset.range (2 * n + 1)

Tactic:
exact Finset.range_subset.2 (add_le_add_right (Nat.div_le_self _ _) _)

Result:
no goals