simp [Real.rpow_def_of_pos]
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 + 2 * ↑n / 3) = 4 ^ ↑n
case this
n : ℕ
hn : 0 < n
h : ↑(4 ^ n) ≤ ↑((2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3))
⊢ ↑n / 3 + 2 * ↑n / 3 = ↑n ∨ 4 = -1