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