. apply Finset.monotone_filter_left
  exact Finset.Ioc_subset_Iic_self
case h
n : ℕ
hn : 2 < n
⊢ Finset.filter Nat.Prime (Finset.Ioc (Nat.sqrt (2 * n)) (2 * n / 3)) ⊆
    Finset.filter Nat.Prime (Finset.Icc 0 (2 * n / 3))

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
⊢ ∀ (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