. apply FactorizationCentralBinom.prodIocSqrtLePowLeProdPrimes
  exact sqrtTwoMulLeSelf (le_of_lt hn)
case h.h₂.h₂.h
n : ℕ
hn : 2 < n
⊢ ∏ i in Finset.Ioc n (2 * n), i ^ ↑(Nat.factorization (Nat.centralBinom n)) i ≤ ∏ p in primes (Finset.Ioc n (2 * n)), p
no goals