rw [← Real.rpow_mul (by norm_num)]
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 4 ^ n ≤ (4 ^ (n / 3)) ^ 3
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 4 ^ n ≤ 4 ^ (n / 3 * 3)