clear h
case inr
n : ℕ
hn : 0 < n
hn' : 4000 ≤ n
h : ∏ p in primes (Finset.Ioc n (2 * n)), p = 1
h' : 4 ^ n ≤ (2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3)
⊢ False
case inr
n : ℕ
hn : 0 < n
hn' : 4000 ≤ n
h' : 4 ^ n ≤ (2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3)
⊢ False