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

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

State before:
n : ℕ
⊢ ∃ p > n, Nat.Prime p
Tactic:
have : 2 ≤ Nat.factorial (n + 1) + 1 := by
  sorry
State after:
n : ℕ
this : 2 ≤ Nat.factorial (n + 1) + 1
⊢ ∃ p > n, Nat.Prime p

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

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

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

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

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

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

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

State before:
n : ℕ
⊢ 2 ≤ Nat.factorial (n + 1) + 1
Tactic:
sorry
State after:
no goals

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

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