have hp : ∃ p, p ∈ nums ∧ p ∈ Set.Ioc n (2*n)
n : ℕ
hn_pos : 0 < n
hn_lt : n ≤ 4000
hp : n ∈ Set.Icc 1 4000 → ∃ p, p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)
⊢ ∃ p, p ∈ Set.Ioc n (2 * n) ∧ Nat.Prime p
case hp
n : ℕ
hn_pos : 0 < n
hn_lt : n ≤ 4000
hp : n ∈ Set.Icc 1 4000 → ∃ p, p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)
⊢ ∃ p, p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)

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