rw [← @Finset.prod_filter_of_ne _ _ _ _ _ Nat.Prime]
n a b : ℕ
ha : Nat.sqrt (2 * n) ≤ a
⊢ ∏ p in Finset.Ioc a b, p ^ ↑(Nat.factorization (Nat.centralBinom n)) p ≤
    ∏ p in Finset.filter Nat.Prime (Finset.Ioc a b), p
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