intro i hi
case h.h
n : ℕ
hn : 0 < n
hn' : 4000 ≤ n
h : ∀ (x : ℕ), n < x → x ≤ 2 * n → ¬Nat.Prime x
⊢ ∀ (x : ℕ), x ∈ primes (Finset.Ioc n (2 * n)) → x = 1
case h.h
n : ℕ
hn : 0 < n
hn' : 4000 ≤ n
h : ∀ (x : ℕ), n < x → x ≤ 2 * n → ¬Nat.Prime x
i : ℕ
hi : i ∈ primes (Finset.Ioc n (2 * n))
⊢ i = 1