. apply Finset.prod_eq_one
  intro i hi
  specialize h i
  simp [primes] at *
  specialize h hi.left.left hi.left.right hi.right
  contradiction
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
case inr
n : ℕ
hn : 0 < n
hn' : 4000 ≤ n
h : ∏ p in primes (Finset.Ioc n (2 * n)), p = 1
⊢ False