refine List.all₂_iff_forall.mp ?_ p hp.left
case intro
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 : ℕ
hp : p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)
⊢ Nat.Prime p
case intro
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 : ℕ
hp : p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)
⊢ List.All₂ Nat.Prime nums