. conv => lhs; rw [← Finset.prod_Ioc_consecutive _ (mulDivLeSelf (by norm_num)) (by linarith : n ≤ 2*n)]
  apply mulRightLeOfLeOne
  . apply le_of_eq
    apply Finset.prod_eq_one
    intro x hx
    simp at hx
    rw [Nat.factorization_centralBinom_of_two_mul_self_lt_three_mul hn hx.right]
    . simp
    . apply @Nat.lt_of_div_lt_div _ _ 3
      simp
      exact hx.left
  . apply FactorizationCentralBinom.prodIocSqrtLePowLeProdPrimes
    exact sqrtTwoMulLeSelf (le_of_lt hn)
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
no goals