internlm/Lean-Github huggingface dataset:
Theorem: lt4kIff
Proof state before:
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ n * 2 < 8000 ↔ n < 4000
Tactic:
rw [← lt_div_iff (by norm_num)]
Proof state after:
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ n < 8000 / 2 ↔ n < 4000
Theorem: lt4kIff
Proof state before:
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ n < 8000 / 2 ↔ n < 4000
Tactic:
norm_num
Proof state after:
no goals
Theorem: lt4kIff
Proof state before:
n : ℝ
hn : 0 < n
⊢ 4 = 2 ^ 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: lt4kIff
Proof state before:
n : ℝ
hn : 0 < n
⊢ 0 ≤ 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: lt4kIff
Proof state before:
n : ℝ
hn : 0 < n
⊢ 1 < 2
Tactic:
linarith
Proof state after:
no goals
Theorem: lt4kIff
Proof state before:
n : ℝ
hn : 0 < n
⊢ 0 < (2 * n) ^ (2 / 3)
Tactic:
apply Real.rpow_pos_of_pos
Proof state after:
case hx
n : ℝ
hn : 0 < n
⊢ 0 < 2 * n
Theorem: lt4kIff
Proof state before:
case hx
n : ℝ
hn : 0 < n
⊢ 0 < 2 * n
Tactic:
linarith
Proof state after:
no goals
Theorem: lt4kIff
Proof state before:
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ 0 ≤ 2 * n
Tactic:
linarith
Proof state after:
no goals
Theorem: lt4kIff
Proof state before:
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ 0 ≤ 20 * (2 * n) ^ (2 / 3)
Tactic:
linarith
Proof state after:
no goals
Theorem: lt4kIff
Proof state before:
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ 0 < 3
Tactic:
norm_num
Proof state after:
no goals
Theorem: lt4kIff
Proof state before:
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ 0 ≤ 20
Tactic:
norm_num
Proof state after:
no goals
Theorem: lt4kIff
Proof state before:
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ 0 ≤ (2 * n) ^ (2 / 3)
Tactic:
linarith
Proof state after:
no goals
Theorem: lt4kIff
Proof state before:
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ 3 = 1 + 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: lt4kIff
Proof state before:
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ 0 < 2 * n
Tactic:
linarith
Proof state after:
no goals
Theorem: lt4kIff
Proof state before:
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ 0 < 20
Tactic:
norm_num
Proof state after:
no goals
Theorem: lt4kIff
Proof state before:
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ 0 < (2 * n) ^ 2
Tactic:
apply sq_pos_of_pos
Proof state after:
case ha
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ 0 < 2 * n
Theorem: lt4kIff
Proof state before:
case ha
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ 0 < 2 * n
Tactic:
linarith
Proof state after:
no goals
Theorem: lt4kIff
Proof state before:
n : ℝ
hn : 0 < n
h_nonneg : 0 < (2 * n) ^ (2 / 3)
⊢ 0 < 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: bertrand
Proof state before:
n : ℕ
⊢ 0 < n → ∃ p, p ∈ Set.Ioc n (2 * n) ∧ Nat.Prime p
Tactic:
intro hn
Proof state after:
n : ℕ
hn : 0 < n
⊢ ∃ p, p ∈ Set.Ioc n (2 * n) ∧ Nat.Prime p
Theorem: bertrand
Proof state before:
n : ℕ
hn : 0 < n
⊢ ∃ p, p ∈ Set.Ioc n (2 * n) ∧ Nat.Prime p
Tactic:
cases lt_or_le n 4000 with
| inl hn' => exact landauTrick (by linarith) (by linarith)
| inr hn' =>
  by_contra h
  simp at h
  replace h : ∏ p in primes (Finset.Ioc n (2*n)), p = 1
  . apply Finset.prod_eq_one
    intro i hi
    specialize h i
    simp [primes] at *
    specialize h hi.left.left hi.left.right hi.right
    contradiction
  have h' := fourPowLeMulProdPrimes (by linarith : 2 < n)
  simp [h] at h'; clear h
  replace h' := rpowDivThreeLe (by linarith : 0 < n) h'
  have : (81 / 2 : ℝ) < ↑n
  . rw [div_lt_iff (by norm_num)]; norm_cast; linarith
  replace h' := fourPowLtOf this h'; clear this
  rw [lt4kIff (by norm_cast)] at h'
  norm_cast at h'
  linarith
Proof state after:
no goals
Theorem: bertrand
Proof state before:
case inl
n : ℕ
hn : 0 < n
hn' : n < 4000
⊢ ∃ p, p ∈ Set.Ioc n (2 * n) ∧ Nat.Prime p
Tactic:
exact landauTrick (by linarith) (by linarith)
Proof state after:
no goals
Theorem: bertrand
Proof state before:
n : ℕ
hn : 0 < n
hn' : n < 4000
⊢ 0 < n
Tactic:
linarith
Proof state after:
no goals
Theorem: bertrand
Proof state before:
n : ℕ
hn : 0 < n
hn' : n < 4000
⊢ n ≤ 4000
Tactic:
linarith
Proof state after:
no goals
Theorem: bertrand
Proof state before:
case inr
n : ℕ
hn : 0 < n
hn' : 4000 ≤ n
⊢ ∃ p, p ∈ Set.Ioc n (2 * n) ∧ Nat.Prime p
Tactic:
by_contra h
Proof state after:
case inr
n : ℕ
hn : 0 < n
hn' : 4000 ≤ n
h : ¬∃ p, p ∈ Set.Ioc n (2 * n) ∧ Nat.Prime p
⊢ False
Theorem: bertrand
Proof state before:
case inr
n : ℕ
hn : 0 < n
hn' : 4000 ≤ n
h : ¬∃ p, p ∈ Set.Ioc n (2 * n) ∧ Nat.Prime p
⊢ False
Tactic:
simp at h
Proof state after:
case inr
n : ℕ
hn : 0 < n
hn' : 4000 ≤ n
h : ∀ (x : ℕ), n < x → x ≤ 2 * n → ¬Nat.Prime x
⊢ False
Theorem: bertrand
Proof state before:
case inr
n : ℕ
hn : 0 < n
hn' : 4000 ≤ n
h : ∀ (x : ℕ), n < x → x ≤ 2 * n → ¬Nat.Prime x
⊢ False
Tactic:
replace h : ∏ p in primes (Finset.Ioc n (2*n)), p = 1
Proof state after:
case h
n : ℕ
hn : 0 < n
hn' : 4000 ≤ n
h : ∀ (x : ℕ), n < x → x ≤ 2 * n → ¬Nat.Prime x
⊢ ∏ p in primes (Finset.Ioc n (2 * n)), p = 1

case inr
n : ℕ
hn : 0 < n
hn' : 4000 ≤ n
h : ∏ p in primes (Finset.Ioc n (2 * n)), p = 1
⊢ False
Theorem: bertrand
Proof state before:
case h
n : ℕ
hn : 0 < n
hn' : 4000 ≤ n
h : ∀ (x : ℕ), n < x → x ≤ 2 * n → ¬Nat.Prime x
⊢ ∏ p in primes (Finset.Ioc n (2 * n)), p = 1

case inr
n : ℕ
hn : 0 < n
hn' : 4000 ≤ n
h : ∏ p in primes (Finset.Ioc n (2 * n)), p = 1
⊢ False
Tactic:
. apply Finset.prod_eq_one
  intro i hi
  specialize h i
  simp [primes] at *
  specialize h hi.left.left hi.left.right hi.right
  contradiction
Proof state after:
case inr
n : ℕ
hn : 0 < n
hn' : 4000 ≤ n
h : ∏ p in primes (Finset.Ioc n (2 * n)), p = 1
⊢ False
Theorem: bertrand
Proof state before:
case inr
n : ℕ
hn : 0 < n
hn' : 4000 ≤ n
h : ∏ p in primes (Finset.Ioc n (2 * n)), p = 1
⊢ False
Tactic:
have h' := fourPowLeMulProdPrimes (by linarith : 2 < n)
Proof state after:
case inr
n : ℕ
hn : 0 < n
hn' : 4000 ≤ n
h : ∏ p in primes (Finset.Ioc n (2 * n)), p = 1
h' : 4 ^ n ≤ (2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3) * ∏ p in primes (Finset.Ioc n (2 * n)), p
⊢ False
Theorem: bertrand
Proof state before:
case inr
n : ℕ
hn : 0 < n
hn' : 4000 ≤ n
h : ∏ p in primes (Finset.Ioc n (2 * n)), p = 1
h' : 4 ^ n ≤ (2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3) * ∏ p in primes (Finset.Ioc n (2 * n)), p
⊢ False
Tactic:
simp [h] at h'
Proof state after:
case inr
n : ℕ
hn : 0 < n
hn' : 4000 ≤ n
h : ∏ p in primes (Finset.Ioc n (2 * n)), p = 1
h' : 4 ^ n ≤ (2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3)
⊢ False
Theorem: bertrand
Proof state before:
case inr
n : ℕ
hn : 0 < n
hn' : 4000 ≤ n
h : ∏ p in primes (Finset.Ioc n (2 * n)), p = 1
h' : 4 ^ n ≤ (2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3)
⊢ False
Tactic:
clear h
Proof state after:
case inr
n : ℕ
hn : 0 < n
hn' : 4000 ≤ n
h' : 4 ^ n ≤ (2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3)
⊢ False
Theorem: bertrand
Proof state before:
case inr
n : ℕ
hn : 0 < n
hn' : 4000 ≤ n
h' : 4 ^ n ≤ (2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3)
⊢ False
Tactic:
replace h' := rpowDivThreeLe (by linarith : 0 < n) h'
Proof state after:
case inr
n : ℕ
hn : 0 < n
hn' : 4000 ≤ n
h' : 4 ^ (↑n / 3) ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n))
⊢ False
Theorem: bertrand
Proof state before:
case inr
n : ℕ
hn : 0 < n
hn' : 4000 ≤ n
h' : 4 ^ (↑n / 3) ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n))
⊢ False
Tactic:
have : (81 / 2 : ℝ) < ↑n
Proof state after:
case this
n : ℕ
hn : 0 < n
hn' : 4000 ≤ n
h' : 4 ^ (↑n / 3) ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n))
⊢ 81 / 2 < ↑n

case inr
n : ℕ
hn : 0 < n
hn' : 4000 ≤ n
h' : 4 ^ (↑n / 3) ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n))
this : 81 / 2 < ↑n
⊢ False
Theorem: bertrand
Proof state before:
case this
n : ℕ
hn : 0 < n
hn' : 4000 ≤ n
h' : 4 ^ (↑n / 3) ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n))
⊢ 81 / 2 < ↑n

case inr
n : ℕ
hn : 0 < n
hn' : 4000 ≤ n
h' : 4 ^ (↑n / 3) ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n))
this : 81 / 2 < ↑n
⊢ False
Tactic:
. rw [div_lt_iff (by norm_num)]; norm_cast; linarith
Proof state after:
case inr
n : ℕ
hn : 0 < n
hn' : 4000 ≤ n
h' : 4 ^ (↑n / 3) ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n))
this : 81 / 2 < ↑n
⊢ False
Theorem: bertrand
Proof state before:
case inr
n : ℕ
hn : 0 < n
hn' : 4000 ≤ n
h' : 4 ^ (↑n / 3) ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n))
this : 81 / 2 < ↑n
⊢ False
Tactic:
replace h' := fourPowLtOf this h'
Proof state after:
case inr
n : ℕ
hn : 0 < n
hn' : 4000 ≤ n
this : 81 / 2 < ↑n
h' : 4 ^ ↑n < 2 ^ (20 * (2 * ↑n) ^ (2 / 3))
⊢ False
Theorem: bertrand
Proof state before:
case inr
n : ℕ
hn : 0 < n
hn' : 4000 ≤ n
this : 81 / 2 < ↑n
h' : 4 ^ ↑n < 2 ^ (20 * (2 * ↑n) ^ (2 / 3))
⊢ False
Tactic:
clear this
Proof state after:
case inr
n : ℕ
hn : 0 < n
hn' : 4000 ≤ n
h' : 4 ^ ↑n < 2 ^ (20 * (2 * ↑n) ^ (2 / 3))
⊢ False
Theorem: bertrand
Proof state before:
case inr
n : ℕ
hn : 0 < n
hn' : 4000 ≤ n
h' : 4 ^ ↑n < 2 ^ (20 * (2 * ↑n) ^ (2 / 3))
⊢ False
Tactic:
rw [lt4kIff (by norm_cast)] at h'
Proof state after:
case inr
n : ℕ
hn : 0 < n
hn' : 4000 ≤ n
h' : ↑n < 4000
⊢ False
Theorem: bertrand
Proof state before:
case inr
n : ℕ
hn : 0 < n
hn' : 4000 ≤ n
h' : ↑n < 4000
⊢ False
Tactic:
norm_cast at h'
Proof state after:
case inr
n : ℕ
hn : 0 < n
hn' : 4000 ≤ n
h' : n < 4000
⊢ False
Theorem: bertrand
Proof state before:
case inr
n : ℕ
hn : 0 < n
hn' : 4000 ≤ n
h' : n < 4000
⊢ False
Tactic:
linarith
Proof state after:
no goals
Theorem: bertrand
Proof state before:
case h
n : ℕ
hn : 0 < n
hn' : 4000 ≤ n
h : ∀ (x : ℕ), n < x → x ≤ 2 * n → ¬Nat.Prime x
⊢ ∏ p in primes (Finset.Ioc n (2 * n)), p = 1
Tactic:
apply Finset.prod_eq_one
Proof state after:
case h.h
n : ℕ
hn : 0 < n
hn' : 4000 ≤ n
h : ∀ (x : ℕ), n < x → x ≤ 2 * n → ¬Nat.Prime x
⊢ ∀ (x : ℕ), x ∈ primes (Finset.Ioc n (2 * n)) → x = 1
Theorem: bertrand
Proof state before:
case h.h
n : ℕ
hn : 0 < n
hn' : 4000 ≤ n
h : ∀ (x : ℕ), n < x → x ≤ 2 * n → ¬Nat.Prime x
⊢ ∀ (x : ℕ), x ∈ primes (Finset.Ioc n (2 * n)) → x = 1
Tactic:
intro i hi
Proof state after:
case h.h
n : ℕ
hn : 0 < n
hn' : 4000 ≤ n
h : ∀ (x : ℕ), n < x → x ≤ 2 * n → ¬Nat.Prime x
i : ℕ
hi : i ∈ primes (Finset.Ioc n (2 * n))
⊢ i = 1
Theorem: bertrand
Proof state before:
case h.h
n : ℕ
hn : 0 < n
hn' : 4000 ≤ n
h : ∀ (x : ℕ), n < x → x ≤ 2 * n → ¬Nat.Prime x
i : ℕ
hi : i ∈ primes (Finset.Ioc n (2 * n))
⊢ i = 1
Tactic:
specialize h i
Proof state after:
case h.h
n : ℕ
hn : 0 < n
hn' : 4000 ≤ n
i : ℕ
hi : i ∈ primes (Finset.Ioc n (2 * n))
h : n < i → i ≤ 2 * n → ¬Nat.Prime i
⊢ i = 1
Theorem: bertrand
Proof state before:
case h.h
n : ℕ
hn : 0 < n
hn' : 4000 ≤ n
i : ℕ
hi : i ∈ primes (Finset.Ioc n (2 * n))
h : n < i → i ≤ 2 * n → ¬Nat.Prime i
⊢ i = 1
Tactic:
simp [primes] at *
Proof state after:
case h.h
n : ℕ
hn : 0 < n
hn' : 4000 ≤ n
i : ℕ
h : n < i → i ≤ 2 * n → ¬Nat.Prime i
hi : (n < i ∧ i ≤ 2 * n) ∧ Nat.Prime i
⊢ i = 1
Theorem: bertrand
Proof state before:
case h.h
n : ℕ
hn : 0 < n
hn' : 4000 ≤ n
i : ℕ
h : n < i → i ≤ 2 * n → ¬Nat.Prime i
hi : (n < i ∧ i ≤ 2 * n) ∧ Nat.Prime i
⊢ i = 1
Tactic:
specialize h hi.left.left hi.left.right hi.right
Proof state after:
case h.h
n : ℕ
hn : 0 < n
hn' : 4000 ≤ n
i : ℕ
hi : (n < i ∧ i ≤ 2 * n) ∧ Nat.Prime i
h : False
⊢ i = 1
Theorem: bertrand
Proof state before:
case h.h
n : ℕ
hn : 0 < n
hn' : 4000 ≤ n
i : ℕ
hi : (n < i ∧ i ≤ 2 * n) ∧ Nat.Prime i
h : False
⊢ i = 1
Tactic:
contradiction
Proof state after:
no goals
Theorem: bertrand
Proof state before:
n : ℕ
hn : 0 < n
hn' : 4000 ≤ n
h : ∏ p in primes (Finset.Ioc n (2 * n)), p = 1
⊢ 2 < n
Tactic:
linarith
Proof state after:
no goals
Theorem: bertrand
Proof state before:
n : ℕ
hn : 0 < n
hn' : 4000 ≤ n
h' : 4 ^ n ≤ (2 * n) ^ (1 + Nat.sqrt (2 * n)) * 4 ^ Nat.pred (2 * n / 3)
⊢ 0 < n
Tactic:
linarith
Proof state after:
no goals
Theorem: bertrand
Proof state before:
case this
n : ℕ
hn : 0 < n
hn' : 4000 ≤ n
h' : 4 ^ (↑n / 3) ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n))
⊢ 81 / 2 < ↑n
Tactic:
rw [div_lt_iff (by norm_num)]
Proof state after:
case this
n : ℕ
hn : 0 < n
hn' : 4000 ≤ n
h' : 4 ^ (↑n / 3) ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n))
⊢ 81 < ↑n * 2
Theorem: bertrand
Proof state before:
case this
n : ℕ
hn : 0 < n
hn' : 4000 ≤ n
h' : 4 ^ (↑n / 3) ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n))
⊢ 81 < ↑n * 2
Tactic:
norm_cast
Proof state after:
case this
n : ℕ
hn : 0 < n
hn' : 4000 ≤ n
h' : 4 ^ (↑n / 3) ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n))
⊢ 81 < n * 2
Theorem: bertrand
Proof state before:
case this
n : ℕ
hn : 0 < n
hn' : 4000 ≤ n
h' : 4 ^ (↑n / 3) ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n))
⊢ 81 < n * 2
Tactic:
linarith
Proof state after:
no goals
Theorem: bertrand
Proof state before:
n : ℕ
hn : 0 < n
hn' : 4000 ≤ n
h' : 4 ^ (↑n / 3) ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n))
⊢ 0 < 2
Tactic:
norm_num
Proof state after:
no goals
Theorem: bertrand
Proof state before:
n : ℕ
hn : 0 < n
hn' : 4000 ≤ n
h' : 4 ^ ↑n < 2 ^ (20 * (2 * ↑n) ^ (2 / 3))
⊢ 0 < ↑n
Tactic:
norm_cast
Proof state after:
no goals
Theorem: chooseHalfLePowFour
Proof state before:
m : ℕ
⊢ ∑ k in {m}, Nat.choose (2 * m + 1) k = ∑ k in Finset.Ico m (m + 1), Nat.choose (2 * m + 1) k
Tactic:
rw [Nat.Ico_succ_singleton]
Proof state after:
no goals
Theorem: chooseHalfLePowFour
Proof state before:
m : ℕ
⊢ ∑ k in Finset.Ico 0 (m + 1), Nat.choose (2 * m + 1) k = ∑ k in Finset.range (m + 1), Nat.choose (2 * m + 1) k
Tactic:
rw [Finset.range_eq_Ico]
Proof state after:
no goals
Theorem: prodPrimesIocLeChoose
Proof state before:
m : ℕ
⊢ ∏ p in primes (Finset.Ioc (m + 1) (2 * m + 1)), p ≤ Nat.choose (2 * m + 1) m
Tactic:
rw [primes]
Proof state after:
m : ℕ
⊢ ∏ p in Finset.filter Nat.Prime (Finset.Ioc (m + 1) (2 * m + 1)), p ≤ Nat.choose (2 * m + 1) m
Theorem: prodPrimesIocLeChoose
Proof state before:
m : ℕ
⊢ ∏ p in Finset.filter Nat.Prime (Finset.Ioc (m + 1) (2 * m + 1)), p ≤ Nat.choose (2 * m + 1) m
Tactic:
apply Nat.le_of_dvd
Proof state after:
case h
m : ℕ
⊢ 0 < Nat.choose (2 * m + 1) m

case a
m : ℕ
⊢ ∏ p in Finset.filter Nat.Prime (Finset.Ioc (m + 1) (2 * m + 1)), p ∣ Nat.choose (2 * m + 1) m
Theorem: prodPrimesIocLeChoose
Proof state before:
case h
m : ℕ
⊢ 0 < Nat.choose (2 * m + 1) m

case a
m : ℕ
⊢ ∏ p in Finset.filter Nat.Prime (Finset.Ioc (m + 1) (2 * m + 1)), p ∣ Nat.choose (2 * m + 1) m
Tactic:
. apply Nat.choose_pos; linarith
Proof state after:
case a
m : ℕ
⊢ ∏ p in Finset.filter Nat.Prime (Finset.Ioc (m + 1) (2 * m + 1)), p ∣ Nat.choose (2 * m + 1) m
Theorem: prodPrimesIocLeChoose
Proof state before:
case a
m : ℕ
⊢ ∏ p in Finset.filter Nat.Prime (Finset.Ioc (m + 1) (2 * m + 1)), p ∣ Nat.choose (2 * m + 1) m
Tactic:
apply Finset.prod_primes_dvd <;> simp [← Nat.prime_iff]
Proof state after:
case a.div
m : ℕ
⊢ ∀ (a : ℕ), m + 1 < a → a ≤ 2 * m + 1 → Nat.Prime a → a ∣ Nat.choose (2 * m + 1) m
Theorem: prodPrimesIocLeChoose
Proof state before:
case a.div
m : ℕ
⊢ ∀ (a : ℕ), m + 1 < a → a ≤ 2 * m + 1 → Nat.Prime a → a ∣ Nat.choose (2 * m + 1) m
Tactic:
intro p ha hb hp
Proof state after:
case a.div
m p : ℕ
ha : m + 1 < p
hb : p ≤ 2 * m + 1
hp : Nat.Prime p
⊢ p ∣ Nat.choose (2 * m + 1) m
Theorem: prodPrimesIocLeChoose
Proof state before:
case a.div
m p : ℕ
ha : m + 1 < p
hb : p ≤ 2 * m + 1
hp : Nat.Prime p
⊢ p ∣ Nat.choose (2 * m + 1) m
Tactic:
rw [two_mul, add_assoc]
Proof state after:
case a.div
m p : ℕ
ha : m + 1 < p
hb : p ≤ 2 * m + 1
hp : Nat.Prime p
⊢ p ∣ Nat.choose (m + (m + 1)) m
Theorem: prodPrimesIocLeChoose
Proof state before:
case a.div
m p : ℕ
ha : m + 1 < p
hb : p ≤ 2 * m + 1
hp : Nat.Prime p
⊢ p ∣ Nat.choose (m + (m + 1)) m
Tactic:
apply Nat.Prime.dvd_choose_add hp <;> linarith
Proof state after:
no goals
Theorem: prodPrimesIocLeChoose
Proof state before:
case h
m : ℕ
⊢ 0 < Nat.choose (2 * m + 1) m
Tactic:
apply Nat.choose_pos
Proof state after:
case h.a
m : ℕ
⊢ m ≤ 2 * m + 1
Theorem: prodPrimesIocLeChoose
Proof state before:
case h.a
m : ℕ
⊢ m ≤ 2 * m + 1
Tactic:
linarith
Proof state after:
no goals
Theorem: primesSuccEqPrimesSelf
Proof state before:
n : ℕ
hn : ¬Nat.Prime (Nat.succ n)
⊢ primes (Finset.range (Nat.succ (Nat.succ n))) = primes (Finset.range (Nat.succ n))
Tactic:
simp [primes]
Proof state after:
n : ℕ
hn : ¬Nat.Prime (Nat.succ n)
⊢ Finset.filter Nat.Prime (Finset.range (Nat.succ (Nat.succ n))) = Finset.filter Nat.Prime (Finset.range (Nat.succ n))
Theorem: primesSuccEqPrimesSelf
Proof state before:
n : ℕ
hn : ¬Nat.Prime (Nat.succ n)
⊢ Finset.filter Nat.Prime (Finset.range (Nat.succ (Nat.succ n))) = Finset.filter Nat.Prime (Finset.range (Nat.succ n))
Tactic:
rw [Finset.range_succ]
Proof state after:
n : ℕ
hn : ¬Nat.Prime (Nat.succ n)
⊢ Finset.filter Nat.Prime (insert (n + 1) (Finset.range (n + 1))) = Finset.filter Nat.Prime (Finset.range (Nat.succ n))
Theorem: primesSuccEqPrimesSelf
Proof state before:
n : ℕ
hn : ¬Nat.Prime (Nat.succ n)
⊢ Finset.filter Nat.Prime (insert (n + 1) (Finset.range (n + 1))) = Finset.filter Nat.Prime (Finset.range (Nat.succ n))
Tactic:
simp [Finset.filter_insert]
Proof state after:
n : ℕ
hn : ¬Nat.Prime (Nat.succ n)
⊢ Nat.Prime (n + 1) → False
Theorem: primesSuccEqPrimesSelf
Proof state before:
n : ℕ
hn : ¬Nat.Prime (Nat.succ n)
⊢ Nat.Prime (n + 1) → False
Tactic:
assumption
Proof state after:
no goals
Theorem: caseStrongRecOnOddPrimes
Proof state before:
p : ℕ → Prop
zero : p 0
two : p 2
not_prime : ∀ (n : ℕ), ¬Nat.Prime (Nat.succ n) → (∀ (x : ℕ), x ≤ n → p x) → p (Nat.succ n)
odd_prime : ∀ (n : ℕ), Nat.Prime (Nat.succ (2 * n)) → (∀ (x : ℕ), x ≤ 2 * n → p x) → p (Nat.succ (2 * n))
⊢ ∀ (n : ℕ), p n
Tactic:
intro n
Proof state after:
p : ℕ → Prop
zero : p 0
two : p 2
not_prime : ∀ (n : ℕ), ¬Nat.Prime (Nat.succ n) → (∀ (x : ℕ), x ≤ n → p x) → p (Nat.succ n)
odd_prime : ∀ (n : ℕ), Nat.Prime (Nat.succ (2 * n)) → (∀ (x : ℕ), x ≤ 2 * n → p x) → p (Nat.succ (2 * n))
n : ℕ
⊢ p n
Theorem: caseStrongRecOnOddPrimes
Proof state before:
p : ℕ → Prop
zero : p 0
two : p 2
not_prime : ∀ (n : ℕ), ¬Nat.Prime (Nat.succ n) → (∀ (x : ℕ), x ≤ n → p x) → p (Nat.succ n)
odd_prime : ∀ (n : ℕ), Nat.Prime (Nat.succ (2 * n)) → (∀ (x : ℕ), x ≤ 2 * n → p x) → p (Nat.succ (2 * n))
n : ℕ
⊢ p n
Tactic:
induction n using Nat.caseStrongInductionOn with
| zero => exact zero
| ind k h_ind =>
  cases dec_em (Nat.Prime k.succ) with
  | inr hk_prime =>
    apply not_prime _ hk_prime
    exact h_ind
  | inl hk_prime =>
    cases Nat.Prime.eq_two_or_odd' hk_prime with
    | inl hk_two => rw [hk_two]; exact two
    | inr hk_two =>
      cases hk_two with
      | intro m hm =>
        simp [Nat.add_one] at hm
        simp [hm] at *
        apply odd_prime _ hk_prime h_ind
Proof state after:
no goals
Theorem: caseStrongRecOnOddPrimes
Proof state before:
case zero
p : ℕ → Prop
zero : p 0
two : p 2
not_prime : ∀ (n : ℕ), ¬Nat.Prime (Nat.succ n) → (∀ (x : ℕ), x ≤ n → p x) → p (Nat.succ n)
odd_prime : ∀ (n : ℕ), Nat.Prime (Nat.succ (2 * n)) → (∀ (x : ℕ), x ≤ 2 * n → p x) → p (Nat.succ (2 * n))
⊢ p 0
Tactic:
exact zero
Proof state after:
no goals
Theorem: caseStrongRecOnOddPrimes
Proof state before:
case ind
p : ℕ → Prop
zero : p 0
two : p 2
not_prime : ∀ (n : ℕ), ¬Nat.Prime (Nat.succ n) → (∀ (x : ℕ), x ≤ n → p x) → p (Nat.succ n)
odd_prime : ∀ (n : ℕ), Nat.Prime (Nat.succ (2 * n)) → (∀ (x : ℕ), x ≤ 2 * n → p x) → p (Nat.succ (2 * n))
k : ℕ
h_ind : ∀ (m : ℕ), m ≤ k → p m
⊢ p (Nat.succ k)
Tactic:
cases dec_em (Nat.Prime k.succ) with
| inr hk_prime =>
  apply not_prime _ hk_prime
  exact h_ind
| inl hk_prime =>
  cases Nat.Prime.eq_two_or_odd' hk_prime with
  | inl hk_two => rw [hk_two]; exact two
  | inr hk_two =>
    cases hk_two with
    | intro m hm =>
      simp [Nat.add_one] at hm
      simp [hm] at *
      apply odd_prime _ hk_prime h_ind
Proof state after:
no goals
Theorem: caseStrongRecOnOddPrimes
Proof state before:
case ind.inr
p : ℕ → Prop
zero : p 0
two : p 2
not_prime : ∀ (n : ℕ), ¬Nat.Prime (Nat.succ n) → (∀ (x : ℕ), x ≤ n → p x) → p (Nat.succ n)
odd_prime : ∀ (n : ℕ), Nat.Prime (Nat.succ (2 * n)) → (∀ (x : ℕ), x ≤ 2 * n → p x) → p (Nat.succ (2 * n))
k : ℕ
h_ind : ∀ (m : ℕ), m ≤ k → p m
hk_prime : ¬Nat.Prime (Nat.succ k)
⊢ p (Nat.succ k)
Tactic:
apply not_prime _ hk_prime
Proof state after:
case ind.inr
p : ℕ → Prop
zero : p 0
two : p 2
not_prime : ∀ (n : ℕ), ¬Nat.Prime (Nat.succ n) → (∀ (x : ℕ), x ≤ n → p x) → p (Nat.succ n)
odd_prime : ∀ (n : ℕ), Nat.Prime (Nat.succ (2 * n)) → (∀ (x : ℕ), x ≤ 2 * n → p x) → p (Nat.succ (2 * n))
k : ℕ
h_ind : ∀ (m : ℕ), m ≤ k → p m
hk_prime : ¬Nat.Prime (Nat.succ k)
⊢ ∀ (x : ℕ), x ≤ k → p x
Theorem: caseStrongRecOnOddPrimes
Proof state before:
case ind.inr
p : ℕ → Prop
zero : p 0
two : p 2
not_prime : ∀ (n : ℕ), ¬Nat.Prime (Nat.succ n) → (∀ (x : ℕ), x ≤ n → p x) → p (Nat.succ n)
odd_prime : ∀ (n : ℕ), Nat.Prime (Nat.succ (2 * n)) → (∀ (x : ℕ), x ≤ 2 * n → p x) → p (Nat.succ (2 * n))
k : ℕ
h_ind : ∀ (m : ℕ), m ≤ k → p m
hk_prime : ¬Nat.Prime (Nat.succ k)
⊢ ∀ (x : ℕ), x ≤ k → p x
Tactic:
exact h_ind
Proof state after:
no goals
Theorem: caseStrongRecOnOddPrimes
Proof state before:
case ind.inl
p : ℕ → Prop
zero : p 0
two : p 2
not_prime : ∀ (n : ℕ), ¬Nat.Prime (Nat.succ n) → (∀ (x : ℕ), x ≤ n → p x) → p (Nat.succ n)
odd_prime : ∀ (n : ℕ), Nat.Prime (Nat.succ (2 * n)) → (∀ (x : ℕ), x ≤ 2 * n → p x) → p (Nat.succ (2 * n))
k : ℕ
h_ind : ∀ (m : ℕ), m ≤ k → p m
hk_prime : Nat.Prime (Nat.succ k)
⊢ p (Nat.succ k)
Tactic:
cases Nat.Prime.eq_two_or_odd' hk_prime with
| inl hk_two => rw [hk_two]; exact two
| inr hk_two =>
  cases hk_two with
  | intro m hm =>
    simp [Nat.add_one] at hm
    simp [hm] at *
    apply odd_prime _ hk_prime h_ind
Proof state after:
no goals
Theorem: caseStrongRecOnOddPrimes
Proof state before:
case ind.inl.inl
p : ℕ → Prop
zero : p 0
two : p 2
not_prime : ∀ (n : ℕ), ¬Nat.Prime (Nat.succ n) → (∀ (x : ℕ), x ≤ n → p x) → p (Nat.succ n)
odd_prime : ∀ (n : ℕ), Nat.Prime (Nat.succ (2 * n)) → (∀ (x : ℕ), x ≤ 2 * n → p x) → p (Nat.succ (2 * n))
k : ℕ
h_ind : ∀ (m : ℕ), m ≤ k → p m
hk_prime : Nat.Prime (Nat.succ k)
hk_two : Nat.succ k = 2
⊢ p (Nat.succ k)
Tactic:
rw [hk_two]
Proof state after:
case ind.inl.inl
p : ℕ → Prop
zero : p 0
two : p 2
not_prime : ∀ (n : ℕ), ¬Nat.Prime (Nat.succ n) → (∀ (x : ℕ), x ≤ n → p x) → p (Nat.succ n)
odd_prime : ∀ (n : ℕ), Nat.Prime (Nat.succ (2 * n)) → (∀ (x : ℕ), x ≤ 2 * n → p x) → p (Nat.succ (2 * n))
k : ℕ
h_ind : ∀ (m : ℕ), m ≤ k → p m
hk_prime : Nat.Prime (Nat.succ k)
hk_two : Nat.succ k = 2
⊢ p 2
Theorem: caseStrongRecOnOddPrimes
Proof state before:
case ind.inl.inl
p : ℕ → Prop
zero : p 0
two : p 2
not_prime : ∀ (n : ℕ), ¬Nat.Prime (Nat.succ n) → (∀ (x : ℕ), x ≤ n → p x) → p (Nat.succ n)
odd_prime : ∀ (n : ℕ), Nat.Prime (Nat.succ (2 * n)) → (∀ (x : ℕ), x ≤ 2 * n → p x) → p (Nat.succ (2 * n))
k : ℕ
h_ind : ∀ (m : ℕ), m ≤ k → p m
hk_prime : Nat.Prime (Nat.succ k)
hk_two : Nat.succ k = 2
⊢ p 2
Tactic:
exact two
Proof state after:
no goals
Theorem: caseStrongRecOnOddPrimes
Proof state before:
case ind.inl.inr
p : ℕ → Prop
zero : p 0
two : p 2
not_prime : ∀ (n : ℕ), ¬Nat.Prime (Nat.succ n) → (∀ (x : ℕ), x ≤ n → p x) → p (Nat.succ n)
odd_prime : ∀ (n : ℕ), Nat.Prime (Nat.succ (2 * n)) → (∀ (x : ℕ), x ≤ 2 * n → p x) → p (Nat.succ (2 * n))
k : ℕ
h_ind : ∀ (m : ℕ), m ≤ k → p m
hk_prime : Nat.Prime (Nat.succ k)
hk_two : Odd (Nat.succ k)
⊢ p (Nat.succ k)
Tactic:
cases hk_two with
| intro m hm =>
  simp [Nat.add_one] at hm
  simp [hm] at *
  apply odd_prime _ hk_prime h_ind
Proof state after:
no goals
Theorem: caseStrongRecOnOddPrimes
Proof state before:
case ind.inl.inr.intro
p : ℕ → Prop
zero : p 0
two : p 2
not_prime : ∀ (n : ℕ), ¬Nat.Prime (Nat.succ n) → (∀ (x : ℕ), x ≤ n → p x) → p (Nat.succ n)
odd_prime : ∀ (n : ℕ), Nat.Prime (Nat.succ (2 * n)) → (∀ (x : ℕ), x ≤ 2 * n → p x) → p (Nat.succ (2 * n))
k : ℕ
h_ind : ∀ (m : ℕ), m ≤ k → p m
hk_prime : Nat.Prime (Nat.succ k)
m : ℕ
hm : Nat.succ k = 2 * m + 1
⊢ p (Nat.succ k)
Tactic:
simp [Nat.add_one] at hm
Proof state after:
case ind.inl.inr.intro
p : ℕ → Prop
zero : p 0
two : p 2
not_prime : ∀ (n : ℕ), ¬Nat.Prime (Nat.succ n) → (∀ (x : ℕ), x ≤ n → p x) → p (Nat.succ n)
odd_prime : ∀ (n : ℕ), Nat.Prime (Nat.succ (2 * n)) → (∀ (x : ℕ), x ≤ 2 * n → p x) → p (Nat.succ (2 * n))
k : ℕ
h_ind : ∀ (m : ℕ), m ≤ k → p m
hk_prime : Nat.Prime (Nat.succ k)
m : ℕ
hm : k = 2 * m
⊢ p (Nat.succ k)