rw [Real.rpow_lt_rpow_left_iff (by linarith)]
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 2 ^ (6 * (2 * n) ^ 6⁻¹ * ((1 + Real.sqrt (2 * n)) * 3)) < 2 ^ (20 * (2 * n) ^ (2 / 3))
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 6 * (2 * n) ^ 6⁻¹ * ((1 + Real.sqrt (2 * n)) * 3) < 20 * (2 * n) ^ (2 / 3)