apply Real.rpow_le_rpow _ h (by linarith)
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ (4 ^ (n / 3)) ^ 3 ≤ ((2 * n) ^ (1 + Real.sqrt (2 * n))) ^ 3
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 0 ≤ 4 ^ (n / 3)