. have hs : Finset.Ioc (Nat.sqrt (2*n)) (2*n) ⊆ Finset.Ioc (Nat.sqrt (2*n)) (2*n/3) ∪ Finset.Ioc (2*n/3) (2*n)
  . repeat rw [← Nat.Ico_succ_succ]
    apply Finset.Ico_subset_Ico_union_Ico
  apply le_trans (prodLeProdMulProdOfUnionOfOneLe hs (powFactorizationPos _))
  clear hs
  apply Nat.mul_le_mul
  . 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
  . 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₂
n : ℕ
hn : 2 < n
⊢ ∏ x in Finset.Ioc (Nat.sqrt (2 * n)) (2 * n), x ^ ↑(Nat.factorization (Nat.centralBinom n)) x ≤
    4 ^ Nat.pred (2 * n / 3) * ∏ p in primes (Finset.Ioc n (2 * n)), p
no goals