. intro p hp _
  simp at hp
  replace hp := Nat.Prime.one_lt hp.right
  linarith
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
no goals