internlm/Lean-Github huggingface dataset:
Theorem: FactorizationCentralBinom.prodIocSqrtLePowLeProdPrimes
Proof state before:
n a b : ℕ
ha : Nat.sqrt (2 * n) ≤ a
⊢ ∏ x in Finset.filter Nat.Prime (Finset.Ioc a b), x ^ ↑(Nat.factorization (Nat.centralBinom n)) x ≤
    ∏ p in Finset.filter Nat.Prime (Finset.Ioc a b), p
Tactic:
apply Finset.prod_le_prod'
Proof state after:
case h
n a b : ℕ
ha : Nat.sqrt (2 * n) ≤ a
⊢ ∀ (i : ℕ), i ∈ Finset.filter Nat.Prime (Finset.Ioc a b) → i ^ ↑(Nat.factorization (Nat.centralBinom n)) i ≤ i
Theorem: FactorizationCentralBinom.prodIocSqrtLePowLeProdPrimes
Proof state before:
case h
n a b : ℕ
ha : Nat.sqrt (2 * n) ≤ a
⊢ ∀ (i : ℕ), i ∈ Finset.filter Nat.Prime (Finset.Ioc a b) → i ^ ↑(Nat.factorization (Nat.centralBinom n)) i ≤ i
Tactic:
simp
Proof state after:
case h
n a b : ℕ
ha : Nat.sqrt (2 * n) ≤ a
⊢ ∀ (i : ℕ), a < i → i ≤ b → Nat.Prime i → i ^ ↑(Nat.factorization (Nat.centralBinom n)) i ≤ i
Theorem: FactorizationCentralBinom.prodIocSqrtLePowLeProdPrimes
Proof state before:
case h
n a b : ℕ
ha : Nat.sqrt (2 * n) ≤ a
⊢ ∀ (i : ℕ), a < i → i ≤ b → Nat.Prime i → i ^ ↑(Nat.factorization (Nat.centralBinom n)) i ≤ i
Tactic:
intro p hbp _ hp
Proof state after:
case h
n a b : ℕ
ha : Nat.sqrt (2 * n) ≤ a
p : ℕ
hbp : a < p
a✝ : p ≤ b
hp : Nat.Prime p
⊢ p ^ ↑(Nat.factorization (Nat.centralBinom n)) p ≤ p
Theorem: FactorizationCentralBinom.prodIocSqrtLePowLeProdPrimes
Proof state before:
case h
n a b : ℕ
ha : Nat.sqrt (2 * n) ≤ a
p : ℕ
hbp : a < p
a✝ : p ≤ b
hp : Nat.Prime p
⊢ p ^ ↑(Nat.factorization (Nat.centralBinom n)) p ≤ p
Tactic:
replace hbp := lt_of_le_of_lt ha hbp
Proof state after:
case h
n a b : ℕ
ha : Nat.sqrt (2 * n) ≤ a
p : ℕ
a✝ : p ≤ b
hp : Nat.Prime p
hbp : Nat.sqrt (2 * n) < p
⊢ p ^ ↑(Nat.factorization (Nat.centralBinom n)) p ≤ p
Theorem: FactorizationCentralBinom.prodIocSqrtLePowLeProdPrimes
Proof state before:
case h
n a b : ℕ
ha : Nat.sqrt (2 * n) ≤ a
p : ℕ
a✝ : p ≤ b
hp : Nat.Prime p
hbp : Nat.sqrt (2 * n) < p
⊢ p ^ ↑(Nat.factorization (Nat.centralBinom n)) p ≤ p
Tactic:
conv => rhs; rw [← Nat.pow_one p]
Proof state after:
case h
n a b : ℕ
ha : Nat.sqrt (2 * n) ≤ a
p : ℕ
a✝ : p ≤ b
hp : Nat.Prime p
hbp : Nat.sqrt (2 * n) < p
⊢ p ^ ↑(Nat.factorization (Nat.centralBinom n)) p ≤ p ^ 1
Theorem: FactorizationCentralBinom.prodIocSqrtLePowLeProdPrimes
Proof state before:
case h
n a b : ℕ
ha : Nat.sqrt (2 * n) ≤ a
p : ℕ
a✝ : p ≤ b
hp : Nat.Prime p
hbp : Nat.sqrt (2 * n) < p
⊢ p ^ ↑(Nat.factorization (Nat.centralBinom n)) p ≤ p ^ 1
Tactic:
rw [pow_le_pow_iff (Nat.Prime.one_lt hp)]
Proof state after:
case h
n a b : ℕ
ha : Nat.sqrt (2 * n) ≤ a
p : ℕ
a✝ : p ≤ b
hp : Nat.Prime p
hbp : Nat.sqrt (2 * n) < p
⊢ ↑(Nat.factorization (Nat.centralBinom n)) p ≤ 1
Theorem: FactorizationCentralBinom.prodIocSqrtLePowLeProdPrimes
Proof state before:
case h
n a b : ℕ
ha : Nat.sqrt (2 * n) ≤ a
p : ℕ
a✝ : p ≤ b
hp : Nat.Prime p
hbp : Nat.sqrt (2 * n) < p
⊢ ↑(Nat.factorization (Nat.centralBinom n)) p ≤ 1
Tactic:
rw [Nat.sqrt_lt'] at hbp
Proof state after:
case h
n a b : ℕ
ha : Nat.sqrt (2 * n) ≤ a
p : ℕ
a✝ : p ≤ b
hp : Nat.Prime p
hbp : 2 * n < p ^ 2
⊢ ↑(Nat.factorization (Nat.centralBinom n)) p ≤ 1
Theorem: FactorizationCentralBinom.prodIocSqrtLePowLeProdPrimes
Proof state before:
case h
n a b : ℕ
ha : Nat.sqrt (2 * n) ≤ a
p : ℕ
a✝ : p ≤ b
hp : Nat.Prime p
hbp : 2 * n < p ^ 2
⊢ ↑(Nat.factorization (Nat.centralBinom n)) p ≤ 1
Tactic:
exact leOne hp hbp
Proof state after:
no goals
Theorem: FactorizationCentralBinom.prodIocSqrtLePowLeProdPrimes
Proof state before:
case hp
n a b : ℕ
ha : Nat.sqrt (2 * n) ≤ a
⊢ ∀ (x : ℕ), x ∈ Finset.Ioc a b → x ^ ↑(Nat.factorization (Nat.centralBinom n)) x ≠ 1 → Nat.Prime x
Tactic:
intro p _
Proof state after:
case hp
n a b : ℕ
ha : Nat.sqrt (2 * n) ≤ a
p : ℕ
a✝ : p ∈ Finset.Ioc a b
⊢ p ^ ↑(Nat.factorization (Nat.centralBinom n)) p ≠ 1 → Nat.Prime p
Theorem: FactorizationCentralBinom.prodIocSqrtLePowLeProdPrimes
Proof state before:
case hp
n a b : ℕ
ha : Nat.sqrt (2 * n) ≤ a
p : ℕ
a✝ : p ∈ Finset.Ioc a b
⊢ p ^ ↑(Nat.factorization (Nat.centralBinom n)) p ≠ 1 → Nat.Prime p
Tactic:
apply primeOfPowFactorizationNeOne
Proof state after:
no goals
Theorem: sqrtTwoMulLeSelf
Proof state before:
n : ℕ
hn : 2 ≤ n
⊢ Nat.sqrt (2 * n) ≤ n
Tactic:
conv => rhs; rw [← Nat.sqrt_eq n]
Proof state after:
n : ℕ
hn : 2 ≤ n
⊢ Nat.sqrt (2 * n) ≤ Nat.sqrt (n * n)
Theorem: sqrtTwoMulLeSelf
Proof state before:
n : ℕ
hn : 2 ≤ n
⊢ Nat.sqrt (2 * n) ≤ Nat.sqrt (n * n)
Tactic:
apply Nat.sqrt_le_sqrt
Proof state after:
case h
n : ℕ
hn : 2 ≤ n
⊢ 2 * n ≤ n * n
Theorem: sqrtTwoMulLeSelf
Proof state before:
case h
n : ℕ
hn : 2 ≤ n
⊢ 2 * n ≤ n * n
Tactic:
exact Nat.mul_le_mul_right _ hn
Proof state after:
no goals
Theorem: prodRangePowFactorization
Proof state before:
b n : ℕ
⊢ ∏ p in Finset.range b, p ^ ↑(Nat.factorization n) p = ∏ p in Finset.Ico 1 b, p ^ ↑(Nat.factorization n) p
Tactic:
cases b with
| zero => simp
| succ b =>
  rw [← Finset.prod_range_mul_prod_Ico _ (Nat.zero_lt_succ _)]
  simp
Proof state after:
no goals
Theorem: prodRangePowFactorization
Proof state before:
case zero
n : ℕ
⊢ ∏ p in Finset.range Nat.zero, p ^ ↑(Nat.factorization n) p =
    ∏ p in Finset.Ico 1 Nat.zero, p ^ ↑(Nat.factorization n) p
Tactic:
simp
Proof state after:
no goals
Theorem: prodRangePowFactorization
Proof state before:
case succ
n b : ℕ
⊢ ∏ p in Finset.range (Nat.succ b), p ^ ↑(Nat.factorization n) p =
    ∏ p in Finset.Ico 1 (Nat.succ b), p ^ ↑(Nat.factorization n) p
Tactic:
rw [← Finset.prod_range_mul_prod_Ico _ (Nat.zero_lt_succ _)]
Proof state after:
case succ
n b : ℕ
⊢ (∏ k in Finset.range (Nat.succ 0), k ^ ↑(Nat.factorization n) k) *
      ∏ k in Finset.Ico (Nat.succ 0) (Nat.succ b), k ^ ↑(Nat.factorization n) k =
    ∏ p in Finset.Ico 1 (Nat.succ b), p ^ ↑(Nat.factorization n) p
Theorem: prodRangePowFactorization
Proof state before:
case succ
n b : ℕ
⊢ (∏ k in Finset.range (Nat.succ 0), k ^ ↑(Nat.factorization n) k) *
      ∏ k in Finset.Ico (Nat.succ 0) (Nat.succ b), k ^ ↑(Nat.factorization n) k =
    ∏ p in Finset.Ico 1 (Nat.succ b), p ^ ↑(Nat.factorization n) p
Tactic:
simp
Proof state after:
no goals
Theorem: powFactorizationPos
Proof state before:
n p : ℕ
⊢ 0 < p ^ ↑(Nat.factorization n) p
Tactic:
cases p with
| zero => simp
| succ p => exact Nat.one_le_pow _ _ (Nat.zero_lt_succ _)
Proof state after:
no goals
Theorem: powFactorizationPos
Proof state before:
case zero
n : ℕ
⊢ 0 < Nat.zero ^ ↑(Nat.factorization n) Nat.zero
Tactic:
simp
Proof state after:
no goals
Theorem: powFactorizationPos
Proof state before:
case succ
n p : ℕ
⊢ 0 < Nat.succ p ^ ↑(Nat.factorization n) (Nat.succ p)
Tactic:
exact Nat.one_le_pow _ _ (Nat.zero_lt_succ _)
Proof state after:
no goals
Theorem: prodLeProdMulProdOfUnionOfOneLe
Proof state before:
s t₁ t₂ : Finset ℕ
f : ℕ → ℕ
hs : s ⊆ t₁ ∪ t₂
hf : ∀ (y : ℕ), 1 ≤ f y
⊢ ∏ x in s, f x ≤ (∏ x in t₁, f x) * ∏ x in t₂, f x
Tactic:
rw [← Finset.prod_union_inter]
Proof state after:
s t₁ t₂ : Finset ℕ
f : ℕ → ℕ
hs : s ⊆ t₁ ∪ t₂
hf : ∀ (y : ℕ), 1 ≤ f y
⊢ ∏ x in s, f x ≤ (∏ x in t₁ ∪ t₂, f x) * ∏ x in t₁ ∩ t₂, f x
Theorem: prodLeProdMulProdOfUnionOfOneLe
Proof state before:
s t₁ t₂ : Finset ℕ
f : ℕ → ℕ
hs : s ⊆ t₁ ∪ t₂
hf : ∀ (y : ℕ), 1 ≤ f y
⊢ ∏ x in s, f x ≤ (∏ x in t₁ ∪ t₂, f x) * ∏ x in t₁ ∩ t₂, f x
Tactic:
apply le_trans _ (Nat.le_mul_of_pos_right _)
Proof state after:
s t₁ t₂ : Finset ℕ
f : ℕ → ℕ
hs : s ⊆ t₁ ∪ t₂
hf : ∀ (y : ℕ), 1 ≤ f y
⊢ ∏ x in s, f x ≤ ∏ x in t₁ ∪ t₂, f x

s t₁ t₂ : Finset ℕ
f : ℕ → ℕ
hs : s ⊆ t₁ ∪ t₂
hf : ∀ (y : ℕ), 1 ≤ f y
⊢ 0 < ∏ x in t₁ ∩ t₂, f x
Theorem: prodLeProdMulProdOfUnionOfOneLe
Proof state before:
s t₁ t₂ : Finset ℕ
f : ℕ → ℕ
hs : s ⊆ t₁ ∪ t₂
hf : ∀ (y : ℕ), 1 ≤ f y
⊢ ∏ x in s, f x ≤ ∏ x in t₁ ∪ t₂, f x

s t₁ t₂ : Finset ℕ
f : ℕ → ℕ
hs : s ⊆ t₁ ∪ t₂
hf : ∀ (y : ℕ), 1 ≤ f y
⊢ 0 < ∏ x in t₁ ∩ t₂, f x
Tactic:
. exact Finset.prod_mono_set_of_one_le' hf hs
Proof state after:
s t₁ t₂ : Finset ℕ
f : ℕ → ℕ
hs : s ⊆ t₁ ∪ t₂
hf : ∀ (y : ℕ), 1 ≤ f y
⊢ 0 < ∏ x in t₁ ∩ t₂, f x
Theorem: prodLeProdMulProdOfUnionOfOneLe
Proof state before:
s t₁ t₂ : Finset ℕ
f : ℕ → ℕ
hs : s ⊆ t₁ ∪ t₂
hf : ∀ (y : ℕ), 1 ≤ f y
⊢ 0 < ∏ x in t₁ ∩ t₂, f x
Tactic:
. apply Finset.prod_pos
  intro x _
  apply hf
Proof state after:
no goals
Theorem: prodLeProdMulProdOfUnionOfOneLe
Proof state before:
s t₁ t₂ : Finset ℕ
f : ℕ → ℕ
hs : s ⊆ t₁ ∪ t₂
hf : ∀ (y : ℕ), 1 ≤ f y
⊢ ∏ x in s, f x ≤ ∏ x in t₁ ∪ t₂, f x
Tactic:
exact Finset.prod_mono_set_of_one_le' hf hs
Proof state after:
no goals
Theorem: prodLeProdMulProdOfUnionOfOneLe
Proof state before:
s t₁ t₂ : Finset ℕ
f : ℕ → ℕ
hs : s ⊆ t₁ ∪ t₂
hf : ∀ (y : ℕ), 1 ≤ f y
⊢ 0 < ∏ x in t₁ ∩ t₂, f x
Tactic:
apply Finset.prod_pos
Proof state after:
case h0
s t₁ t₂ : Finset ℕ
f : ℕ → ℕ
hs : s ⊆ t₁ ∪ t₂
hf : ∀ (y : ℕ), 1 ≤ f y
⊢ ∀ (i : ℕ), i ∈ t₁ ∩ t₂ → 0 < f i
Theorem: prodLeProdMulProdOfUnionOfOneLe
Proof state before:
case h0
s t₁ t₂ : Finset ℕ
f : ℕ → ℕ
hs : s ⊆ t₁ ∪ t₂
hf : ∀ (y : ℕ), 1 ≤ f y
⊢ ∀ (i : ℕ), i ∈ t₁ ∩ t₂ → 0 < f i
Tactic:
intro x _
Proof state after:
case h0
s t₁ t₂ : Finset ℕ
f : ℕ → ℕ
hs : s ⊆ t₁ ∪ t₂
hf : ∀ (y : ℕ), 1 ≤ f y
x : ℕ
a✝ : x ∈ t₁ ∩ t₂
⊢ 0 < f x
Theorem: prodLeProdMulProdOfUnionOfOneLe
Proof state before:
case h0
s t₁ t₂ : Finset ℕ
f : ℕ → ℕ
hs : s ⊆ t₁ ∪ t₂
hf : ∀ (y : ℕ), 1 ≤ f y
x : ℕ
a✝ : x ∈ t₁ ∩ t₂
⊢ 0 < f x
Tactic:
apply hf
Proof state after:
no goals
Theorem: mulDivLeSelf
Proof state before:
n a b : ℕ
hab : a ≤ b
⊢ a * n / b ≤ n
Tactic:
cases b with
| zero => simp
| succ b =>
  conv => rhs; rw [← Nat.mul_div_right n (Nat.zero_lt_succ b)]
  apply Nat.div_le_div_right
  exact Nat.mul_le_mul_right _ hab
Proof state after:
no goals
Theorem: mulDivLeSelf
Proof state before:
case zero
n a : ℕ
hab : a ≤ Nat.zero
⊢ a * n / Nat.zero ≤ n
Tactic:
simp
Proof state after:
no goals
Theorem: mulDivLeSelf
Proof state before:
case succ
n a b : ℕ
hab : a ≤ Nat.succ b
⊢ a * n / Nat.succ b ≤ n
Tactic:
conv => rhs; rw [← Nat.mul_div_right n (Nat.zero_lt_succ b)]
Proof state after:
case succ
n a b : ℕ
hab : a ≤ Nat.succ b
⊢ a * n / Nat.succ b ≤ Nat.succ b * n / Nat.succ b
Theorem: mulDivLeSelf
Proof state before:
case succ
n a b : ℕ
hab : a ≤ Nat.succ b
⊢ a * n / Nat.succ b ≤ Nat.succ b * n / Nat.succ b
Tactic:
apply Nat.div_le_div_right
Proof state after:
case succ.h
n a b : ℕ
hab : a ≤ Nat.succ b
⊢ a * n ≤ Nat.succ b * n
Theorem: mulDivLeSelf
Proof state before:
case succ.h
n a b : ℕ
hab : a ≤ Nat.succ b
⊢ a * n ≤ Nat.succ b * n
Tactic:
exact Nat.mul_le_mul_right _ hab
Proof state after:
no goals
Theorem: mulRightLeOfLeOne
Proof state before:
x y z : ℕ
h1 : x ≤ 1
h : y ≤ z
⊢ x * y ≤ z
Tactic:
rw [← Nat.one_mul z]
Proof state after:
x y z : ℕ
h1 : x ≤ 1
h : y ≤ z
⊢ x * y ≤ 1 * z
Theorem: mulRightLeOfLeOne
Proof state before:
x y z : ℕ
h1 : x ≤ 1
h : y ≤ z
⊢ x * y ≤ 1 * z
Tactic:
apply Nat.mul_le_mul h1 h
Proof state after:
no goals
Theorem: mulLeftLeOfLeOne
Proof state before:
x y z : ℕ
h1 : y ≤ 1
h : x ≤ z
⊢ x * y ≤ z
Tactic:
rw [← Nat.mul_one z]
Proof state after:
x y z : ℕ
h1 : y ≤ 1
h : x ≤ z
⊢ x * y ≤ z * 1
Theorem: mulLeftLeOfLeOne
Proof state before:
x y z : ℕ
h1 : y ≤ 1
h : x ≤ z
⊢ x * y ≤ z * 1
Tactic:
apply Nat.mul_le_mul h h1
Proof state after:
no goals
Theorem: fourPowLeMulProdPrimes
Proof 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))
Proof 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
Theorem: fourPowLeMulProdPrimes
Proof 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]
Proof 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
Theorem: fourPowLeMulProdPrimes
Proof 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
Proof 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
Theorem: fourPowLeMulProdPrimes
Proof 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]
Proof 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)
Theorem: fourPowLeMulProdPrimes
Proof 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
Proof 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)
Theorem: fourPowLeMulProdPrimes
Proof 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
Proof 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
Theorem: fourPowLeMulProdPrimes
Proof 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]
Proof 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
Theorem: fourPowLeMulProdPrimes
Proof 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]
Proof 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
Theorem: fourPowLeMulProdPrimes
Proof 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 _))]
Proof 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
Theorem: fourPowLeMulProdPrimes
Proof 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]
Proof 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
Theorem: fourPowLeMulProdPrimes
Proof 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]
Proof 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)
Theorem: fourPowLeMulProdPrimes
Proof 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
Proof 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
Theorem: fourPowLeMulProdPrimes
Proof 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
Proof 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
Theorem: fourPowLeMulProdPrimes
Proof 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)
Proof state after:
no goals
Theorem: fourPowLeMulProdPrimes
Proof state before:
n : ℕ
hn : 2 < n
⊢ 0 < n
Tactic:
linarith
Proof state after:
no goals
Theorem: fourPowLeMulProdPrimes
Proof state before:
n : ℕ
hn : 2 < n
⊢ ∀ {x y z : ℕ}, x * (2 * n) * y * z = 2 * n * (x * y * z)
Tactic:
intro x y z
Proof state after:
n : ℕ
hn : 2 < n
x y z : ℕ
⊢ x * (2 * n) * y * z = 2 * n * (x * y * z)
Theorem: fourPowLeMulProdPrimes
Proof state before:
n : ℕ
hn : 2 < n
x y z : ℕ
⊢ x * (2 * n) * y * z = 2 * n * (x * y * z)
Tactic:
linarith
Proof state after:
no goals
Theorem: fourPowLeMulProdPrimes
Proof 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)]
Proof 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)
Theorem: fourPowLeMulProdPrimes
Proof 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' _)
Proof 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))) = ∅
Theorem: fourPowLeMulProdPrimes
Proof 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
Proof state after:
n : ℕ
hn : 2 < n
⊢ n = 0 → Finset.Ico 1 (Nat.succ (Nat.sqrt (2 * n))) = ∅
Theorem: fourPowLeMulProdPrimes
Proof state before:
n : ℕ
hn : 2 < n
⊢ n = 0 → Finset.Ico 1 (Nat.succ (Nat.sqrt (2 * n))) = ∅
Tactic:
. intro hn; rw [hn]; norm_num
Proof state after:
no goals
Theorem: fourPowLeMulProdPrimes
Proof 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
Proof state after:
no goals
Theorem: fourPowLeMulProdPrimes
Proof state before:
n : ℕ
hn : 2 < n
⊢ n = 0 → Finset.Ico 1 (Nat.succ (Nat.sqrt (2 * n))) = ∅
Tactic:
intro hn
Proof state after:
n : ℕ
hn✝ : 2 < n
hn : n = 0
⊢ Finset.Ico 1 (Nat.succ (Nat.sqrt (2 * n))) = ∅
Theorem: fourPowLeMulProdPrimes
Proof state before:
n : ℕ
hn✝ : 2 < n
hn : n = 0
⊢ Finset.Ico 1 (Nat.succ (Nat.sqrt (2 * n))) = ∅
Tactic:
rw [hn]
Proof state after:
n : ℕ
hn✝ : 2 < n
hn : n = 0
⊢ Finset.Ico 1 (Nat.succ (Nat.sqrt (2 * 0))) = ∅
Theorem: fourPowLeMulProdPrimes
Proof state before:
n : ℕ
hn✝ : 2 < n
hn : n = 0
⊢ Finset.Ico 1 (Nat.succ (Nat.sqrt (2 * 0))) = ∅
Tactic:
norm_num
Proof state after:
no goals
Theorem: fourPowLeMulProdPrimes
Proof 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)
Proof 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