Theorem: fourPowLeMulProdPrimes (FromTheBook/Ch02/Bertrand/CentralBinom.lean)

State before:
n : ℕ
hn : 2 < n
⊢ 4 ^ n ≤ (2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3) * ∏ p in primes (Finset.Ioc n (2 * n)), p
Tactic:
apply le_trans (Nat.four_pow_le_two_mul_self_mul_centralBinom _ (by linarith))
State after:
n : ℕ
hn : 2 < n
⊢ 2 * n * Nat.centralBinom n ≤
    (2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3) * ∏ p in primes (Finset.Ioc n (2 * n)), p

State before:
n : ℕ
hn : 2 < n
⊢ 2 * n * Nat.centralBinom n ≤
    (2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3) * ∏ p in primes (Finset.Ioc n (2 * n)), p
Tactic:
rw [Nat.one_add, Nat.pow_succ]
State after:
n : ℕ
hn : 2 < n
⊢ 2 * n * Nat.centralBinom n ≤
    (2 * n) ^ Nat.sqrt (2 * n) * (2 * n) * 4 ^ Nat.pred (2 * n / 3) * ∏ p in primes (Finset.Ioc n (2 * n)), p

State before:
n : ℕ
hn : 2 < n
⊢ 2 * n * Nat.centralBinom n ≤
    (2 * n) ^ Nat.sqrt (2 * n) * (2 * n) * 4 ^ Nat.pred (2 * n / 3) * ∏ p in primes (Finset.Ioc n (2 * n)), p
Tactic:
have : ∀ {x y z : ℕ}, x * (2*n) * y * z = (2*n) * (x * y * z) := by intro x y z; linarith
State after:
n : ℕ
hn : 2 < n
this : ∀ {x y z : ℕ}, x * (2 * n) * y * z = 2 * n * (x * y * z)
⊢ 2 * n * Nat.centralBinom n ≤
    (2 * n) ^ Nat.sqrt (2 * n) * (2 * n) * 4 ^ Nat.pred (2 * n / 3) * ∏ p in primes (Finset.Ioc n (2 * n)), p

State before:
n : ℕ
hn : 2 < n
this : ∀ {x y z : ℕ}, x * (2 * n) * y * z = 2 * n * (x * y * z)
⊢ 2 * n * Nat.centralBinom n ≤
    (2 * n) ^ Nat.sqrt (2 * n) * (2 * n) * 4 ^ Nat.pred (2 * n / 3) * ∏ p in primes (Finset.Ioc n (2 * n)), p
Tactic:
rw [this]
State after:
n : ℕ
hn : 2 < n
this : ∀ {x y z : ℕ}, x * (2 * n) * y * z = 2 * n * (x * y * z)
⊢ 2 * n * Nat.centralBinom n ≤
    2 * n * ((2 * n) ^ Nat.sqrt (2 * n) * 4 ^ Nat.pred (2 * n / 3) * ∏ p in primes (Finset.Ioc n (2 * n)), p)

State before:
n : ℕ
hn : 2 < n
this : ∀ {x y z : ℕ}, x * (2 * n) * y * z = 2 * n * (x * y * z)
⊢ 2 * n * Nat.centralBinom n ≤
    2 * n * ((2 * n) ^ Nat.sqrt (2 * n) * 4 ^ Nat.pred (2 * n / 3) * ∏ p in primes (Finset.Ioc n (2 * n)), p)
Tactic:
clear this
State after:
n : ℕ
hn : 2 < n
⊢ 2 * n * Nat.centralBinom n ≤
    2 * n * ((2 * n) ^ Nat.sqrt (2 * n) * 4 ^ Nat.pred (2 * n / 3) * ∏ p in primes (Finset.Ioc n (2 * n)), p)

State before:
n : ℕ
hn : 2 < n
⊢ 2 * n * Nat.centralBinom n ≤
    2 * n * ((2 * n) ^ Nat.sqrt (2 * n) * 4 ^ Nat.pred (2 * n / 3) * ∏ p in primes (Finset.Ioc n (2 * n)), p)
Tactic:
apply Nat.mul_le_mul_left
State after:
case h
n : ℕ
hn : 2 < n
⊢ Nat.centralBinom n ≤ (2 * n) ^ Nat.sqrt (2 * n) * 4 ^ Nat.pred (2 * n / 3) * ∏ p in primes (Finset.Ioc n (2 * n)), p

State before:
case h
n : ℕ
hn : 2 < n
⊢ Nat.centralBinom n ≤ (2 * n) ^ Nat.sqrt (2 * n) * 4 ^ Nat.pred (2 * n / 3) * ∏ p in primes (Finset.Ioc n (2 * n)), p
Tactic:
rw [← Nat.prod_pow_factorization_centralBinom]
State after:
case h
n : ℕ
hn : 2 < n
⊢ ∏ p in Finset.range (2 * n + 1), p ^ ↑(Nat.factorization (Nat.centralBinom n)) p ≤
    (2 * n) ^ Nat.sqrt (2 * n) * 4 ^ Nat.pred (2 * n / 3) * ∏ p in primes (Finset.Ioc n (2 * n)), p

State before:
case h
n : ℕ
hn : 2 < n
⊢ ∏ p in Finset.range (2 * n + 1), p ^ ↑(Nat.factorization (Nat.centralBinom n)) p ≤
    (2 * n) ^ Nat.sqrt (2 * n) * 4 ^ Nat.pred (2 * n / 3) * ∏ p in primes (Finset.Ioc n (2 * n)), p
Tactic:
rw [Finset.range_eq_Ico]
State after:
case h
n : ℕ
hn : 2 < n
⊢ ∏ p in Finset.Ico 0 (2 * n + 1), p ^ ↑(Nat.factorization (Nat.centralBinom n)) p ≤
    (2 * n) ^ Nat.sqrt (2 * n) * 4 ^ Nat.pred (2 * n / 3) * ∏ p in primes (Finset.Ioc n (2 * n)), p

State before:
case h
n : ℕ
hn : 2 < n
⊢ ∏ p in Finset.Ico 0 (2 * n + 1), p ^ ↑(Nat.factorization (Nat.centralBinom n)) p ≤
    (2 * n) ^ Nat.sqrt (2 * n) * 4 ^ Nat.pred (2 * n / 3) * ∏ p in primes (Finset.Ioc n (2 * n)), p
Tactic:
conv => lhs; rw [← Finset.prod_Ico_consecutive _ (Nat.zero_le _) (Nat.succ_le_succ (Nat.sqrt_le_self _))]
State after:
case h
n : ℕ
hn : 2 < n
⊢ (∏ i in Finset.Ico 0 (Nat.succ (Nat.sqrt (2 * n))), i ^ ↑(Nat.factorization (Nat.centralBinom n)) i) *
      ∏ i in Finset.Ico (Nat.succ (Nat.sqrt (2 * n))) (Nat.succ (2 * n)),
        i ^ ↑(Nat.factorization (Nat.centralBinom n)) i ≤
    (2 * n) ^ Nat.sqrt (2 * n) * 4 ^ Nat.pred (2 * n / 3) * ∏ p in primes (Finset.Ioc n (2 * n)), p

State before:
case h
n : ℕ
hn : 2 < n
⊢ (∏ i in Finset.Ico 0 (Nat.succ (Nat.sqrt (2 * n))), i ^ ↑(Nat.factorization (Nat.centralBinom n)) i) *
      ∏ i in Finset.Ico (Nat.succ (Nat.sqrt (2 * n))) (Nat.succ (2 * n)),
        i ^ ↑(Nat.factorization (Nat.centralBinom n)) i ≤
    (2 * n) ^ Nat.sqrt (2 * n) * 4 ^ Nat.pred (2 * n / 3) * ∏ p in primes (Finset.Ioc n (2 * n)), p
Tactic:
simp [Nat.Ico_succ_succ]
State after:
case h
n : ℕ
hn : 2 < n
⊢ (∏ x in Finset.range (Nat.succ (Nat.sqrt (2 * n))), x ^ ↑(Nat.factorization (Nat.centralBinom n)) x) *
      ∏ x in Finset.Ioc (Nat.sqrt (2 * n)) (2 * n), x ^ ↑(Nat.factorization (Nat.centralBinom n)) x ≤
    (2 * n) ^ Nat.sqrt (2 * n) * 4 ^ Nat.pred (2 * n / 3) * ∏ p in primes (Finset.Ioc n (2 * n)), p

State before:
case h
n : ℕ
hn : 2 < n
⊢ (∏ x in Finset.range (Nat.succ (Nat.sqrt (2 * n))), x ^ ↑(Nat.factorization (Nat.centralBinom n)) x) *
      ∏ x in Finset.Ioc (Nat.sqrt (2 * n)) (2 * n), x ^ ↑(Nat.factorization (Nat.centralBinom n)) x ≤
    (2 * n) ^ Nat.sqrt (2 * n) * 4 ^ Nat.pred (2 * n / 3) * ∏ p in primes (Finset.Ioc n (2 * n)), p
Tactic:
conv => rhs; rw [mul_assoc]
State after:
case h
n : ℕ
hn : 2 < n
⊢ (∏ x in Finset.range (Nat.succ (Nat.sqrt (2 * n))), x ^ ↑(Nat.factorization (Nat.centralBinom n)) x) *
      ∏ x in Finset.Ioc (Nat.sqrt (2 * n)) (2 * n), x ^ ↑(Nat.factorization (Nat.centralBinom n)) x ≤
    (2 * n) ^ Nat.sqrt (2 * n) * (4 ^ Nat.pred (2 * n / 3) * ∏ p in primes (Finset.Ioc n (2 * n)), p)

State before:
case h
n : ℕ
hn : 2 < n
⊢ (∏ x in Finset.range (Nat.succ (Nat.sqrt (2 * n))), x ^ ↑(Nat.factorization (Nat.centralBinom n)) x) *
      ∏ x in Finset.Ioc (Nat.sqrt (2 * n)) (2 * n), x ^ ↑(Nat.factorization (Nat.centralBinom n)) x ≤
    (2 * n) ^ Nat.sqrt (2 * n) * (4 ^ Nat.pred (2 * n / 3) * ∏ p in primes (Finset.Ioc n (2 * n)), p)
Tactic:
apply Nat.mul_le_mul
State after:
case h.h₁
n : ℕ
hn : 2 < n
⊢ ∏ x in Finset.range (Nat.succ (Nat.sqrt (2 * n))), x ^ ↑(Nat.factorization (Nat.centralBinom n)) x ≤
    (2 * n) ^ Nat.sqrt (2 * n)

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

State before:
case h.h₁
n : ℕ
hn : 2 < n
⊢ ∏ x in Finset.range (Nat.succ (Nat.sqrt (2 * n))), x ^ ↑(Nat.factorization (Nat.centralBinom n)) x ≤
    (2 * n) ^ Nat.sqrt (2 * n)

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
Tactic:
. rw [FactorizationCentralBinom.prodRangePowEqProdIcoPowOfLeTwo (Nat.le_succ _ : 1 ≤ 2)]
  apply le_of_le_of_eq (FactorizationCentralBinom.prodIcoPowLePow' _)
  . norm_num
  . intro hn; rw [hn]; norm_num
State after:
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

State before:
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
Tactic:
. 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)
State after:
no goals

State before:
n : ℕ
hn : 2 < n
⊢ 0 < n
Tactic:
linarith
State after:
no goals

State before:
n : ℕ
hn : 2 < n
⊢ ∀ {x y z : ℕ}, x * (2 * n) * y * z = 2 * n * (x * y * z)
Tactic:
intro x y z
State after:
n : ℕ
hn : 2 < n
x y z : ℕ
⊢ x * (2 * n) * y * z = 2 * n * (x * y * z)

State before:
n : ℕ
hn : 2 < n
x y z : ℕ
⊢ x * (2 * n) * y * z = 2 * n * (x * y * z)
Tactic:
linarith
State after:
no goals

State before:
case h.h₁
n : ℕ
hn : 2 < n
⊢ ∏ x in Finset.range (Nat.succ (Nat.sqrt (2 * n))), x ^ ↑(Nat.factorization (Nat.centralBinom n)) x ≤
    (2 * n) ^ Nat.sqrt (2 * n)
Tactic:
rw [FactorizationCentralBinom.prodRangePowEqProdIcoPowOfLeTwo (Nat.le_succ _ : 1 ≤ 2)]
State after:
case h.h₁
n : ℕ
hn : 2 < n
⊢ ∏ p in Finset.Ico 1 (Nat.succ (Nat.sqrt (2 * n))), p ^ ↑(Nat.factorization (Nat.centralBinom n)) p ≤
    (2 * n) ^ Nat.sqrt (2 * n)

State before:
case h.h₁
n : ℕ
hn : 2 < n
⊢ ∏ p in Finset.Ico 1 (Nat.succ (Nat.sqrt (2 * n))), p ^ ↑(Nat.factorization (Nat.centralBinom n)) p ≤
    (2 * n) ^ Nat.sqrt (2 * n)
Tactic:
apply le_of_le_of_eq (FactorizationCentralBinom.prodIcoPowLePow' _)
State after:
case h.h₁
n : ℕ
hn : 2 < n
⊢ (2 * n) ^ Finset.card (Finset.Ico 1 (Nat.succ (Nat.sqrt (2 * n)))) = (2 * n) ^ Nat.sqrt (2 * n)

n : ℕ
hn : 2 < n
⊢ n = 0 → Finset.Ico 1 (Nat.succ (Nat.sqrt (2 * n))) = ∅

State before:
case h.h₁
n : ℕ
hn : 2 < n
⊢ (2 * n) ^ Finset.card (Finset.Ico 1 (Nat.succ (Nat.sqrt (2 * n)))) = (2 * n) ^ Nat.sqrt (2 * n)

n : ℕ
hn : 2 < n
⊢ n = 0 → Finset.Ico 1 (Nat.succ (Nat.sqrt (2 * n))) = ∅
Tactic:
. norm_num
State after:
n : ℕ
hn : 2 < n
⊢ n = 0 → Finset.Ico 1 (Nat.succ (Nat.sqrt (2 * n))) = ∅

State before:
n : ℕ
hn : 2 < n
⊢ n = 0 → Finset.Ico 1 (Nat.succ (Nat.sqrt (2 * n))) = ∅
Tactic:
. intro hn; rw [hn]; norm_num
State after:
no goals

State before:
case h.h₁
n : ℕ
hn : 2 < n
⊢ (2 * n) ^ Finset.card (Finset.Ico 1 (Nat.succ (Nat.sqrt (2 * n)))) = (2 * n) ^ Nat.sqrt (2 * n)
Tactic:
norm_num
State after:
no goals

State before:
n : ℕ
hn : 2 < n
⊢ n = 0 → Finset.Ico 1 (Nat.succ (Nat.sqrt (2 * n))) = ∅
Tactic:
intro hn
State after:
n : ℕ
hn✝ : 2 < n
hn : n = 0
⊢ Finset.Ico 1 (Nat.succ (Nat.sqrt (2 * n))) = ∅

State before:
n : ℕ
hn✝ : 2 < n
hn : n = 0
⊢ Finset.Ico 1 (Nat.succ (Nat.sqrt (2 * n))) = ∅
Tactic:
rw [hn]
State after:
n : ℕ
hn✝ : 2 < n
hn : n = 0
⊢ Finset.Ico 1 (Nat.succ (Nat.sqrt (2 * 0))) = ∅

State before:
n : ℕ
hn✝ : 2 < n
hn : n = 0
⊢ Finset.Ico 1 (Nat.succ (Nat.sqrt (2 * 0))) = ∅
Tactic:
norm_num
State after:
no goals

State before:
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
Tactic:
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)
State after:
case hs
n : ℕ
hn : 2 < n
⊢ Finset.Ioc (Nat.sqrt (2 * n)) (2 * n) ⊆ Finset.Ioc (Nat.sqrt (2 * n)) (2 * n / 3) ∪ Finset.Ioc (2 * n / 3) (2 * n)

case h.h₂
n : ℕ
hn : 2 < n
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)
⊢ ∏ 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

State before:
case hs
n : ℕ
hn : 2 < n
⊢ Finset.Ioc (Nat.sqrt (2 * n)) (2 * n) ⊆ Finset.Ioc (Nat.sqrt (2 * n)) (2 * n / 3) ∪ Finset.Ioc (2 * n / 3) (2 * n)

case h.h₂
n : ℕ
hn : 2 < n
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)
⊢ ∏ 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
Tactic:
. repeat rw [← Nat.Ico_succ_succ]
  apply Finset.Ico_subset_Ico_union_Ico
State after:
case h.h₂
n : ℕ
hn : 2 < n
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)
⊢ ∏ 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

State before:
case h.h₂
n : ℕ
hn : 2 < n
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)
⊢ ∏ 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
Tactic:
apply le_trans (prodLeProdMulProdOfUnionOfOneLe hs (powFactorizationPos _))
State after:
case h.h₂
n : ℕ
hn : 2 < n
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)
⊢ (∏ x in Finset.Ioc (Nat.sqrt (2 * n)) (2 * n / 3), x ^ ↑(Nat.factorization (Nat.centralBinom n)) x) *
      ∏ x in Finset.Ioc (2 * n / 3) (2 * n), x ^ ↑(Nat.factorization (Nat.centralBinom n)) x ≤
    4 ^ Nat.pred (2 * n / 3) * ∏ p in primes (Finset.Ioc n (2 * n)), p

State before:
case h.h₂
n : ℕ
hn : 2 < n
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)
⊢ (∏ x in Finset.Ioc (Nat.sqrt (2 * n)) (2 * n / 3), x ^ ↑(Nat.factorization (Nat.centralBinom n)) x) *
      ∏ x in Finset.Ioc (2 * n / 3) (2 * n), x ^ ↑(Nat.factorization (Nat.centralBinom n)) x ≤
    4 ^ Nat.pred (2 * n / 3) * ∏ p in primes (Finset.Ioc n (2 * n)), p
Tactic:
clear hs
State after:
case h.h₂
n : ℕ
hn : 2 < n
⊢ (∏ x in Finset.Ioc (Nat.sqrt (2 * n)) (2 * n / 3), x ^ ↑(Nat.factorization (Nat.centralBinom n)) x) *
      ∏ x in Finset.Ioc (2 * n / 3) (2 * n), x ^ ↑(Nat.factorization (Nat.centralBinom n)) x ≤
    4 ^ Nat.pred (2 * n / 3) * ∏ p in primes (Finset.Ioc n (2 * n)), p

State before:
case h.h₂
n : ℕ
hn : 2 < n
⊢ (∏ x in Finset.Ioc (Nat.sqrt (2 * n)) (2 * n / 3), x ^ ↑(Nat.factorization (Nat.centralBinom n)) x) *
      ∏ x in Finset.Ioc (2 * n / 3) (2 * n), x ^ ↑(Nat.factorization (Nat.centralBinom n)) x ≤
    4 ^ Nat.pred (2 * n / 3) * ∏ p in primes (Finset.Ioc n (2 * n)), p
Tactic:
apply Nat.mul_le_mul
State after:
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

State before:
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
Tactic:
. 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
State after:
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

State before:
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
Tactic:
. 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)
State after:
no goals

State before:
case hs
n : ℕ
hn : 2 < n
⊢ Finset.Ioc (Nat.sqrt (2 * n)) (2 * n) ⊆ Finset.Ioc (Nat.sqrt (2 * n)) (2 * n / 3) ∪ Finset.Ioc (2 * n / 3) (2 * n)
Tactic:
repeat rw [← Nat.Ico_succ_succ]
State after:
case hs
n : ℕ
hn : 2 < n
⊢ Finset.Ico (Nat.succ (Nat.sqrt (2 * n))) (Nat.succ (2 * n)) ⊆
    Finset.Ico (Nat.succ (Nat.sqrt (2 * n))) (Nat.succ (2 * n / 3)) ∪
      Finset.Ico (Nat.succ (2 * n / 3)) (Nat.succ (2 * n))

State before:
case hs
n : ℕ
hn : 2 < n
⊢ Finset.Ico (Nat.succ (Nat.sqrt (2 * n))) (Nat.succ (2 * n)) ⊆
    Finset.Ico (Nat.succ (Nat.sqrt (2 * n))) (Nat.succ (2 * n / 3)) ∪
      Finset.Ico (Nat.succ (2 * n / 3)) (Nat.succ (2 * n))
Tactic:
apply Finset.Ico_subset_Ico_union_Ico
State after:
no goals

State before:
case hs
n : ℕ
hn : 2 < n
⊢ Finset.Ico (Nat.succ (Nat.sqrt (2 * n))) (Nat.succ (2 * n)) ⊆
    Finset.Ico (Nat.succ (Nat.sqrt (2 * n))) (Nat.succ (2 * n / 3)) ∪ Finset.Ioc (2 * n / 3) (2 * n)
Tactic:
rw [← Nat.Ico_succ_succ]
State after:
case hs
n : ℕ
hn : 2 < n
⊢ Finset.Ico (Nat.succ (Nat.sqrt (2 * n))) (Nat.succ (2 * n)) ⊆
    Finset.Ico (Nat.succ (Nat.sqrt (2 * n))) (Nat.succ (2 * n / 3)) ∪
      Finset.Ico (Nat.succ (2 * n / 3)) (Nat.succ (2 * n))

State before:
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)
Tactic:
apply le_trans FactorizationCentralBinom.prodIocSqrtPowLeProdPrimes
State after:
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)

State before:
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)
Tactic:
apply le_trans _ (@prodPrimesLePowFour (2*n/3))
State after:
n : ℕ
hn : 2 < n
⊢ ∏ p in primes (Finset.Ioc (Nat.sqrt (2 * n)) (2 * n / 3)), p ≤ prodPrimes (2 * n / 3)

State before:
n : ℕ
hn : 2 < n
⊢ ∏ p in primes (Finset.Ioc (Nat.sqrt (2 * n)) (2 * n / 3)), p ≤ prodPrimes (2 * n / 3)
Tactic:
rw [prodPrimes, Finset.range_eq_Ico, Nat.Ico_succ_right]
State after:
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

State before:
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
Tactic:
apply Finset.prod_le_prod_of_subset_of_one_le' <;> rw [primes]
State after:
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

State before:
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
Tactic:
. apply Finset.monotone_filter_left
  exact Finset.Ioc_subset_Iic_self
State after:
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

State before:
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
Tactic:
. intro p hp _
  simp at hp
  replace hp := Nat.Prime.one_lt hp.right
  linarith
State after:
no goals

State before:
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))
Tactic:
apply Finset.monotone_filter_left
State after:
case h.a
n : ℕ
hn : 2 < n
⊢ Finset.Ioc (Nat.sqrt (2 * n)) (2 * n / 3) ≤ Finset.Icc 0 (2 * n / 3)

State before:
case h.a
n : ℕ
hn : 2 < n
⊢ Finset.Ioc (Nat.sqrt (2 * n)) (2 * n / 3) ≤ Finset.Icc 0 (2 * n / 3)
Tactic:
exact Finset.Ioc_subset_Iic_self
State after:
no goals

State before:
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
Tactic:
intro p hp _
State after:
case hf
n : ℕ
hn : 2 < n
p : ℕ
hp : p ∈ Finset.filter Nat.Prime (Finset.Icc 0 (2 * n / 3))
a✝ : ¬p ∈ Finset.filter Nat.Prime (Finset.Ioc (Nat.sqrt (2 * n)) (2 * n / 3))
⊢ 1 ≤ p

State before:
case hf
n : ℕ
hn : 2 < n
p : ℕ
hp : p ∈ Finset.filter Nat.Prime (Finset.Icc 0 (2 * n / 3))
a✝ : ¬p ∈ Finset.filter Nat.Prime (Finset.Ioc (Nat.sqrt (2 * n)) (2 * n / 3))
⊢ 1 ≤ p
Tactic:
simp at hp
State after:
case hf
n : ℕ
hn : 2 < n
p : ℕ
a✝ : ¬p ∈ Finset.filter Nat.Prime (Finset.Ioc (Nat.sqrt (2 * n)) (2 * n / 3))
hp : p ≤ 2 * n / 3 ∧ Nat.Prime p
⊢ 1 ≤ p

State before:
case hf
n : ℕ
hn : 2 < n
p : ℕ
a✝ : ¬p ∈ Finset.filter Nat.Prime (Finset.Ioc (Nat.sqrt (2 * n)) (2 * n / 3))
hp : p ≤ 2 * n / 3 ∧ Nat.Prime p
⊢ 1 ≤ p
Tactic:
replace hp := Nat.Prime.one_lt hp.right
State after:
case hf
n : ℕ
hn : 2 < n
p : ℕ
a✝ : ¬p ∈ Finset.filter Nat.Prime (Finset.Ioc (Nat.sqrt (2 * n)) (2 * n / 3))
hp : 1 < p
⊢ 1 ≤ p

State before:
case hf
n : ℕ
hn : 2 < n
p : ℕ
a✝ : ¬p ∈ Finset.filter Nat.Prime (Finset.Ioc (Nat.sqrt (2 * n)) (2 * n / 3))
hp : 1 < p
⊢ 1 ≤ p
Tactic:
linarith
State after:
no goals

State before:
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
Tactic:
conv => lhs; rw [← Finset.prod_Ioc_consecutive _ (mulDivLeSelf (by norm_num)) (by linarith : n ≤ 2*n)]
State after:
case h.h₂.h₂
n : ℕ
hn : 2 < n
⊢ (∏ i in Finset.Ioc (2 * n / 3) n, i ^ ↑(Nat.factorization (Nat.centralBinom n)) i) *
      ∏ i in Finset.Ioc n (2 * n), i ^ ↑(Nat.factorization (Nat.centralBinom n)) i ≤
    ∏ p in primes (Finset.Ioc n (2 * n)), p

State before:
case h.h₂.h₂
n : ℕ
hn : 2 < n
⊢ (∏ i in Finset.Ioc (2 * n / 3) n, i ^ ↑(Nat.factorization (Nat.centralBinom n)) i) *
      ∏ i in Finset.Ioc n (2 * n), i ^ ↑(Nat.factorization (Nat.centralBinom n)) i ≤
    ∏ p in primes (Finset.Ioc n (2 * n)), p
Tactic:
apply mulRightLeOfLeOne
State after:
case h.h₂.h₂.h1
n : ℕ
hn : 2 < n
⊢ ∏ i in Finset.Ioc (2 * n / 3) n, i ^ ↑(Nat.factorization (Nat.centralBinom n)) i ≤ 1

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

State before:
case h.h₂.h₂.h1
n : ℕ
hn : 2 < n
⊢ ∏ i in Finset.Ioc (2 * n / 3) n, i ^ ↑(Nat.factorization (Nat.centralBinom n)) i ≤ 1

case h.h₂.h₂.h
n : ℕ
hn : 2 < n
⊢ ∏ i in Finset.Ioc n (2 * n), i ^ ↑(Nat.factorization (Nat.centralBinom n)) i ≤ ∏ p in primes (Finset.Ioc n (2 * n)), p
Tactic:
. 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
State after:
case h.h₂.h₂.h
n : ℕ
hn : 2 < n
⊢ ∏ i in Finset.Ioc n (2 * n), i ^ ↑(Nat.factorization (Nat.centralBinom n)) i ≤ ∏ p in primes (Finset.Ioc n (2 * n)), p

State before:
case h.h₂.h₂.h
n : ℕ
hn : 2 < n
⊢ ∏ i in Finset.Ioc n (2 * n), i ^ ↑(Nat.factorization (Nat.centralBinom n)) i ≤ ∏ p in primes (Finset.Ioc n (2 * n)), p
Tactic:
. apply FactorizationCentralBinom.prodIocSqrtLePowLeProdPrimes
  exact sqrtTwoMulLeSelf (le_of_lt hn)
State after:
no goals

State before:
n : ℕ
hn : 2 < n
⊢ 2 ≤ 3
Tactic:
norm_num
State after:
no goals

State before:
n : ℕ
hn : 2 < n
⊢ n ≤ 2 * n
Tactic:
linarith
State after:
no goals

State before:
case h.h₂.h₂.h1
n : ℕ
hn : 2 < n
⊢ ∏ i in Finset.Ioc (2 * n / 3) n, i ^ ↑(Nat.factorization (Nat.centralBinom n)) i ≤ 1
Tactic:
apply le_of_eq
State after:
case h.h₂.h₂.h1.a
n : ℕ
hn : 2 < n
⊢ ∏ i in Finset.Ioc (2 * n / 3) n, i ^ ↑(Nat.factorization (Nat.centralBinom n)) i = 1

State before:
case h.h₂.h₂.h1.a
n : ℕ
hn : 2 < n
⊢ ∏ i in Finset.Ioc (2 * n / 3) n, i ^ ↑(Nat.factorization (Nat.centralBinom n)) i = 1
Tactic:
apply Finset.prod_eq_one
State after:
case h.h₂.h₂.h1.a.h
n : ℕ
hn : 2 < n
⊢ ∀ (x : ℕ), x ∈ Finset.Ioc (2 * n / 3) n → x ^ ↑(Nat.factorization (Nat.centralBinom n)) x = 1

State before:
case h.h₂.h₂.h1.a.h
n : ℕ
hn : 2 < n
⊢ ∀ (x : ℕ), x ∈ Finset.Ioc (2 * n / 3) n → x ^ ↑(Nat.factorization (Nat.centralBinom n)) x = 1
Tactic:
intro x hx
State after:
case h.h₂.h₂.h1.a.h
n : ℕ
hn : 2 < n
x : ℕ
hx : x ∈ Finset.Ioc (2 * n / 3) n
⊢ x ^ ↑(Nat.factorization (Nat.centralBinom n)) x = 1

State before:
case h.h₂.h₂.h1.a.h
n : ℕ
hn : 2 < n
x : ℕ
hx : x ∈ Finset.Ioc (2 * n / 3) n
⊢ x ^ ↑(Nat.factorization (Nat.centralBinom n)) x = 1
Tactic:
simp at hx
State after:
case h.h₂.h₂.h1.a.h
n : ℕ
hn : 2 < n
x : ℕ
hx : 2 * n / 3 < x ∧ x ≤ n
⊢ x ^ ↑(Nat.factorization (Nat.centralBinom n)) x = 1

State before:
case h.h₂.h₂.h1.a.h
n : ℕ
hn : 2 < n
x : ℕ
hx : 2 * n / 3 < x ∧ x ≤ n
⊢ x ^ ↑(Nat.factorization (Nat.centralBinom n)) x = 1
Tactic:
rw [Nat.factorization_centralBinom_of_two_mul_self_lt_three_mul hn hx.right]
State after:
case h.h₂.h₂.h1.a.h
n : ℕ
hn : 2 < n
x : ℕ
hx : 2 * n / 3 < x ∧ x ≤ n
⊢ x ^ 0 = 1

case h.h₂.h₂.h1.a.h
n : ℕ
hn : 2 < n
x : ℕ
hx : 2 * n / 3 < x ∧ x ≤ n
⊢ 2 * n < 3 * x

State before:
case h.h₂.h₂.h1.a.h
n : ℕ
hn : 2 < n
x : ℕ
hx : 2 * n / 3 < x ∧ x ≤ n
⊢ x ^ 0 = 1

case h.h₂.h₂.h1.a.h
n : ℕ
hn : 2 < n
x : ℕ
hx : 2 * n / 3 < x ∧ x ≤ n
⊢ 2 * n < 3 * x
Tactic:
. simp
State after:
case h.h₂.h₂.h1.a.h
n : ℕ
hn : 2 < n
x : ℕ
hx : 2 * n / 3 < x ∧ x ≤ n
⊢ 2 * n < 3 * x

State before:
case h.h₂.h₂.h1.a.h
n : ℕ
hn : 2 < n
x : ℕ
hx : 2 * n / 3 < x ∧ x ≤ n
⊢ 2 * n < 3 * x
Tactic:
. apply @Nat.lt_of_div_lt_div _ _ 3
  simp
  exact hx.left
State after:
no goals

State before:
case h.h₂.h₂.h1.a.h
n : ℕ
hn : 2 < n
x : ℕ
hx : 2 * n / 3 < x ∧ x ≤ n
⊢ x ^ 0 = 1
Tactic:
simp
State after:
no goals

State before:
case h.h₂.h₂.h1.a.h
n : ℕ
hn : 2 < n
x : ℕ
hx : 2 * n / 3 < x ∧ x ≤ n
⊢ 2 * n < 3 * x
Tactic:
apply @Nat.lt_of_div_lt_div _ _ 3
State after:
case h.h₂.h₂.h1.a.h
n : ℕ
hn : 2 < n
x : ℕ
hx : 2 * n / 3 < x ∧ x ≤ n
⊢ 2 * n / 3 < 3 * x / 3

State before:
case h.h₂.h₂.h1.a.h
n : ℕ
hn : 2 < n
x : ℕ
hx : 2 * n / 3 < x ∧ x ≤ n
⊢ 2 * n / 3 < 3 * x / 3
Tactic:
simp
State after:
case h.h₂.h₂.h1.a.h
n : ℕ
hn : 2 < n
x : ℕ
hx : 2 * n / 3 < x ∧ x ≤ n
⊢ 2 * n / 3 < x

State before:
case h.h₂.h₂.h1.a.h
n : ℕ
hn : 2 < n
x : ℕ
hx : 2 * n / 3 < x ∧ x ≤ n
⊢ 2 * n / 3 < x
Tactic:
exact hx.left
State after:
no goals

State before:
case h.h₂.h₂.h
n : ℕ
hn : 2 < n
⊢ ∏ i in Finset.Ioc n (2 * n), i ^ ↑(Nat.factorization (Nat.centralBinom n)) i ≤ ∏ p in primes (Finset.Ioc n (2 * n)), p
Tactic:
apply FactorizationCentralBinom.prodIocSqrtLePowLeProdPrimes
State after:
case h.h₂.h₂.h.ha
n : ℕ
hn : 2 < n
⊢ Nat.sqrt (2 * n) ≤ n

State before:
case h.h₂.h₂.h.ha
n : ℕ
hn : 2 < n
⊢ Nat.sqrt (2 * n) ≤ n
Tactic:
exact sqrtTwoMulLeSelf (le_of_lt hn)
State after:
no goals