rw [Real.rpow_le_rpow_left_iff (by norm_cast; linarith)]
case h₁
n : ℕ
hn : 0 < n
⊢ (2 * ↑n) ^ ↑(1 + Nat.sqrt (2 * n)) ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n))
case h₁
n : ℕ
hn : 0 < n
⊢ ↑(1 + Nat.sqrt (2 * n)) ≤ 1 + Real.sqrt (2 * ↑n)