cases hp with
| intro p hp =>
  exists p
  apply And.intro hp.right
  refine List.all₂_iff_forall.mp ?_ p hp.left
  exact allPrimeNums
n : ℕ
hn_pos : 0 < n
hn_lt : n ≤ 4000
hp✝ : n ∈ Set.Icc 1 4000 → ∃ p, p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)
hp : ∃ p, p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)
⊢ ∃ p, p ∈ Set.Ioc n (2 * n) ∧ Nat.Prime p
no goals