simp [primes] at *
case h.h
n : ℕ
hn : 0 < n
hn' : 4000 ≤ n
i : ℕ
hi : i ∈ primes (Finset.Ioc n (2 * n))
h : n < i → i ≤ 2 * n → ¬Nat.Prime i
⊢ i = 1
case h.h
n : ℕ
hn : 0 < n
hn' : 4000 ≤ n
i : ℕ
h : n < i → i ≤ 2 * n → ¬Nat.Prime i
hi : (n < i ∧ i ≤ 2 * n) ∧ Nat.Prime i
⊢ i = 1