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