clear this
case inr
n : ℕ
hn : 0 < n
hn' : 4000 ≤ n
this : 81 / 2 < ↑n
h' : 4 ^ ↑n < 2 ^ (20 * (2 * ↑n) ^ (2 / 3))
⊢ False
case inr
n : ℕ
hn : 0 < n
hn' : 4000 ≤ n
h' : 4 ^ ↑n < 2 ^ (20 * (2 * ↑n) ^ (2 / 3))
⊢ False