rw [hf _ (by norm_num1), log_nonneg_iff (by positivity), this, one_le_div (by norm_num1)]
case refine'_1
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : (2 * 18).sqrt = 6
⊢ 0 ≤ f 18
case refine'_1
x : ℝ
n_large : 512 ≤ x
f : ℝ → ℝ := fun x => x.log + (2 * x).sqrt * (2 * x).log - log 4 / 3 * x
hf' : ∀ (x : ℝ), 0 < x → 0 < x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)
hf : ∀ (x : ℝ), 0 < x → f x = (x * (2 * x) ^ (2 * x).sqrt / 4 ^ (x / 3)).log
h5 : 0 < x
h : ConcaveOn ℝ (Set.Ioi 0.5) f
this : (2 * 18).sqrt = 6
⊢ 4 ^ (18 / 3) ≤ 18 * (2 * 18) ^ 6