intro p hp _
case hf
n : ℕ
hn : 2 < n
⊢ ∀ (i : ℕ),
    i ∈ Finset.filter Nat.Prime (Finset.Icc 0 (2 * n / 3)) →
      ¬i ∈ Finset.filter Nat.Prime (Finset.Ioc (Nat.sqrt (2 * n)) (2 * n / 3)) → 1 ≤ i
case hf
n : ℕ
hn : 2 < n
p : ℕ
hp : p ∈ Finset.filter Nat.Prime (Finset.Icc 0 (2 * n / 3))
a✝ : ¬p ∈ Finset.filter Nat.Prime (Finset.Ioc (Nat.sqrt (2 * n)) (2 * n / 3))
⊢ 1 ≤ p