replace h : ∏ p in primes (Finset.Ioc n (2*n)), p = 1
case inr
n : ℕ
hn : 0 < n
hn' : 4000 ≤ n
h : ∀ (x : ℕ), n < x → x ≤ 2 * n → ¬Nat.Prime x
⊢ False
case h
n : ℕ
hn : 0 < n
hn' : 4000 ≤ n
h : ∀ (x : ℕ), n < x → x ≤ 2 * n → ¬Nat.Prime x
⊢ ∏ p in primes (Finset.Ioc n (2 * n)), p = 1

case inr
n : ℕ
hn : 0 < n
hn' : 4000 ≤ n
h : ∏ p in primes (Finset.Ioc n (2 * n)), p = 1
⊢ False