Theorem: existsGap (FromTheBook/Ch02/UnboundedGaps.lean)

State before:
k : ℕ
⊢ ∃ m, ∀ (x : ℕ), x < k → ¬Nat.Prime (m + x)
Tactic:
exists PrimeRange.prod k.succ.succ + 2
State after:
k : ℕ
⊢ ∀ (x : ℕ), x < k → ¬Nat.Prime (PrimeRange.prod (Nat.succ (Nat.succ k)) + 2 + x)

State before:
k : ℕ
⊢ ∀ (x : ℕ), x < k → ¬Nat.Prime (PrimeRange.prod (Nat.succ (Nat.succ k)) + 2 + x)
Tactic:
intros x hx
State after:
k x : ℕ
hx : x < k
⊢ ¬Nat.Prime (PrimeRange.prod (Nat.succ (Nat.succ k)) + 2 + x)

State before:
k x : ℕ
hx : x < k
⊢ ¬Nat.Prime (PrimeRange.prod (Nat.succ (Nat.succ k)) + 2 + x)
Tactic:
rw [add_assoc]
State after:
k x : ℕ
hx : x < k
⊢ ¬Nat.Prime (PrimeRange.prod (Nat.succ (Nat.succ k)) + (2 + x))

State before:
k x : ℕ
hx : x < k
⊢ ¬Nat.Prime (PrimeRange.prod (Nat.succ (Nat.succ k)) + (2 + x))
Tactic:
apply gapAfterProdPrimeRange
State after:
case a
k x : ℕ
hx : x < k
⊢ 2 ≤ 2 + x ∧ 2 + x ≤ Nat.succ k

State before:
case a
k x : ℕ
hx : x < k
⊢ 2 ≤ 2 + x ∧ 2 + x ≤ Nat.succ k
Tactic:
simp
State after:
case a
k x : ℕ
hx : x < k
⊢ 2 + x ≤ Nat.succ k

State before:
case a
k x : ℕ
hx : x < k
⊢ 2 + x ≤ Nat.succ k
Tactic:
linarith
State after:
no goals