have : 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))
⊢ 4 ^ (↑n / 3) ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n))
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))