Theorem: infinitude_of_primes (LoVe/Lectures/LoVe00_Preface_Demo.lean)

State before:
⊢ ∀ (N : ℕ), ∃ p, p ≥ N ∧ Nat.Prime p
Tactic:
intro M
State after:
M : ℕ
⊢ ∃ p, p ≥ M ∧ Nat.Prime p

State before:
M : ℕ
⊢ ∃ p, p ≥ M ∧ Nat.Prime p
Tactic:
let F := M ! + 1
State after:
M : ℕ
F : ℕ := M ! + 1
⊢ ∃ p, p ≥ M ∧ Nat.Prime p

State before:
M : ℕ
F : ℕ := M ! + 1
⊢ ∃ p, p ≥ M ∧ Nat.Prime p
Tactic:
let q := minFac F
State after:
M : ℕ
F : ℕ := M ! + 1
q : ℕ := minFac F
⊢ ∃ p, p ≥ M ∧ Nat.Prime p

State before:
M : ℕ
F : ℕ := M ! + 1
q : ℕ := minFac F
⊢ ∃ p, p ≥ M ∧ Nat.Prime p
Tactic:
use q
State after:
case h
M : ℕ
F : ℕ := M ! + 1
q : ℕ := minFac F
⊢ q ≥ M ∧ Nat.Prime q

State before:
case h
M : ℕ
F : ℕ := M ! + 1
q : ℕ := minFac F
⊢ q ≥ M ∧ Nat.Prime q
Tactic:
have qPrime : Nat.Prime q
State after:
case qPrime
M : ℕ
F : ℕ := M ! + 1
q : ℕ := minFac F
⊢ Nat.Prime q

case h
M : ℕ
F : ℕ := M ! + 1
q : ℕ := minFac F
qPrime : Nat.Prime q
⊢ q ≥ M ∧ Nat.Prime q

State before:
case qPrime
M : ℕ
F : ℕ := M ! + 1
q : ℕ := minFac F
⊢ Nat.Prime q

case h
M : ℕ
F : ℕ := M ! + 1
q : ℕ := minFac F
qPrime : Nat.Prime q
⊢ q ≥ M ∧ Nat.Prime q
Tactic:
{ refine' minFac_prime _
  have hn : M ! > 0 := factorial_pos M 
  linarith }
State after:
case h
M : ℕ
F : ℕ := M ! + 1
q : ℕ := minFac F
qPrime : Nat.Prime q
⊢ q ≥ M ∧ Nat.Prime q

State before:
case h
M : ℕ
F : ℕ := M ! + 1
q : ℕ := minFac F
qPrime : Nat.Prime q
⊢ q ≥ M ∧ Nat.Prime q
Tactic:
apply And.intro
State after:
case h.left
M : ℕ
F : ℕ := M ! + 1
q : ℕ := minFac F
qPrime : Nat.Prime q
⊢ q ≥ M

case h.right
M : ℕ
F : ℕ := M ! + 1
q : ℕ := minFac F
qPrime : Nat.Prime q
⊢ Nat.Prime q

State before:
case h.left
M : ℕ
F : ℕ := M ! + 1
q : ℕ := minFac F
qPrime : Nat.Prime q
⊢ q ≥ M

case h.right
M : ℕ
F : ℕ := M ! + 1
q : ℕ := minFac F
qPrime : Nat.Prime q
⊢ Nat.Prime q
Tactic:
{ by_contra hqM
  have h1 : q ∣ M ! + 1 := minFac_dvd F
  have hqM2 : q ≤ M := by linarith
  have hqM3 : q ∣ M ! := Iff.mpr (Prime.dvd_factorial qPrime) hqM2
  have hq1 : q ∣ 1 := Iff.mp (Nat.dvd_add_right hqM3) h1
  apply Nat.Prime.not_dvd_one qPrime hq1
}
State after:
case h.right
M : ℕ
F : ℕ := M ! + 1
q : ℕ := minFac F
qPrime : Nat.Prime q
⊢ Nat.Prime q

State before:
case h.right
M : ℕ
F : ℕ := M ! + 1
q : ℕ := minFac F
qPrime : Nat.Prime q
⊢ Nat.Prime q
Tactic:
{ assumption }
State after:
no goals

State before:
case qPrime
M : ℕ
F : ℕ := M ! + 1
q : ℕ := minFac F
⊢ Nat.Prime q
Tactic:
refine' minFac_prime _
State after:
case qPrime
M : ℕ
F : ℕ := M ! + 1
q : ℕ := minFac F
⊢ F ≠ 1

State before:
case qPrime
M : ℕ
F : ℕ := M ! + 1
q : ℕ := minFac F
⊢ F ≠ 1
Tactic:
have hn : M ! > 0 := factorial_pos M
State after:
case qPrime
M : ℕ
F : ℕ := M ! + 1
q : ℕ := minFac F
hn : M ! > 0
⊢ F ≠ 1

State before:
case qPrime
M : ℕ
F : ℕ := M ! + 1
q : ℕ := minFac F
hn : M ! > 0
⊢ F ≠ 1
Tactic:
linarith
State after:
no goals

State before:
case h.left
M : ℕ
F : ℕ := M ! + 1
q : ℕ := minFac F
qPrime : Nat.Prime q
⊢ q ≥ M
Tactic:
by_contra hqM
State after:
case h.left
M : ℕ
F : ℕ := M ! + 1
q : ℕ := minFac F
qPrime : Nat.Prime q
hqM : ¬q ≥ M
⊢ False

State before:
case h.left
M : ℕ
F : ℕ := M ! + 1
q : ℕ := minFac F
qPrime : Nat.Prime q
hqM : ¬q ≥ M
⊢ False
Tactic:
have h1 : q ∣ M ! + 1 := minFac_dvd F
State after:
case h.left
M : ℕ
F : ℕ := M ! + 1
q : ℕ := minFac F
qPrime : Nat.Prime q
hqM : ¬q ≥ M
h1 : q ∣ M ! + 1
⊢ False

State before:
case h.left
M : ℕ
F : ℕ := M ! + 1
q : ℕ := minFac F
qPrime : Nat.Prime q
hqM : ¬q ≥ M
h1 : q ∣ M ! + 1
⊢ False
Tactic:
have hqM2 : q ≤ M := by linarith
State after:
case h.left
M : ℕ
F : ℕ := M ! + 1
q : ℕ := minFac F
qPrime : Nat.Prime q
hqM : ¬q ≥ M
h1 : q ∣ M ! + 1
hqM2 : q ≤ M
⊢ False

State before:
case h.left
M : ℕ
F : ℕ := M ! + 1
q : ℕ := minFac F
qPrime : Nat.Prime q
hqM : ¬q ≥ M
h1 : q ∣ M ! + 1
hqM2 : q ≤ M
⊢ False
Tactic:
have hqM3 : q ∣ M ! := Iff.mpr (Prime.dvd_factorial qPrime) hqM2
State after:
case h.left
M : ℕ
F : ℕ := M ! + 1
q : ℕ := minFac F
qPrime : Nat.Prime q
hqM : ¬q ≥ M
h1 : q ∣ M ! + 1
hqM2 : q ≤ M
hqM3 : q ∣ M !
⊢ False

State before:
case h.left
M : ℕ
F : ℕ := M ! + 1
q : ℕ := minFac F
qPrime : Nat.Prime q
hqM : ¬q ≥ M
h1 : q ∣ M ! + 1
hqM2 : q ≤ M
hqM3 : q ∣ M !
⊢ False
Tactic:
have hq1 : q ∣ 1 := Iff.mp (Nat.dvd_add_right hqM3) h1
State after:
case h.left
M : ℕ
F : ℕ := M ! + 1
q : ℕ := minFac F
qPrime : Nat.Prime q
hqM : ¬q ≥ M
h1 : q ∣ M ! + 1
hqM2 : q ≤ M
hqM3 : q ∣ M !
hq1 : q ∣ 1
⊢ False

State before:
case h.left
M : ℕ
F : ℕ := M ! + 1
q : ℕ := minFac F
qPrime : Nat.Prime q
hqM : ¬q ≥ M
h1 : q ∣ M ! + 1
hqM2 : q ≤ M
hqM3 : q ∣ M !
hq1 : q ∣ 1
⊢ False
Tactic:
apply Nat.Prime.not_dvd_one qPrime hq1
State after:
no goals

State before:
M : ℕ
F : ℕ := M ! + 1
q : ℕ := minFac F
qPrime : Nat.Prime q
hqM : ¬q ≥ M
h1 : q ∣ M ! + 1
⊢ q ≤ M
Tactic:
linarith
State after:
no goals

State before:
case h.right
M : ℕ
F : ℕ := M ! + 1
q : ℕ := minFac F
qPrime : Nat.Prime q
⊢ Nat.Prime q
Tactic:
assumption
State after:
no goals