conv => lhs; rw [← Finset.prod_Ico_consecutive _ (Nat.zero_le _) (Nat.succ_le_succ (Nat.sqrt_le_self _))]
case h
n : ℕ
hn : 2 < n
⊢ ∏ p in Finset.Ico 0 (2 * n + 1), p ^ ↑(Nat.factorization (Nat.centralBinom n)) p ≤
    (2 * n) ^ Nat.sqrt (2 * n) * 4 ^ Nat.pred (2 * n / 3) * ∏ p in primes (Finset.Ioc n (2 * n)), p
case h
n : ℕ
hn : 2 < n
⊢ (∏ i in Finset.Ico 0 (Nat.succ (Nat.sqrt (2 * n))), i ^ ↑(Nat.factorization (Nat.centralBinom n)) i) *
      ∏ i in Finset.Ico (Nat.succ (Nat.sqrt (2 * n))) (Nat.succ (2 * n)),
        i ^ ↑(Nat.factorization (Nat.centralBinom n)) i ≤
    (2 * n) ^ Nat.sqrt (2 * n) * 4 ^ Nat.pred (2 * n / 3) * ∏ p in primes (Finset.Ioc n (2 * n)), p