Theorem: bertrand (FromTheBook/Ch02/Bertrand/Bertrand.lean)

State before:
n : ℕ
⊢ 0 < n → ∃ p, p ∈ Set.Ioc n (2 * n) ∧ Nat.Prime p
Tactic:
intro hn
State after:
n : ℕ
hn : 0 < n
⊢ ∃ p, p ∈ Set.Ioc n (2 * n) ∧ Nat.Prime p

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
State after:
no goals

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

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

State before:
n : ℕ
hn : 0 < n
hn' : n < 4000
⊢ n ≤ 4000
Tactic:
linarith
State after:
no goals

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
State after:
case inr
n : ℕ
hn : 0 < n
hn' : 4000 ≤ n
h : ¬∃ p, p ∈ Set.Ioc n (2 * n) ∧ Nat.Prime p
⊢ False

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
State after:
case inr
n : ℕ
hn : 0 < n
hn' : 4000 ≤ n
h : ∀ (x : ℕ), n < x → x ≤ 2 * n → ¬Nat.Prime x
⊢ False

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

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
State after:
case inr
n : ℕ
hn : 0 < n
hn' : 4000 ≤ n
h : ∏ p in primes (Finset.Ioc n (2 * n)), p = 1
⊢ False

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

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

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

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'
State after:
case inr
n : ℕ
hn : 0 < n
hn' : 4000 ≤ n
h' : 4 ^ (↑n / 3) ≤ (2 * ↑n) ^ (1 + Real.sqrt (2 * ↑n))
⊢ False

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

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

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

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
State after:
case inr
n : ℕ
hn : 0 < n
hn' : 4000 ≤ n
h' : 4 ^ ↑n < 2 ^ (20 * (2 * ↑n) ^ (2 / 3))
⊢ False

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'
State after:
case inr
n : ℕ
hn : 0 < n
hn' : 4000 ≤ n
h' : ↑n < 4000
⊢ False

State before:
case inr
n : ℕ
hn : 0 < n
hn' : 4000 ≤ n
h' : ↑n < 4000
⊢ False
Tactic:
norm_cast at h'
State after:
case inr
n : ℕ
hn : 0 < n
hn' : 4000 ≤ n
h' : n < 4000
⊢ False

State before:
case inr
n : ℕ
hn : 0 < n
hn' : 4000 ≤ n
h' : n < 4000
⊢ False
Tactic:
linarith
State after:
no goals

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

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

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

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

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

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
State after:
no goals

State before:
n : ℕ
hn : 0 < n
hn' : 4000 ≤ n
h : ∏ p in primes (Finset.Ioc n (2 * n)), p = 1
⊢ 2 < n
Tactic:
linarith
State after:
no goals

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
State after:
no goals

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

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

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
State after:
no goals

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
State after:
no goals

State before:
n : ℕ
hn : 0 < n
hn' : 4000 ≤ n
h' : 4 ^ ↑n < 2 ^ (20 * (2 * ↑n) ^ (2 / 3))
⊢ 0 < ↑n
Tactic:
norm_cast
State after:
no goals