Theorem: C05S03.primes_infinite (MIL/C05_Elementary_Number_Theory/S03_Infinitely_Many_Primes.lean)

State before:
⊢ ∀ (n : ℕ), ∃ p > n, p.Prime
Tactic:
intro n
State after:
n : ℕ
⊢ ∃ p > n, p.Prime

State before:
n : ℕ
⊢ ∃ p > n, p.Prime
Tactic:
have : 2 ≤ Nat.factorial (n + 1) + 1 := by
  apply Nat.succ_le_succ
  exact Nat.succ_le_of_lt (Nat.factorial_pos _)
State after:
n : ℕ
this : 2 ≤ (n + 1).factorial + 1
⊢ ∃ p > n, p.Prime

State before:
n : ℕ
this : 2 ≤ (n + 1).factorial + 1
⊢ ∃ p > n, p.Prime
Tactic:
rcases exists_prime_factor this with ⟨p, pp, pdvd⟩
State after:
case intro.intro
n : ℕ
this : 2 ≤ (n + 1).factorial + 1
p : ℕ
pp : p.Prime
pdvd : p ∣ (n + 1).factorial + 1
⊢ ∃ p > n, p.Prime

State before:
case intro.intro
n : ℕ
this : 2 ≤ (n + 1).factorial + 1
p : ℕ
pp : p.Prime
pdvd : p ∣ (n + 1).factorial + 1
⊢ ∃ p > n, p.Prime
Tactic:
refine' ⟨p, _, pp⟩
State after:
case intro.intro
n : ℕ
this : 2 ≤ (n + 1).factorial + 1
p : ℕ
pp : p.Prime
pdvd : p ∣ (n + 1).factorial + 1
⊢ p > n

State before:
case intro.intro
n : ℕ
this : 2 ≤ (n + 1).factorial + 1
p : ℕ
pp : p.Prime
pdvd : p ∣ (n + 1).factorial + 1
⊢ p > n
Tactic:
by_contra ple
State after:
case intro.intro
n : ℕ
this : 2 ≤ (n + 1).factorial + 1
p : ℕ
pp : p.Prime
pdvd : p ∣ (n + 1).factorial + 1
ple : ¬p > n
⊢ False

State before:
case intro.intro
n : ℕ
this : 2 ≤ (n + 1).factorial + 1
p : ℕ
pp : p.Prime
pdvd : p ∣ (n + 1).factorial + 1
ple : ¬p > n
⊢ False
Tactic:
push_neg  at ple
State after:
case intro.intro
n : ℕ
this : 2 ≤ (n + 1).factorial + 1
p : ℕ
pp : p.Prime
pdvd : p ∣ (n + 1).factorial + 1
ple : p ≤ n
⊢ False

State before:
case intro.intro
n : ℕ
this : 2 ≤ (n + 1).factorial + 1
p : ℕ
pp : p.Prime
pdvd : p ∣ (n + 1).factorial + 1
ple : p ≤ n
⊢ False
Tactic:
have : p ∣ Nat.factorial (n + 1) := by
  apply Nat.dvd_factorial
  apply pp.pos
  linarith
State after:
case intro.intro
n : ℕ
this✝ : 2 ≤ (n + 1).factorial + 1
p : ℕ
pp : p.Prime
pdvd : p ∣ (n + 1).factorial + 1
ple : p ≤ n
this : p ∣ (n + 1).factorial
⊢ False

State before:
case intro.intro
n : ℕ
this✝ : 2 ≤ (n + 1).factorial + 1
p : ℕ
pp : p.Prime
pdvd : p ∣ (n + 1).factorial + 1
ple : p ≤ n
this : p ∣ (n + 1).factorial
⊢ False
Tactic:
have : p ∣ 1 := by
  convert Nat.dvd_sub' pdvd this
  simp
State after:
case intro.intro
n : ℕ
this✝¹ : 2 ≤ (n + 1).factorial + 1
p : ℕ
pp : p.Prime
pdvd : p ∣ (n + 1).factorial + 1
ple : p ≤ n
this✝ : p ∣ (n + 1).factorial
this : p ∣ 1
⊢ False

State before:
case intro.intro
n : ℕ
this✝¹ : 2 ≤ (n + 1).factorial + 1
p : ℕ
pp : p.Prime
pdvd : p ∣ (n + 1).factorial + 1
ple : p ≤ n
this✝ : p ∣ (n + 1).factorial
this : p ∣ 1
⊢ False
Tactic:
have := Nat.le_of_dvd zero_lt_one this
State after:
case intro.intro
n : ℕ
this✝² : 2 ≤ (n + 1).factorial + 1
p : ℕ
pp : p.Prime
pdvd : p ∣ (n + 1).factorial + 1
ple : p ≤ n
this✝¹ : p ∣ (n + 1).factorial
this✝ : p ∣ 1
this : p ≤ 1
⊢ False

State before:
case intro.intro
n : ℕ
this✝² : 2 ≤ (n + 1).factorial + 1
p : ℕ
pp : p.Prime
pdvd : p ∣ (n + 1).factorial + 1
ple : p ≤ n
this✝¹ : p ∣ (n + 1).factorial
this✝ : p ∣ 1
this : p ≤ 1
⊢ False
Tactic:
linarith [pp.two_le]
State after:
no goals

State before:
n : ℕ
⊢ 2 ≤ (n + 1).factorial + 1
Tactic:
apply Nat.succ_le_succ
State after:
case a
n : ℕ
⊢ 1 ≤ (n + 1).factorial

State before:
case a
n : ℕ
⊢ 1 ≤ (n + 1).factorial
Tactic:
exact Nat.succ_le_of_lt (Nat.factorial_pos _)
State after:
no goals

State before:
n : ℕ
this : 2 ≤ (n + 1).factorial + 1
p : ℕ
pp : p.Prime
pdvd : p ∣ (n + 1).factorial + 1
ple : p ≤ n
⊢ p ∣ (n + 1).factorial
Tactic:
apply Nat.dvd_factorial
State after:
case a
n : ℕ
this : 2 ≤ (n + 1).factorial + 1
p : ℕ
pp : p.Prime
pdvd : p ∣ (n + 1).factorial + 1
ple : p ≤ n
⊢ 0 < p

case a
n : ℕ
this : 2 ≤ (n + 1).factorial + 1
p : ℕ
pp : p.Prime
pdvd : p ∣ (n + 1).factorial + 1
ple : p ≤ n
⊢ p ≤ n + 1

State before:
case a
n : ℕ
this : 2 ≤ (n + 1).factorial + 1
p : ℕ
pp : p.Prime
pdvd : p ∣ (n + 1).factorial + 1
ple : p ≤ n
⊢ 0 < p

case a
n : ℕ
this : 2 ≤ (n + 1).factorial + 1
p : ℕ
pp : p.Prime
pdvd : p ∣ (n + 1).factorial + 1
ple : p ≤ n
⊢ p ≤ n + 1
Tactic:
apply pp.pos
State after:
case a
n : ℕ
this : 2 ≤ (n + 1).factorial + 1
p : ℕ
pp : p.Prime
pdvd : p ∣ (n + 1).factorial + 1
ple : p ≤ n
⊢ p ≤ n + 1

State before:
case a
n : ℕ
this : 2 ≤ (n + 1).factorial + 1
p : ℕ
pp : p.Prime
pdvd : p ∣ (n + 1).factorial + 1
ple : p ≤ n
⊢ p ≤ n + 1
Tactic:
linarith
State after:
no goals

State before:
n : ℕ
this✝ : 2 ≤ (n + 1).factorial + 1
p : ℕ
pp : p.Prime
pdvd : p ∣ (n + 1).factorial + 1
ple : p ≤ n
this : p ∣ (n + 1).factorial
⊢ p ∣ 1
Tactic:
convert Nat.dvd_sub' pdvd this
State after:
case h.e'_4
n : ℕ
this✝ : 2 ≤ (n + 1).factorial + 1
p : ℕ
pp : p.Prime
pdvd : p ∣ (n + 1).factorial + 1
ple : p ≤ n
this : p ∣ (n + 1).factorial
⊢ 1 = (n + 1).factorial + 1 - (n + 1).factorial

State before:
case h.e'_4
n : ℕ
this✝ : 2 ≤ (n + 1).factorial + 1
p : ℕ
pp : p.Prime
pdvd : p ∣ (n + 1).factorial + 1
ple : p ≤ n
this : p ∣ (n + 1).factorial
⊢ 1 = (n + 1).factorial + 1 - (n + 1).factorial
Tactic:
simp
State after:
no goals