internlm/Lean-Github huggingface dataset:
Theorem: gapAfterProdPrimeRange
Proof state before:
case intro.left
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ u
hu_pos : 0 < u
hpu : p ≤ u
⊢ p < PrimeRange.prod (Nat.succ (Nat.succ k)) + u

case intro.right
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ u
hu_pos : 0 < u
hpu : p ≤ u
⊢ 2 ≤ p ∧ p ∣ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
Tactic:
. apply lt_of_le_of_lt hpu
  apply Nat.lt_add_of_pos_left
  apply PrimeRange.prodPos
Proof state after:
case intro.right
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ u
hu_pos : 0 < u
hpu : p ≤ u
⊢ 2 ≤ p ∧ p ∣ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
Theorem: gapAfterProdPrimeRange
Proof state before:
case intro.right
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ u
hu_pos : 0 < u
hpu : p ≤ u
⊢ 2 ≤ p ∧ p ∣ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
Tactic:
. apply And.intro
  . exact Nat.Prime.two_le hp.left
  . apply Nat.dvd_add _ hp.right
    apply PrimeRange.prodDvdOfLt hp.left
    linarith
Proof state after:
no goals
Theorem: gapAfterProdPrimeRange
Proof state before:
case hu_pos
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ u
⊢ 0 < u
Tactic:
linarith
Proof state after:
no goals
Theorem: gapAfterProdPrimeRange
Proof state before:
case intro.left
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ u
hu_pos : 0 < u
hpu : p ≤ u
⊢ p < PrimeRange.prod (Nat.succ (Nat.succ k)) + u
Tactic:
apply lt_of_le_of_lt hpu
Proof state after:
case intro.left
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ u
hu_pos : 0 < u
hpu : p ≤ u
⊢ u < PrimeRange.prod (Nat.succ (Nat.succ k)) + u
Theorem: gapAfterProdPrimeRange
Proof state before:
case intro.left
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ u
hu_pos : 0 < u
hpu : p ≤ u
⊢ u < PrimeRange.prod (Nat.succ (Nat.succ k)) + u
Tactic:
apply Nat.lt_add_of_pos_left
Proof state after:
case intro.left.h
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ u
hu_pos : 0 < u
hpu : p ≤ u
⊢ 0 < PrimeRange.prod (Nat.succ (Nat.succ k))
Theorem: gapAfterProdPrimeRange
Proof state before:
case intro.left.h
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ u
hu_pos : 0 < u
hpu : p ≤ u
⊢ 0 < PrimeRange.prod (Nat.succ (Nat.succ k))
Tactic:
apply PrimeRange.prodPos
Proof state after:
no goals
Theorem: gapAfterProdPrimeRange
Proof state before:
case intro.right
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ u
hu_pos : 0 < u
hpu : p ≤ u
⊢ 2 ≤ p ∧ p ∣ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
Tactic:
apply And.intro
Proof state after:
case intro.right.left
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ u
hu_pos : 0 < u
hpu : p ≤ u
⊢ 2 ≤ p

case intro.right.right
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ u
hu_pos : 0 < u
hpu : p ≤ u
⊢ p ∣ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
Theorem: gapAfterProdPrimeRange
Proof state before:
case intro.right.left
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ u
hu_pos : 0 < u
hpu : p ≤ u
⊢ 2 ≤ p

case intro.right.right
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ u
hu_pos : 0 < u
hpu : p ≤ u
⊢ p ∣ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
Tactic:
. exact Nat.Prime.two_le hp.left
Proof state after:
case intro.right.right
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ u
hu_pos : 0 < u
hpu : p ≤ u
⊢ p ∣ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
Theorem: gapAfterProdPrimeRange
Proof state before:
case intro.right.right
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ u
hu_pos : 0 < u
hpu : p ≤ u
⊢ p ∣ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
Tactic:
. apply Nat.dvd_add _ hp.right
  apply PrimeRange.prodDvdOfLt hp.left
  linarith
Proof state after:
no goals
Theorem: gapAfterProdPrimeRange
Proof state before:
case intro.right.left
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ u
hu_pos : 0 < u
hpu : p ≤ u
⊢ 2 ≤ p
Tactic:
exact Nat.Prime.two_le hp.left
Proof state after:
no goals
Theorem: gapAfterProdPrimeRange
Proof state before:
case intro.right.right
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ u
hu_pos : 0 < u
hpu : p ≤ u
⊢ p ∣ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
Tactic:
apply Nat.dvd_add _ hp.right
Proof state after:
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ u
hu_pos : 0 < u
hpu : p ≤ u
⊢ p ∣ PrimeRange.prod (Nat.succ (Nat.succ k))
Theorem: gapAfterProdPrimeRange
Proof state before:
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ u
hu_pos : 0 < u
hpu : p ≤ u
⊢ p ∣ PrimeRange.prod (Nat.succ (Nat.succ k))
Tactic:
apply PrimeRange.prodDvdOfLt hp.left
Proof state after:
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ u
hu_pos : 0 < u
hpu : p ≤ u
⊢ p < Nat.succ (Nat.succ k)
Theorem: gapAfterProdPrimeRange
Proof state before:
k u : ℕ
a✝¹ : 2 ≤ u ∧ u ≤ Nat.succ k
a✝ : 2 ≤ PrimeRange.prod (Nat.succ (Nat.succ k)) + u
this : u ≠ 1
p : ℕ
hp : Nat.Prime p ∧ p ∣ u
hu_pos : 0 < u
hpu : p ≤ u
⊢ p < Nat.succ (Nat.succ k)
Tactic:
linarith
Proof state after:
no goals
Theorem: existsGap
Proof state before:
k : ℕ
⊢ ∃ m, ∀ (x : ℕ), x < k → ¬Nat.Prime (m + x)
Tactic:
exists PrimeRange.prod k.succ.succ + 2
Proof state after:
k : ℕ
⊢ ∀ (x : ℕ), x < k → ¬Nat.Prime (PrimeRange.prod (Nat.succ (Nat.succ k)) + 2 + x)
Theorem: existsGap
Proof state before:
k : ℕ
⊢ ∀ (x : ℕ), x < k → ¬Nat.Prime (PrimeRange.prod (Nat.succ (Nat.succ k)) + 2 + x)
Tactic:
intros x hx
Proof state after:
k x : ℕ
hx : x < k
⊢ ¬Nat.Prime (PrimeRange.prod (Nat.succ (Nat.succ k)) + 2 + x)
Theorem: existsGap
Proof state before:
k x : ℕ
hx : x < k
⊢ ¬Nat.Prime (PrimeRange.prod (Nat.succ (Nat.succ k)) + 2 + x)
Tactic:
rw [add_assoc]
Proof state after:
k x : ℕ
hx : x < k
⊢ ¬Nat.Prime (PrimeRange.prod (Nat.succ (Nat.succ k)) + (2 + x))
Theorem: existsGap
Proof state before:
k x : ℕ
hx : x < k
⊢ ¬Nat.Prime (PrimeRange.prod (Nat.succ (Nat.succ k)) + (2 + x))
Tactic:
apply gapAfterProdPrimeRange
Proof state after:
case a
k x : ℕ
hx : x < k
⊢ 2 ≤ 2 + x ∧ 2 + x ≤ Nat.succ k
Theorem: existsGap
Proof state before:
case a
k x : ℕ
hx : x < k
⊢ 2 ≤ 2 + x ∧ 2 + x ≤ Nat.succ k
Tactic:
simp
Proof state after:
case a
k x : ℕ
hx : x < k
⊢ 2 + x ≤ Nat.succ k
Theorem: existsGap
Proof state before:
case a
k x : ℕ
hx : x < k
⊢ 2 + x ≤ Nat.succ k
Tactic:
linarith
Proof state after:
no goals
Theorem: powNeOneIff'
Proof state before:
x i : ℕ
⊢ x ^ i ≠ 1 ↔ i ≠ 0 ∧ x ≠ 1
Tactic:
cases i with
| zero => simp
| succ i =>
  simp [not_iff_not]
  simp [pow_succ]  intro hx
  simp [hx]
Proof state after:
no goals
Theorem: powNeOneIff'
Proof state before:
case zero
x : ℕ
⊢ x ^ Nat.zero ≠ 1 ↔ Nat.zero ≠ 0 ∧ x ≠ 1
Tactic:
simp
Proof state after:
no goals
Theorem: powNeOneIff'
Proof state before:
case succ
x i : ℕ
⊢ x ^ Nat.succ i ≠ 1 ↔ Nat.succ i ≠ 0 ∧ x ≠ 1
Tactic:
simp [not_iff_not]
Proof state after:
case succ
x i : ℕ
⊢ x ^ Nat.succ i = 1 ↔ x = 1
Theorem: powNeOneIff'
Proof state before:
case succ
x i : ℕ
⊢ x ^ Nat.succ i = 1 ↔ x = 1
Tactic:
simp [pow_succ]
Proof state after:
case succ
x i : ℕ
⊢ x = 1 → x ^ i = 1
Theorem: powNeOneIff'
Proof state before:
case succ
x i : ℕ
⊢ x = 1 → x ^ i = 1
Tactic:
intro hx
Proof state after:
case succ
x i : ℕ
hx : x = 1
⊢ x ^ i = 1
Theorem: powNeOneIff'
Proof state before:
case succ
x i : ℕ
hx : x = 1
⊢ x ^ i = 1
Tactic:
simp [hx]
Proof state after:
no goals
Theorem: primeOfPowFactorizationNeOne
Proof state before:
x n p : ℕ
⊢ p ^ ↑(Nat.factorization n) x ≠ 1 → Nat.Prime x
Tactic:
intro hx
Proof state after:
x n p : ℕ
hx : p ^ ↑(Nat.factorization n) x ≠ 1
⊢ Nat.Prime x
Theorem: primeOfPowFactorizationNeOne
Proof state before:
x n p : ℕ
hx : p ^ ↑(Nat.factorization n) x ≠ 1
⊢ Nat.Prime x
Tactic:
rw [powNeOneIff'] at hx
Proof state after:
x n p : ℕ
hx : ↑(Nat.factorization n) x ≠ 0 ∧ p ≠ 1
⊢ Nat.Prime x
Theorem: primeOfPowFactorizationNeOne
Proof state before:
x n p : ℕ
hx : ↑(Nat.factorization n) x ≠ 0 ∧ p ≠ 1
⊢ Nat.Prime x
Tactic:
by_contra hp
Proof state after:
x n p : ℕ
hx : ↑(Nat.factorization n) x ≠ 0 ∧ p ≠ 1
hp : ¬Nat.Prime x
⊢ False
Theorem: primeOfPowFactorizationNeOne
Proof state before:
x n p : ℕ
hx : ↑(Nat.factorization n) x ≠ 0 ∧ p ≠ 1
hp : ¬Nat.Prime x
⊢ False
Tactic:
cases hx with | intro h hx =>
apply h
simp
exact Nat.factorization_eq_zero_of_non_prime _ hp
Proof state after:
no goals
Theorem: primeOfPowFactorizationNeOne
Proof state before:
case intro
x n p : ℕ
hp : ¬Nat.Prime x
h : ↑(Nat.factorization n) x ≠ 0
hx : p ≠ 1
⊢ False
Tactic:
apply h
Proof state after:
case intro
x n p : ℕ
hp : ¬Nat.Prime x
h : ↑(Nat.factorization n) x ≠ 0
hx : p ≠ 1
⊢ ↑(Nat.factorization n) x = 0
Theorem: primeOfPowFactorizationNeOne
Proof state before:
case intro
x n p : ℕ
hp : ¬Nat.Prime x
h : ↑(Nat.factorization n) x ≠ 0
hx : p ≠ 1
⊢ ↑(Nat.factorization n) x = 0
Tactic:
exact Nat.factorization_eq_zero_of_non_prime _ hp
Proof state after:
no goals
Theorem: FactorizationCentralBinom.leOne
Proof state before:
n p : ℕ
hp : Nat.Prime p
⊢ 2 * n < p ^ 2 → ↑(Nat.factorization (Nat.centralBinom n)) p ≤ 1
Tactic:
intro hnp
Proof state after:
n p : ℕ
hp : Nat.Prime p
hnp : 2 * n < p ^ 2
⊢ ↑(Nat.factorization (Nat.centralBinom n)) p ≤ 1
Theorem: FactorizationCentralBinom.leOne
Proof state before:
n p : ℕ
hp : Nat.Prime p
hnp : 2 * n < p ^ 2
⊢ ↑(Nat.factorization (Nat.centralBinom n)) p ≤ 1
Tactic:
apply le_trans (Nat.factorization_choose_le_log)
Proof state after:
n p : ℕ
hp : Nat.Prime p
hnp : 2 * n < p ^ 2
⊢ Nat.log p (2 * n) ≤ 1
Theorem: FactorizationCentralBinom.leOne
Proof state before:
n p : ℕ
hp : Nat.Prime p
hnp : 2 * n < p ^ 2
⊢ Nat.log p (2 * n) ≤ 1
Tactic:
have hnp := Nat.le_pred_of_lt hnp
Proof state after:
n p : ℕ
hp : Nat.Prime p
hnp✝ : 2 * n < p ^ 2
hnp : 2 * n ≤ p ^ 2 - 1
⊢ Nat.log p (2 * n) ≤ 1
Theorem: FactorizationCentralBinom.leOne
Proof state before:
n p : ℕ
hp : Nat.Prime p
hnp✝ : 2 * n < p ^ 2
hnp : 2 * n ≤ p ^ 2 - 1
⊢ Nat.log p (2 * n) ≤ 1
Tactic:
apply le_trans (Nat.log_mono_right hnp)
Proof state after:
n p : ℕ
hp : Nat.Prime p
hnp✝ : 2 * n < p ^ 2
hnp : 2 * n ≤ p ^ 2 - 1
⊢ Nat.log p (p ^ 2 - 1) ≤ 1
Theorem: FactorizationCentralBinom.leOne
Proof state before:
n p : ℕ
hp : Nat.Prime p
hnp✝ : 2 * n < p ^ 2
hnp : 2 * n ≤ p ^ 2 - 1
⊢ Nat.log p (p ^ 2 - 1) ≤ 1
Tactic:
rw [← Nat.lt_succ_iff]
Proof state after:
n p : ℕ
hp : Nat.Prime p
hnp✝ : 2 * n < p ^ 2
hnp : 2 * n ≤ p ^ 2 - 1
⊢ Nat.log p (p ^ 2 - 1) < Nat.succ 1
Theorem: FactorizationCentralBinom.leOne
Proof state before:
n p : ℕ
hp : Nat.Prime p
hnp✝ : 2 * n < p ^ 2
hnp : 2 * n ≤ p ^ 2 - 1
⊢ Nat.log p (p ^ 2 - 1) < Nat.succ 1
Tactic:
have hp := Nat.Prime.one_lt hp
Proof state after:
n p : ℕ
hp✝ : Nat.Prime p
hnp✝ : 2 * n < p ^ 2
hnp : 2 * n ≤ p ^ 2 - 1
hp : 1 < p
⊢ Nat.log p (p ^ 2 - 1) < Nat.succ 1
Theorem: FactorizationCentralBinom.leOne
Proof state before:
n p : ℕ
hp✝ : Nat.Prime p
hnp✝ : 2 * n < p ^ 2
hnp : 2 * n ≤ p ^ 2 - 1
hp : 1 < p
⊢ Nat.log p (p ^ 2 - 1) < Nat.succ 1
Tactic:
apply Nat.log_lt_of_lt_pow
Proof state after:
case hy
n p : ℕ
hp✝ : Nat.Prime p
hnp✝ : 2 * n < p ^ 2
hnp : 2 * n ≤ p ^ 2 - 1
hp : 1 < p
⊢ p ^ 2 - 1 ≠ 0

case a
n p : ℕ
hp✝ : Nat.Prime p
hnp✝ : 2 * n < p ^ 2
hnp : 2 * n ≤ p ^ 2 - 1
hp : 1 < p
⊢ p ^ 2 - 1 < p ^ Nat.succ 1
Theorem: FactorizationCentralBinom.leOne
Proof state before:
case hy
n p : ℕ
hp✝ : Nat.Prime p
hnp✝ : 2 * n < p ^ 2
hnp : 2 * n ≤ p ^ 2 - 1
hp : 1 < p
⊢ p ^ 2 - 1 ≠ 0

case a
n p : ℕ
hp✝ : Nat.Prime p
hnp✝ : 2 * n < p ^ 2
hnp : 2 * n ≤ p ^ 2 - 1
hp : 1 < p
⊢ p ^ 2 - 1 < p ^ Nat.succ 1
Tactic:
. simp [hp]
Proof state after:
case a
n p : ℕ
hp✝ : Nat.Prime p
hnp✝ : 2 * n < p ^ 2
hnp : 2 * n ≤ p ^ 2 - 1
hp : 1 < p
⊢ p ^ 2 - 1 < p ^ Nat.succ 1
Theorem: FactorizationCentralBinom.leOne
Proof state before:
case a
n p : ℕ
hp✝ : Nat.Prime p
hnp✝ : 2 * n < p ^ 2
hnp : 2 * n ≤ p ^ 2 - 1
hp : 1 < p
⊢ p ^ 2 - 1 < p ^ Nat.succ 1
Tactic:
. apply Nat.pred_lt
  simp [hp]
  linarith
Proof state after:
no goals
Theorem: FactorizationCentralBinom.leOne
Proof state before:
case hy
n p : ℕ
hp✝ : Nat.Prime p
hnp✝ : 2 * n < p ^ 2
hnp : 2 * n ≤ p ^ 2 - 1
hp : 1 < p
⊢ p ^ 2 - 1 ≠ 0
Tactic:
simp [hp]
Proof state after:
no goals
Theorem: FactorizationCentralBinom.leOne
Proof state before:
case a
n p : ℕ
hp✝ : Nat.Prime p
hnp✝ : 2 * n < p ^ 2
hnp : 2 * n ≤ p ^ 2 - 1
hp : 1 < p
⊢ p ^ 2 - 1 < p ^ Nat.succ 1
Tactic:
apply Nat.pred_lt
Proof state after:
case a.a
n p : ℕ
hp✝ : Nat.Prime p
hnp✝ : 2 * n < p ^ 2
hnp : 2 * n ≤ p ^ 2 - 1
hp : 1 < p
⊢ Nat.sub (p ^ 2) 0 ≠ 0
Theorem: FactorizationCentralBinom.leOne
Proof state before:
case a.a
n p : ℕ
hp✝ : Nat.Prime p
hnp✝ : 2 * n < p ^ 2
hnp : 2 * n ≤ p ^ 2 - 1
hp : 1 < p
⊢ Nat.sub (p ^ 2) 0 ≠ 0
Tactic:
simp [hp]
Proof state after:
case a.a
n p : ℕ
hp✝ : Nat.Prime p
hnp✝ : 2 * n < p ^ 2
hnp : 2 * n ≤ p ^ 2 - 1
hp : 1 < p
⊢ ¬p = 0
Theorem: FactorizationCentralBinom.leOne
Proof state before:
case a.a
n p : ℕ
hp✝ : Nat.Prime p
hnp✝ : 2 * n < p ^ 2
hnp : 2 * n ≤ p ^ 2 - 1
hp : 1 < p
⊢ ¬p = 0
Tactic:
linarith
Proof state after:
no goals
Theorem: FactorizationCentralBinom.prodIcoPowLePow
Proof state before:
n : ℕ
s : Finset ℕ
hn : 0 < n
⊢ ∏ p in s, p ^ ↑(Nat.factorization (Nat.centralBinom n)) p ≤ (2 * n) ^ Finset.card s
Tactic:
apply Finset.prod_le_pow_card
Proof state after:
case h
n : ℕ
s : Finset ℕ
hn : 0 < n
⊢ ∀ (x : ℕ), x ∈ s → x ^ ↑(Nat.factorization (Nat.centralBinom n)) x ≤ 2 * n
Theorem: FactorizationCentralBinom.prodIcoPowLePow
Proof state before:
case h
n : ℕ
s : Finset ℕ
hn : 0 < n
⊢ ∀ (x : ℕ), x ∈ s → x ^ ↑(Nat.factorization (Nat.centralBinom n)) x ≤ 2 * n
Tactic:
intro x _
Proof state after:
case h
n : ℕ
s : Finset ℕ
hn : 0 < n
x : ℕ
a✝ : x ∈ s
⊢ x ^ ↑(Nat.factorization (Nat.centralBinom n)) x ≤ 2 * n
Theorem: FactorizationCentralBinom.prodIcoPowLePow
Proof state before:
case h
n : ℕ
s : Finset ℕ
hn : 0 < n
x : ℕ
a✝ : x ∈ s
⊢ x ^ ↑(Nat.factorization (Nat.centralBinom n)) x ≤ 2 * n
Tactic:
apply Nat.pow_factorization_choose_le
Proof state after:
case h.hn
n : ℕ
s : Finset ℕ
hn : 0 < n
x : ℕ
a✝ : x ∈ s
⊢ 0 < 2 * n
Theorem: FactorizationCentralBinom.prodIcoPowLePow
Proof state before:
case h.hn
n : ℕ
s : Finset ℕ
hn : 0 < n
x : ℕ
a✝ : x ∈ s
⊢ 0 < 2 * n
Tactic:
linarith
Proof state after:
no goals
Theorem: FactorizationCentralBinom.prodIcoPowLePow'
Proof state before:
n : ℕ
s : Finset ℕ
hs : n = 0 → s = ∅
⊢ ∏ p in s, p ^ ↑(Nat.factorization (Nat.centralBinom n)) p ≤ (2 * n) ^ Finset.card s
Tactic:
apply Finset.prod_le_pow_card
Proof state after:
case h
n : ℕ
s : Finset ℕ
hs : n = 0 → s = ∅
⊢ ∀ (x : ℕ), x ∈ s → x ^ ↑(Nat.factorization (Nat.centralBinom n)) x ≤ 2 * n
Theorem: FactorizationCentralBinom.prodIcoPowLePow'
Proof state before:
case h
n : ℕ
s : Finset ℕ
hs : n = 0 → s = ∅
⊢ ∀ (x : ℕ), x ∈ s → x ^ ↑(Nat.factorization (Nat.centralBinom n)) x ≤ 2 * n
Tactic:
intro x hx
Proof state after:
case h
n : ℕ
s : Finset ℕ
hs : n = 0 → s = ∅
x : ℕ
hx : x ∈ s
⊢ x ^ ↑(Nat.factorization (Nat.centralBinom n)) x ≤ 2 * n
Theorem: FactorizationCentralBinom.prodIcoPowLePow'
Proof state before:
case h
n : ℕ
s : Finset ℕ
hs : n = 0 → s = ∅
x : ℕ
hx : x ∈ s
⊢ x ^ ↑(Nat.factorization (Nat.centralBinom n)) x ≤ 2 * n
Tactic:
cases n with
| zero => simp at hs; rw [hs] at hx; contradiction
| succ n => apply Nat.pow_factorization_choose_le; simp
Proof state after:
no goals
Theorem: FactorizationCentralBinom.prodIcoPowLePow'
Proof state before:
case h.zero
s : Finset ℕ
x : ℕ
hx : x ∈ s
hs : Nat.zero = 0 → s = ∅
⊢ x ^ ↑(Nat.factorization (Nat.centralBinom Nat.zero)) x ≤ 2 * Nat.zero
Tactic:
simp at hs
Proof state after:
case h.zero
s : Finset ℕ
x : ℕ
hx : x ∈ s
hs : s = ∅
⊢ x ^ ↑(Nat.factorization (Nat.centralBinom Nat.zero)) x ≤ 2 * Nat.zero
Theorem: FactorizationCentralBinom.prodIcoPowLePow'
Proof state before:
case h.zero
s : Finset ℕ
x : ℕ
hx : x ∈ s
hs : s = ∅
⊢ x ^ ↑(Nat.factorization (Nat.centralBinom Nat.zero)) x ≤ 2 * Nat.zero
Tactic:
rw [hs] at hx
Proof state after:
case h.zero
s : Finset ℕ
x : ℕ
hx : x ∈ ∅
hs : s = ∅
⊢ x ^ ↑(Nat.factorization (Nat.centralBinom Nat.zero)) x ≤ 2 * Nat.zero
Theorem: FactorizationCentralBinom.prodIcoPowLePow'
Proof state before:
case h.zero
s : Finset ℕ
x : ℕ
hx : x ∈ ∅
hs : s = ∅
⊢ x ^ ↑(Nat.factorization (Nat.centralBinom Nat.zero)) x ≤ 2 * Nat.zero
Tactic:
contradiction
Proof state after:
no goals
Theorem: FactorizationCentralBinom.prodIcoPowLePow'
Proof state before:
case h.succ
s : Finset ℕ
x : ℕ
hx : x ∈ s
n : ℕ
hs : Nat.succ n = 0 → s = ∅
⊢ x ^ ↑(Nat.factorization (Nat.centralBinom (Nat.succ n))) x ≤ 2 * Nat.succ n
Tactic:
apply Nat.pow_factorization_choose_le
Proof state after:
case h.succ.hn
s : Finset ℕ
x : ℕ
hx : x ∈ s
n : ℕ
hs : Nat.succ n = 0 → s = ∅
⊢ 0 < 2 * Nat.succ n
Theorem: FactorizationCentralBinom.prodIcoPowLePow'
Proof state before:
case h.succ.hn
s : Finset ℕ
x : ℕ
hx : x ∈ s
n : ℕ
hs : Nat.succ n = 0 → s = ∅
⊢ 0 < 2 * Nat.succ n
Tactic:
simp
Proof state after:
no goals
Theorem: FactorizationCentralBinom.prodRangePowEqProdIcoPowOfLeTwo
Proof state before:
n a b : ℕ
ha : a ≤ 2
⊢ ∏ p in Finset.range b, p ^ ↑(Nat.factorization (Nat.centralBinom n)) p =
    ∏ p in Finset.Ico a b, p ^ ↑(Nat.factorization (Nat.centralBinom n)) p
Tactic:
rw [Finset.range_eq_Ico]
Proof state after:
n a b : ℕ
ha : a ≤ 2
⊢ ∏ p in Finset.Ico 0 b, p ^ ↑(Nat.factorization (Nat.centralBinom n)) p =
    ∏ p in Finset.Ico a b, p ^ ↑(Nat.factorization (Nat.centralBinom n)) p
Theorem: FactorizationCentralBinom.prodRangePowEqProdIcoPowOfLeTwo
Proof state before:
n a b : ℕ
ha : a ≤ 2
⊢ ∏ p in Finset.Ico 0 b, p ^ ↑(Nat.factorization (Nat.centralBinom n)) p =
    ∏ p in Finset.Ico a b, p ^ ↑(Nat.factorization (Nat.centralBinom n)) p
Tactic:
rw [← Finset.prod_subset (Finset.Ico_subset_Ico_left (Nat.zero_le a)) _]
Proof state after:
n a b : ℕ
ha : a ≤ 2
⊢ ∀ (x : ℕ), x ∈ Finset.Ico 0 b → ¬x ∈ Finset.Ico a b → x ^ ↑(Nat.factorization (Nat.centralBinom n)) x = 1
Theorem: FactorizationCentralBinom.prodRangePowEqProdIcoPowOfLeTwo
Proof state before:
n a b : ℕ
ha : a ≤ 2
⊢ ∀ (x : ℕ), x ∈ Finset.Ico 0 b → ¬x ∈ Finset.Ico a b → x ^ ↑(Nat.factorization (Nat.centralBinom n)) x = 1
Tactic:
simp
Proof state after:
n a b : ℕ
ha : a ≤ 2
⊢ ∀ (x : ℕ), x < b → (a ≤ x → b ≤ x) → x ^ ↑(Nat.factorization (Nat.centralBinom n)) x = 1
Theorem: FactorizationCentralBinom.prodRangePowEqProdIcoPowOfLeTwo
Proof state before:
n a b : ℕ
ha : a ≤ 2
⊢ ∀ (x : ℕ), x < b → (a ≤ x → b ≤ x) → x ^ ↑(Nat.factorization (Nat.centralBinom n)) x = 1
Tactic:
intro x hxb hbx
Proof state after:
n a b : ℕ
ha : a ≤ 2
x : ℕ
hxb : x < b
hbx : a ≤ x → b ≤ x
⊢ x ^ ↑(Nat.factorization (Nat.centralBinom n)) x = 1
Theorem: FactorizationCentralBinom.prodRangePowEqProdIcoPowOfLeTwo
Proof state before:
n a b : ℕ
ha : a ≤ 2
x : ℕ
hxb : x < b
hbx : a ≤ x → b ≤ x
⊢ x ^ ↑(Nat.factorization (Nat.centralBinom n)) x = 1
Tactic:
rw [Nat.factorization_eq_zero_of_non_prime]
Proof state after:
n a b : ℕ
ha : a ≤ 2
x : ℕ
hxb : x < b
hbx : a ≤ x → b ≤ x
⊢ x ^ 0 = 1

case hp
n a b : ℕ
ha : a ≤ 2
x : ℕ
hxb : x < b
hbx : a ≤ x → b ≤ x
⊢ ¬Nat.Prime x
Theorem: FactorizationCentralBinom.prodRangePowEqProdIcoPowOfLeTwo
Proof state before:
n a b : ℕ
ha : a ≤ 2
x : ℕ
hxb : x < b
hbx : a ≤ x → b ≤ x
⊢ x ^ 0 = 1

case hp
n a b : ℕ
ha : a ≤ 2
x : ℕ
hxb : x < b
hbx : a ≤ x → b ≤ x
⊢ ¬Nat.Prime x
Tactic:
simp
Proof state after:
case hp
n a b : ℕ
ha : a ≤ 2
x : ℕ
hxb : x < b
hbx : a ≤ x → b ≤ x
⊢ ¬Nat.Prime x
Theorem: FactorizationCentralBinom.prodRangePowEqProdIcoPowOfLeTwo
Proof state before:
case hp
n a b : ℕ
ha : a ≤ 2
x : ℕ
hxb : x < b
hbx : a ≤ x → b ≤ x
⊢ ¬Nat.Prime x
Tactic:
intro hp
Proof state after:
case hp
n a b : ℕ
ha : a ≤ 2
x : ℕ
hxb : x < b
hbx : a ≤ x → b ≤ x
hp : Nat.Prime x
⊢ False
Theorem: FactorizationCentralBinom.prodRangePowEqProdIcoPowOfLeTwo
Proof state before:
case hp
n a b : ℕ
ha : a ≤ 2
x : ℕ
hxb : x < b
hbx : a ≤ x → b ≤ x
hp : Nat.Prime x
⊢ False
Tactic:
have hp := Nat.Prime.two_le hp
Proof state after:
case hp
n a b : ℕ
ha : a ≤ 2
x : ℕ
hxb : x < b
hbx : a ≤ x → b ≤ x
hp✝ : Nat.Prime x
hp : 2 ≤ x
⊢ False
Theorem: FactorizationCentralBinom.prodRangePowEqProdIcoPowOfLeTwo
Proof state before:
case hp
n a b : ℕ
ha : a ≤ 2
x : ℕ
hxb : x < b
hbx : a ≤ x → b ≤ x
hp✝ : Nat.Prime x
hp : 2 ≤ x
⊢ False
Tactic:
specialize hbx (le_trans ha hp)
Proof state after:
case hp
n a b : ℕ
ha : a ≤ 2
x : ℕ
hxb : x < b
hp✝ : Nat.Prime x
hp : 2 ≤ x
hbx : b ≤ x
⊢ False
Theorem: FactorizationCentralBinom.prodRangePowEqProdIcoPowOfLeTwo
Proof state before:
case hp
n a b : ℕ
ha : a ≤ 2
x : ℕ
hxb : x < b
hp✝ : Nat.Prime x
hp : 2 ≤ x
hbx : b ≤ x
⊢ False
Tactic:
linarith
Proof state after:
no goals
Theorem: FactorizationCentralBinom.prodIocSqrtLePowLeProdPrimes
Proof state before:
n a b : ℕ
ha : Nat.sqrt (2 * n) ≤ a
⊢ ∏ p in Finset.Ioc a b, p ^ ↑(Nat.factorization (Nat.centralBinom n)) p ≤ ∏ p in primes (Finset.Ioc a b), p
Tactic:
rw [primes]
Proof state after:
n a b : ℕ
ha : Nat.sqrt (2 * n) ≤ a
⊢ ∏ p in Finset.Ioc a b, p ^ ↑(Nat.factorization (Nat.centralBinom n)) p ≤
    ∏ p in Finset.filter Nat.Prime (Finset.Ioc a b), p
Theorem: FactorizationCentralBinom.prodIocSqrtLePowLeProdPrimes
Proof state before:
n a b : ℕ
ha : Nat.sqrt (2 * n) ≤ a
⊢ ∏ p in Finset.Ioc a b, p ^ ↑(Nat.factorization (Nat.centralBinom n)) p ≤
    ∏ p in Finset.filter Nat.Prime (Finset.Ioc a b), p
Tactic:
rw [← @Finset.prod_filter_of_ne _ _ _ _ _ Nat.Prime]
Proof state after:
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

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
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

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:
. apply Finset.prod_le_prod'
  simp
  intro p hbp _ hp
  replace hbp := lt_of_le_of_lt ha hbp
  conv => rhs; rw [← Nat.pow_one p]
  rw [pow_le_pow_iff (Nat.Prime.one_lt hp)]
  rw [Nat.sqrt_lt'] at hbp
  exact leOne hp hbp
Proof state after:
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
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 _
  apply primeOfPowFactorizationNeOne
Proof state after:
no goals