have : ∏ x : ℕ in S, f x = ∏ x : ℕ in Finset.range (2 * n / 3 + 1), f x := by
  refine' Finset.prod_filter_of_ne fun p _ h => _
  contrapose! h
  dsimp [f]
  rw [factorization_eq_zero_of_non_prime n.centralBinom h, _root_.pow_zero]
n : ℕ
n_big : 2 < n
no_prime : ¬∃ p, p.Prime ∧ 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
⊢ n.centralBinom ≤ (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3)
n : ℕ
n_big : 2 < n
no_prime : ¬∃ p, p.Prime ∧ 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
⊢ n.centralBinom ≤ (2 * n) ^ (2 * n).sqrt * 4 ^ (2 * n / 3)