rw [FactorizationCentralBinom.prodRangePowEqProdIcoPowOfLeTwo (Nat.le_succ _ : 1 ≤ 2)]
case h.h₁
n : ℕ
hn : 2 < n
⊢ ∏ x in Finset.range (Nat.succ (Nat.sqrt (2 * n))), x ^ ↑(Nat.factorization (Nat.centralBinom n)) x ≤
    (2 * n) ^ Nat.sqrt (2 * n)
case h.h₁
n : ℕ
hn : 2 < n
⊢ ∏ p in Finset.Ico 1 (Nat.succ (Nat.sqrt (2 * n))), p ^ ↑(Nat.factorization (Nat.centralBinom n)) p ≤
    (2 * n) ^ Nat.sqrt (2 * n)