apply le_trans _ (@prodPrimesLePowFour (2*n/3))
case h.h₂.h₁
n : ℕ
hn : 2 < n
⊢ ∏ p in primes (Finset.Ioc (Nat.sqrt (2 * n)) (2 * n / 3)), p ≤ 4 ^ Nat.pred (2 * n / 3)
n : ℕ
hn : 2 < n
⊢ ∏ p in primes (Finset.Ioc (Nat.sqrt (2 * n)) (2 * n / 3)), p ≤ prodPrimes (2 * n / 3)