apply Finset.prod_subset
n : ℕ
n_large : 2 < n
no_prime : ¬∃ p, p.Prime ∧ 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
case h
n : ℕ
n_large : 2 < n
no_prime : ¬∃ p, p.Prime ∧ 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, p.Prime ∧ n < p ∧ p ≤ 2 * n
⊢ ∀ x ∈ Finset.range (2 * n + 1), x ∉ Finset.range (2 * n / 3 + 1) → x ^ n.centralBinom.factorization x = 1