apply Finset.monotone_filter_left
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 h.a
n : ℕ
hn : 2 < n
⊢ Finset.Ioc (Nat.sqrt (2 * n)) (2 * n / 3) ≤ Finset.Icc 0 (2 * n / 3)