. rw [eq_div_iff]
  swap; {apply ne_of_gt; apply Real.rpow_pos_of_pos (by norm_num)}
  rw [← Real.rpow_add (by norm_num)]
  simp [Real.rpow_def_of_pos]  norm_num
  push_cast
  simp [div_add_div_same]
  norm_cast
  rw [(by linarith : n + 2*n = n*3)]
  simp
case this
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ 4 ^ (↑n / 3) = 4 ^ ↑n / 4 ^ (2 * ↑n / 3)

n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
this : 4 ^ (↑n / 3) = 4 ^ ↑n / 4 ^ (2 * ↑n / 3)
⊢ 4 ^ (↑n / 3) ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n))
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
this : 4 ^ (↑n / 3) = 4 ^ ↑n / 4 ^ (2 * ↑n / 3)
⊢ 4 ^ (↑n / 3) ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n))