. apply le_trans FactorizationCentralBinom.prodIocSqrtPowLeProdPrimes
  apply le_trans _ (@prodPrimesLePowFour (2*n/3))
  rw [prodPrimes, Finset.range_eq_Ico, Nat.Ico_succ_right]
  apply Finset.prod_le_prod_of_subset_of_one_le' <;> rw [primes]
  . apply Finset.monotone_filter_left
    exact Finset.Ioc_subset_Iic_self
  . intro p hp _
    simp at hp
    replace hp := Nat.Prime.one_lt hp.right
    linarith
case h.h₂.h₁
n : ℕ
hn : 2 < n
⊢ ∏ x in Finset.Ioc (Nat.sqrt (2 * n)) (2 * n / 3), x ^ ↑(Nat.factorization (Nat.centralBinom n)) x ≤
    4 ^ Nat.pred (2 * n / 3)

case h.h₂.h₂
n : ℕ
hn : 2 < n
⊢ ∏ x in Finset.Ioc (2 * n / 3) (2 * n), x ^ ↑(Nat.factorization (Nat.centralBinom n)) x ≤
    ∏ p in primes (Finset.Ioc n (2 * n)), p
case h.h₂.h₂
n : ℕ
hn : 2 < n
⊢ ∏ x in Finset.Ioc (2 * n / 3) (2 * n), x ^ ↑(Nat.factorization (Nat.centralBinom n)) x ≤
    ∏ p in primes (Finset.Ioc n (2 * n)), p