rw [← Real.rpow_mul (by linarith)]
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ (2 * n) ^ 3 < 20 ^ 3 * ((2 * n) ^ (2 / 3)) ^ 3 ↔ n < 4000
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ (2 * n) ^ 3 < 20 ^ 3 * (2 * n) ^ (2 / 3 * 3) ↔ n < 4000