internlm/Lean-Github huggingface dataset:
Theorem: fourPowLeMulProdPrimes
Proof 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
Proof 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
Theorem: fourPowLeMulProdPrimes
Proof 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 _))
Proof 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
Theorem: fourPowLeMulProdPrimes
Proof 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
Proof 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
Theorem: fourPowLeMulProdPrimes
Proof 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
Proof 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
Theorem: fourPowLeMulProdPrimes
Proof 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
Proof 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
Theorem: fourPowLeMulProdPrimes
Proof 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)
Proof state after:
no goals
Theorem: fourPowLeMulProdPrimes
Proof 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]
Proof 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))
Theorem: fourPowLeMulProdPrimes
Proof 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
Proof state after:
no goals
Theorem: fourPowLeMulProdPrimes
Proof 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]
Proof 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))
Theorem: fourPowLeMulProdPrimes
Proof 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
Proof 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)
Theorem: fourPowLeMulProdPrimes
Proof 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))
Proof state after:
n : ℕ
hn : 2 < n
⊢ ∏ p in primes (Finset.Ioc (Nat.sqrt (2 * n)) (2 * n / 3)), p ≤ prodPrimes (2 * n / 3)
Theorem: fourPowLeMulProdPrimes
Proof 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]
Proof 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
Theorem: fourPowLeMulProdPrimes
Proof 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]
Proof 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
Theorem: fourPowLeMulProdPrimes
Proof 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
Proof 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
Theorem: fourPowLeMulProdPrimes
Proof 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
Proof state after:
no goals
Theorem: fourPowLeMulProdPrimes
Proof 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
Proof state after:
case h.a
n : ℕ
hn : 2 < n
⊢ Finset.Ioc (Nat.sqrt (2 * n)) (2 * n / 3) ≤ Finset.Icc 0 (2 * n / 3)
Theorem: fourPowLeMulProdPrimes
Proof 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
Proof state after:
no goals
Theorem: fourPowLeMulProdPrimes
Proof 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 _
Proof 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
Theorem: fourPowLeMulProdPrimes
Proof 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
Proof 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
Theorem: fourPowLeMulProdPrimes
Proof 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
Proof 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
Theorem: fourPowLeMulProdPrimes
Proof 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
Proof state after:
no goals
Theorem: fourPowLeMulProdPrimes
Proof 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)]
Proof 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
Theorem: fourPowLeMulProdPrimes
Proof 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
Proof 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
Theorem: fourPowLeMulProdPrimes
Proof 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
Proof 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
Theorem: fourPowLeMulProdPrimes
Proof 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)
Proof state after:
no goals
Theorem: fourPowLeMulProdPrimes
Proof state before:
n : ℕ
hn : 2 < n
⊢ 2 ≤ 3
Tactic:
norm_num
Proof state after:
no goals
Theorem: fourPowLeMulProdPrimes
Proof state before:
n : ℕ
hn : 2 < n
⊢ n ≤ 2 * n
Tactic:
linarith
Proof state after:
no goals
Theorem: fourPowLeMulProdPrimes
Proof 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
Proof 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
Theorem: fourPowLeMulProdPrimes
Proof 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
Proof 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
Theorem: fourPowLeMulProdPrimes
Proof 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
Proof 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
Theorem: fourPowLeMulProdPrimes
Proof 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
Proof 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
Theorem: fourPowLeMulProdPrimes
Proof 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]
Proof 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
Theorem: fourPowLeMulProdPrimes
Proof 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
Proof 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
Theorem: fourPowLeMulProdPrimes
Proof 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
Proof state after:
no goals
Theorem: fourPowLeMulProdPrimes
Proof 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
Proof state after:
no goals
Theorem: fourPowLeMulProdPrimes
Proof 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
Proof 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
Theorem: fourPowLeMulProdPrimes
Proof 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
Proof 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
Theorem: fourPowLeMulProdPrimes
Proof 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
Proof state after:
no goals
Theorem: fourPowLeMulProdPrimes
Proof 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
Proof state after:
case h.h₂.h₂.h.ha
n : ℕ
hn : 2 < n
⊢ Nat.sqrt (2 * n) ≤ n
Theorem: fourPowLeMulProdPrimes
Proof state before:
case h.h₂.h₂.h.ha
n : ℕ
hn : 2 < n
⊢ Nat.sqrt (2 * n) ≤ n
Tactic:
exact sqrtTwoMulLeSelf (le_of_lt hn)
Proof state after:
no goals
Theorem: generic_recursor
Proof state before:
motive : ↑N0 → Prop
hz : motive z
hs : ∀ (n : ↑N0), motive n → motive (S n)
x : ↑N0
⊢ motive x
Tactic:
let A := {x : N0 | motive x}
Proof state after:
motive : ↑N0 → Prop
hz : motive z
hs : ∀ (n : ↑N0), motive n → motive (S n)
x : ↑N0
A : Set ↑N0 := {x | motive x}
⊢ motive x
Theorem: generic_recursor
Proof state before:
motive : ↑N0 → Prop
hz : motive z
hs : ∀ (n : ↑N0), motive n → motive (S n)
x : ↑N0
A : Set ↑N0 := {x | motive x}
⊢ motive x
Tactic:
have hzmem : z ∈ A := by
  simp only [Set.mem_setOf_eq]
  exact hz
Proof state after:
motive : ↑N0 → Prop
hz : motive z
hs : ∀ (n : ↑N0), motive n → motive (S n)
x : ↑N0
A : Set ↑N0 := {x | motive x}
hzmem : z ∈ A
⊢ motive x
Theorem: generic_recursor
Proof state before:
motive : ↑N0 → Prop
hz : motive z
hs : ∀ (n : ↑N0), motive n → motive (S n)
x : ↑N0
A : Set ↑N0 := {x | motive x}
hzmem : z ∈ A
⊢ motive x
Tactic:
have hind : (∀ n : N0, n ∈ A → (S n) ∈ A) := by
  intros n hel
  simp only [Set.mem_setOf_eq]
  simp only [Set.mem_setOf_eq] at hel
  specialize hs n
  exact hs hel
Proof state after:
motive : ↑N0 → Prop
hz : motive z
hs : ∀ (n : ↑N0), motive n → motive (S n)
x : ↑N0
A : Set ↑N0 := {x | motive x}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
⊢ motive x
Theorem: generic_recursor
Proof state before:
motive : ↑N0 → Prop
hz : motive z
hs : ∀ (n : ↑N0), motive n → motive (S n)
x : ↑N0
A : Set ↑N0 := {x | motive x}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
⊢ motive x
Tactic:
have heq := p3 A ⟨hzmem, hind⟩
Proof state after:
motive : ↑N0 → Prop
hz : motive z
hs : ∀ (n : ↑N0), motive n → motive (S n)
x : ↑N0
A : Set ↑N0 := {x | motive x}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq : Subtype.val '' A = N0
⊢ motive x
Theorem: generic_recursor
Proof state before:
motive : ↑N0 → Prop
hz : motive z
hs : ∀ (n : ↑N0), motive n → motive (S n)
x : ↑N0
A : Set ↑N0 := {x | motive x}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq : Subtype.val '' A = N0
⊢ motive x
Tactic:
simp [A, Set.ext_iff] at heq
Proof state after:
motive : ↑N0 → Prop
hz : motive z
hs : ∀ (n : ↑N0), motive n → motive (S n)
x : ↑N0
A : Set ↑N0 := {x | motive x}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq : ∀ (x : α), (∃ (x_1 : x ∈ N0), motive { val := x, property := (_ : x ∈ N0) }) ↔ x ∈ N0
⊢ motive x
Theorem: generic_recursor
Proof state before:
motive : ↑N0 → Prop
hz : motive z
hs : ∀ (n : ↑N0), motive n → motive (S n)
x : ↑N0
A : Set ↑N0 := {x | motive x}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq : ∀ (x : α), (∃ (x_1 : x ∈ N0), motive { val := x, property := (_ : x ∈ N0) }) ↔ x ∈ N0
⊢ motive x
Tactic:
specialize heq x
Proof state after:
motive : ↑N0 → Prop
hz : motive z
hs : ∀ (n : ↑N0), motive n → motive (S n)
x : ↑N0
A : Set ↑N0 := {x | motive x}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq : (∃ (x_1 : ↑x ∈ N0), motive { val := ↑x, property := (_ : ↑x ∈ N0) }) ↔ ↑x ∈ N0
⊢ motive x
Theorem: generic_recursor
Proof state before:
motive : ↑N0 → Prop
hz : motive z
hs : ∀ (n : ↑N0), motive n → motive (S n)
x : ↑N0
A : Set ↑N0 := {x | motive x}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq : (∃ (x_1 : ↑x ∈ N0), motive { val := ↑x, property := (_ : ↑x ∈ N0) }) ↔ ↑x ∈ N0
⊢ motive x
Tactic:
simp only [Subtype.coe_eta, Subtype.coe_prop, exists_const, iff_true] at heq
Proof state after:
motive : ↑N0 → Prop
hz : motive z
hs : ∀ (n : ↑N0), motive n → motive (S n)
x : ↑N0
A : Set ↑N0 := {x | motive x}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq : motive x
⊢ motive x
Theorem: generic_recursor
Proof state before:
motive : ↑N0 → Prop
hz : motive z
hs : ∀ (n : ↑N0), motive n → motive (S n)
x : ↑N0
A : Set ↑N0 := {x | motive x}
hzmem : z ∈ A
hind : ∀ n ∈ A, S n ∈ A
heq : motive x
⊢ motive x
Tactic:
exact heq
Proof state after:
no goals
Theorem: generic_recursor
Proof state before:
motive : ↑N0 → Prop
hz : motive z
hs : ∀ (n : ↑N0), motive n → motive (S n)
x : ↑N0
A : Set ↑N0 := {x | motive x}
⊢ z ∈ A
Tactic:
simp only [Set.mem_setOf_eq]
Proof state after:
motive : ↑N0 → Prop
hz : motive z
hs : ∀ (n : ↑N0), motive n → motive (S n)
x : ↑N0
A : Set ↑N0 := {x | motive x}
⊢ motive z
Theorem: generic_recursor
Proof state before:
motive : ↑N0 → Prop
hz : motive z
hs : ∀ (n : ↑N0), motive n → motive (S n)
x : ↑N0
A : Set ↑N0 := {x | motive x}
⊢ motive z
Tactic:
exact hz
Proof state after:
no goals
Theorem: generic_recursor
Proof state before:
motive : ↑N0 → Prop
hz : motive z
hs : ∀ (n : ↑N0), motive n → motive (S n)
x : ↑N0
A : Set ↑N0 := {x | motive x}
hzmem : z ∈ A
⊢ ∀ n ∈ A, S n ∈ A
Tactic:
intros n hel
Proof state after:
motive : ↑N0 → Prop
hz : motive z
hs : ∀ (n : ↑N0), motive n → motive (S n)
x : ↑N0
A : Set ↑N0 := {x | motive x}
hzmem : z ∈ A
n : ↑N0
hel : n ∈ A
⊢ S n ∈ A
Theorem: generic_recursor
Proof state before:
motive : ↑N0 → Prop
hz : motive z
hs : ∀ (n : ↑N0), motive n → motive (S n)
x : ↑N0
A : Set ↑N0 := {x | motive x}
hzmem : z ∈ A
n : ↑N0
hel : n ∈ A
⊢ S n ∈ A
Tactic:
simp only [Set.mem_setOf_eq]
Proof state after:
motive : ↑N0 → Prop
hz : motive z
hs : ∀ (n : ↑N0), motive n → motive (S n)
x : ↑N0
A : Set ↑N0 := {x | motive x}
hzmem : z ∈ A
n : ↑N0
hel : n ∈ A
⊢ motive (S n)
Theorem: generic_recursor
Proof state before:
motive : ↑N0 → Prop
hz : motive z
hs : ∀ (n : ↑N0), motive n → motive (S n)
x : ↑N0
A : Set ↑N0 := {x | motive x}
hzmem : z ∈ A
n : ↑N0
hel : n ∈ A
⊢ motive (S n)
Tactic:
simp only [Set.mem_setOf_eq] at hel
Proof state after:
motive : ↑N0 → Prop
hz : motive z
hs : ∀ (n : ↑N0), motive n → motive (S n)
x : ↑N0
A : Set ↑N0 := {x | motive x}
hzmem : z ∈ A
n : ↑N0
hel : motive n
⊢ motive (S n)
Theorem: generic_recursor
Proof state before:
motive : ↑N0 → Prop
hz : motive z
hs : ∀ (n : ↑N0), motive n → motive (S n)
x : ↑N0
A : Set ↑N0 := {x | motive x}
hzmem : z ∈ A
n : ↑N0
hel : motive n
⊢ motive (S n)
Tactic:
specialize hs n
Proof state after:
motive : ↑N0 → Prop
hz : motive z
x : ↑N0
A : Set ↑N0 := {x | motive x}
hzmem : z ∈ A
n : ↑N0
hel : motive n
hs : motive n → motive (S n)
⊢ motive (S n)
Theorem: generic_recursor
Proof state before:
motive : ↑N0 → Prop
hz : motive z
x : ↑N0
A : Set ↑N0 := {x | motive x}
hzmem : z ∈ A
n : ↑N0
hel : motive n
hs : motive n → motive (S n)
⊢ motive (S n)
Tactic:
exact hs hel
Proof state after:
no goals
Theorem: zero_plus_x_eq_eq
Proof state before:
⊢ ∀ (x : ↑N0), plus (z, x) = x
Tactic:
apply generic_recursor
Proof state after:
case hz

⊢ plus (z, z) = z

case hs

⊢ ∀ (n : ↑N0), plus (z, n) = n → plus (z, S n) = S n
Theorem: zero_plus_x_eq_eq
Proof state before:
case hz

⊢ plus (z, z) = z
Tactic:
exact zplus z
Proof state after:
no goals
Theorem: zero_plus_x_eq_eq
Proof state before:
case hs

⊢ ∀ (n : ↑N0), plus (z, n) = n → plus (z, S n) = S n
Tactic:
intros n hi
Proof state after:
case hs
n : ↑N0
hi : plus (z, n) = n
⊢ plus (z, S n) = S n