apply Finset.prod_le_prod_of_subset_of_one_le' <;> rw [primes]
n : ℕ
hn : 2 < n
⊢ ∏ p in primes (Finset.Ioc (Nat.sqrt (2 * n)) (2 * n / 3)), p ≤ ∏ p in primes (Finset.Icc 0 (2 * n / 3)), p
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