rw [← div_le_one (rpow_pos_of_pos four_pos x), ← div_div_eq_mul_div, ← rpow_sub four_pos, ←
  mul_div 2 x, mul_div_left_comm, ← mul_one_sub, (by norm_num1 : (1 : ℝ) - 2 / 3 = 1 / 3),
  mul_one_div, ← log_nonpos_iff (hf' x h5), ← hf x h5]
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
⊢ x * (2 * x) ^ (2 * x).sqrt * 4 ^ (2 * x / 3) ≤ 4 ^ x
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
⊢ f x ≤ 0