. simp [mul_add, add_mul]
  apply ltTwoMulSqrtTwoMul
  linarith
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 18 * (1 + Real.sqrt (2 * n)) < (2 + 18) * Real.sqrt (2 * n)

n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 0 < (2 * n) ^ 6⁻¹
n : ℝ
hn : 81 / 2 < n
h : 4 ^ (n / 3) ≤ (2 * n) ^ (1 + Real.sqrt (2 * n))
⊢ 0 < (2 * n) ^ 6⁻¹