Theorem: landauTrick (FromTheBook/Ch02/Bertrand/LandauTrick.lean)

State before:
n : ℕ
hn_pos : 0 < n
hn_lt : n ≤ 4000
⊢ ∃ p, p ∈ Set.Ioc n (2 * n) ∧ Nat.Prime p
Tactic:
have hp : n ∈ Set.Icc 1 4000 → ∃ p, p ∈ nums ∧ p ∈ Set.Ioc n (2*n)
State after:
case hp
n : ℕ
hn_pos : 0 < n
hn_lt : n ≤ 4000
⊢ n ∈ Set.Icc 1 4000 → ∃ p, p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)

n : ℕ
hn_pos : 0 < n
hn_lt : n ≤ 4000
hp : n ∈ Set.Icc 1 4000 → ∃ p, p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)
⊢ ∃ p, p ∈ Set.Ioc n (2 * n) ∧ Nat.Prime p

State before:
case hp
n : ℕ
hn_pos : 0 < n
hn_lt : n ≤ 4000
⊢ n ∈ Set.Icc 1 4000 → ∃ p, p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)

n : ℕ
hn_pos : 0 < n
hn_lt : n ≤ 4000
hp : n ∈ Set.Icc 1 4000 → ∃ p, p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)
⊢ ∃ p, p ∈ Set.Ioc n (2 * n) ∧ Nat.Prime p
Tactic:
. apply existsOfSlowMono <;> simp [nums]
State after:
n : ℕ
hn_pos : 0 < n
hn_lt : n ≤ 4000
hp : n ∈ Set.Icc 1 4000 → ∃ p, p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)
⊢ ∃ p, p ∈ Set.Ioc n (2 * n) ∧ Nat.Prime p

State before:
n : ℕ
hn_pos : 0 < n
hn_lt : n ≤ 4000
hp : n ∈ Set.Icc 1 4000 → ∃ p, p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)
⊢ ∃ p, p ∈ Set.Ioc n (2 * n) ∧ Nat.Prime p
Tactic:
have hp : ∃ p, p ∈ nums ∧ p ∈ Set.Ioc n (2*n)
State after:
case hp
n : ℕ
hn_pos : 0 < n
hn_lt : n ≤ 4000
hp : n ∈ Set.Icc 1 4000 → ∃ p, p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)
⊢ ∃ p, p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)

n : ℕ
hn_pos : 0 < n
hn_lt : n ≤ 4000
hp✝ : n ∈ Set.Icc 1 4000 → ∃ p, p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)
hp : ∃ p, p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)
⊢ ∃ p, p ∈ Set.Ioc n (2 * n) ∧ Nat.Prime p

State before:
case hp
n : ℕ
hn_pos : 0 < n
hn_lt : n ≤ 4000
hp : n ∈ Set.Icc 1 4000 → ∃ p, p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)
⊢ ∃ p, p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)

n : ℕ
hn_pos : 0 < n
hn_lt : n ≤ 4000
hp✝ : n ∈ Set.Icc 1 4000 → ∃ p, p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)
hp : ∃ p, p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)
⊢ ∃ p, p ∈ Set.Ioc n (2 * n) ∧ Nat.Prime p
Tactic:
. apply hp
  apply And.intro <;> linarith
State after:
n : ℕ
hn_pos : 0 < n
hn_lt : n ≤ 4000
hp✝ : n ∈ Set.Icc 1 4000 → ∃ p, p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)
hp : ∃ p, p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)
⊢ ∃ p, p ∈ Set.Ioc n (2 * n) ∧ Nat.Prime p

State before:
n : ℕ
hn_pos : 0 < n
hn_lt : n ≤ 4000
hp✝ : n ∈ Set.Icc 1 4000 → ∃ p, p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)
hp : ∃ p, p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)
⊢ ∃ p, p ∈ Set.Ioc n (2 * n) ∧ Nat.Prime p
Tactic:
cases hp with
| intro p hp =>
  exists p
  apply And.intro hp.right
  refine List.all₂_iff_forall.mp ?_ p hp.left
  exact allPrimeNums
State after:
no goals

State before:
case hp
n : ℕ
hn_pos : 0 < n
hn_lt : n ≤ 4000
⊢ n ∈ Set.Icc 1 4000 → ∃ p, p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)
Tactic:
apply existsOfSlowMono <;> simp [nums]
State after:
no goals

State before:
case hp
n : ℕ
hn_pos : 0 < n
hn_lt : n ≤ 4000
hp : n ∈ Set.Icc 1 4000 → ∃ p, p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)
⊢ ∃ p, p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)
Tactic:
apply hp
State after:
case hp
n : ℕ
hn_pos : 0 < n
hn_lt : n ≤ 4000
hp : n ∈ Set.Icc 1 4000 → ∃ p, p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)
⊢ n ∈ Set.Icc 1 4000

State before:
case hp
n : ℕ
hn_pos : 0 < n
hn_lt : n ≤ 4000
hp : n ∈ Set.Icc 1 4000 → ∃ p, p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)
⊢ n ∈ Set.Icc 1 4000
Tactic:
apply And.intro <;> linarith
State after:
no goals

State before:
case intro
n : ℕ
hn_pos : 0 < n
hn_lt : n ≤ 4000
hp✝ : n ∈ Set.Icc 1 4000 → ∃ p, p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)
p : ℕ
hp : p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)
⊢ ∃ p, p ∈ Set.Ioc n (2 * n) ∧ Nat.Prime p
Tactic:
exists p
State after:
case intro
n : ℕ
hn_pos : 0 < n
hn_lt : n ≤ 4000
hp✝ : n ∈ Set.Icc 1 4000 → ∃ p, p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)
p : ℕ
hp : p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)
⊢ p ∈ Set.Ioc n (2 * n) ∧ Nat.Prime p

State before:
case intro
n : ℕ
hn_pos : 0 < n
hn_lt : n ≤ 4000
hp✝ : n ∈ Set.Icc 1 4000 → ∃ p, p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)
p : ℕ
hp : p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)
⊢ p ∈ Set.Ioc n (2 * n) ∧ Nat.Prime p
Tactic:
apply And.intro hp.right
State after:
case intro
n : ℕ
hn_pos : 0 < n
hn_lt : n ≤ 4000
hp✝ : n ∈ Set.Icc 1 4000 → ∃ p, p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)
p : ℕ
hp : p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)
⊢ Nat.Prime p

State before:
case intro
n : ℕ
hn_pos : 0 < n
hn_lt : n ≤ 4000
hp✝ : n ∈ Set.Icc 1 4000 → ∃ p, p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)
p : ℕ
hp : p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)
⊢ Nat.Prime p
Tactic:
refine List.all₂_iff_forall.mp ?_ p hp.left
State after:
case intro
n : ℕ
hn_pos : 0 < n
hn_lt : n ≤ 4000
hp✝ : n ∈ Set.Icc 1 4000 → ∃ p, p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)
p : ℕ
hp : p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)
⊢ List.All₂ Nat.Prime nums

State before:
case intro
n : ℕ
hn_pos : 0 < n
hn_lt : n ≤ 4000
hp✝ : n ∈ Set.Icc 1 4000 → ∃ p, p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)
p : ℕ
hp : p ∈ nums ∧ p ∈ Set.Ioc n (2 * n)
⊢ List.All₂ Nat.Prime nums
Tactic:
exact allPrimeNums
State after:
no goals