. apply Finset.prod_le_prod'
  simp
  intro p hbp _ hp
  replace hbp := lt_of_le_of_lt ha hbp
  conv => rhs; rw [← Nat.pow_one p]
  rw [pow_le_pow_iff (Nat.Prime.one_lt hp)]
  rw [Nat.sqrt_lt'] at hbp
  exact leOne hp hbp
n a b : ℕ
ha : Nat.sqrt (2 * n) ≤ a
⊢ ∏ x in Finset.filter Nat.Prime (Finset.Ioc a b), x ^ ↑(Nat.factorization (Nat.centralBinom n)) x ≤
    ∏ p in Finset.filter Nat.Prime (Finset.Ioc a b), p

case hp
n a b : ℕ
ha : Nat.sqrt (2 * n) ≤ a
⊢ ∀ (x : ℕ), x ∈ Finset.Ioc a b → x ^ ↑(Nat.factorization (Nat.centralBinom n)) x ≠ 1 → Nat.Prime x
case hp
n a b : ℕ
ha : Nat.sqrt (2 * n) ≤ a
⊢ ∀ (x : ℕ), x ∈ Finset.Ioc a b → x ^ ↑(Nat.factorization (Nat.centralBinom n)) x ≠ 1 → Nat.Prime x