calc
_ = (18 * (1 + Real.sqrt (2*n))) * ((2*n)^6⁻¹) := by linarith
_ < (2 + 18) * Real.sqrt (2*n) * (2*n)^6⁻¹ := by
  rw [mul_lt_mul_right]
  . simp [mul_add, add_mul]
    apply ltTwoMulSqrtTwoMul
    linarith
  . apply Real.rpow_pos_of_pos
    linarith
_ = 20 * (Real.sqrt (2*n) * (2*n)^6⁻¹) := by linarith
_ = _ := by
  simp [Real.sqrt_eq_rpow]
  rw [← Real.rpow_add (by linarith)]
  norm_num
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)
no goals