apply hp
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)
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)
⊢ n ∈ Set.Icc 1 4000