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

State before:
n : ℕ
h : 2 ≤ n
⊢ ∃ p, Nat.Prime p ∧ p ∣ n
Tactic:
by_cases np : n.Prime
State after:
case pos
n : ℕ
h : 2 ≤ n
np : Nat.Prime n
⊢ ∃ p, Nat.Prime p ∧ p ∣ n

case neg
n : ℕ
h : 2 ≤ n
np : ¬Nat.Prime n
⊢ ∃ p, Nat.Prime p ∧ p ∣ n

State before:
case neg
n : ℕ
h : 2 ≤ n
np : ¬Nat.Prime n
⊢ ∃ p, Nat.Prime p ∧ p ∣ n
Tactic:
induction' n using Nat.strong_induction_on with n ih
State after:
case neg.h
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬Nat.Prime m → ∃ p, Nat.Prime p ∧ p ∣ m
h : 2 ≤ n
np : ¬Nat.Prime n
⊢ ∃ p, Nat.Prime p ∧ p ∣ n

State before:
case neg.h
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬Nat.Prime m → ∃ p, Nat.Prime p ∧ p ∣ m
h : 2 ≤ n
np : ¬Nat.Prime n
⊢ ∃ p, Nat.Prime p ∧ p ∣ n
Tactic:
rw [Nat.prime_def_lt] at np
State after:
case neg.h
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬Nat.Prime m → ∃ p, Nat.Prime p ∧ p ∣ m
h : 2 ≤ n
np : ¬(2 ≤ n ∧ ∀ m < n, m ∣ n → m = 1)
⊢ ∃ p, Nat.Prime p ∧ p ∣ n

State before:
case neg.h
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬Nat.Prime m → ∃ p, Nat.Prime p ∧ p ∣ m
h : 2 ≤ n
np : ¬(2 ≤ n ∧ ∀ m < n, m ∣ n → m = 1)
⊢ ∃ p, Nat.Prime p ∧ p ∣ n
Tactic:
push_neg at np
State after:
case neg.h
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬Nat.Prime m → ∃ p, Nat.Prime p ∧ p ∣ m
h : 2 ≤ n
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
⊢ ∃ p, Nat.Prime p ∧ p ∣ n

State before:
case neg.h
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬Nat.Prime m → ∃ p, Nat.Prime p ∧ p ∣ m
h : 2 ≤ n
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
⊢ ∃ p, Nat.Prime p ∧ p ∣ n
Tactic:
rcases np h with ⟨m, mltn, mdvdn, mne1⟩
State after:
case neg.h.intro.intro.intro
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬Nat.Prime m → ∃ p, Nat.Prime p ∧ p ∣ m
h : 2 ≤ n
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
⊢ ∃ p, Nat.Prime p ∧ p ∣ n

State before:
case neg.h.intro.intro.intro
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬Nat.Prime m → ∃ p, Nat.Prime p ∧ p ∣ m
h : 2 ≤ n
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
⊢ ∃ p, Nat.Prime p ∧ p ∣ n
Tactic:
have : m ≠ 0 := by
  intro mz
  rw [mz, zero_dvd_iff] at mdvdn
  linarith
State after:
case neg.h.intro.intro.intro
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬Nat.Prime m → ∃ p, Nat.Prime p ∧ p ∣ m
h : 2 ≤ n
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
this : m ≠ 0
⊢ ∃ p, Nat.Prime p ∧ p ∣ n

State before:
case neg.h.intro.intro.intro
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬Nat.Prime m → ∃ p, Nat.Prime p ∧ p ∣ m
h : 2 ≤ n
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
this : m ≠ 0
⊢ ∃ p, Nat.Prime p ∧ p ∣ n
Tactic:
have mgt2 : 2 ≤ m := two_le this mne1
State after:
case neg.h.intro.intro.intro
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬Nat.Prime m → ∃ p, Nat.Prime p ∧ p ∣ m
h : 2 ≤ n
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
this : m ≠ 0
mgt2 : 2 ≤ m
⊢ ∃ p, Nat.Prime p ∧ p ∣ n

State before:
case neg.h.intro.intro.intro
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬Nat.Prime m → ∃ p, Nat.Prime p ∧ p ∣ m
h : 2 ≤ n
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
this : m ≠ 0
mgt2 : 2 ≤ m
⊢ ∃ p, Nat.Prime p ∧ p ∣ n
Tactic:
by_cases mp : m.Prime
State after:
case pos
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬Nat.Prime m → ∃ p, Nat.Prime p ∧ p ∣ m
h : 2 ≤ n
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
this : m ≠ 0
mgt2 : 2 ≤ m
mp : Nat.Prime m
⊢ ∃ p, Nat.Prime p ∧ p ∣ n

case neg
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬Nat.Prime m → ∃ p, Nat.Prime p ∧ p ∣ m
h : 2 ≤ n
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
this : m ≠ 0
mgt2 : 2 ≤ m
mp : ¬Nat.Prime m
⊢ ∃ p, Nat.Prime p ∧ p ∣ n

State before:
case neg
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬Nat.Prime m → ∃ p, Nat.Prime p ∧ p ∣ m
h : 2 ≤ n
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
this : m ≠ 0
mgt2 : 2 ≤ m
mp : ¬Nat.Prime m
⊢ ∃ p, Nat.Prime p ∧ p ∣ n
Tactic:
. rcases ih m mltn mgt2 mp with ⟨p, pp, pdvd⟩
  use p, pp
  apply pdvd.trans mdvdn
State after:
no goals

State before:
case pos
n : ℕ
h : 2 ≤ n
np : Nat.Prime n
⊢ ∃ p, Nat.Prime p ∧ p ∣ n
Tactic:
use n, np
State after:
no goals

State before:
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬Nat.Prime m → ∃ p, Nat.Prime p ∧ p ∣ m
h : 2 ≤ n
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
⊢ m ≠ 0
Tactic:
intro mz
State after:
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬Nat.Prime m → ∃ p, Nat.Prime p ∧ p ∣ m
h : 2 ≤ n
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
mz : m = 0
⊢ False

State before:
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬Nat.Prime m → ∃ p, Nat.Prime p ∧ p ∣ m
h : 2 ≤ n
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
mz : m = 0
⊢ False
Tactic:
rw [mz, zero_dvd_iff] at mdvdn
State after:
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬Nat.Prime m → ∃ p, Nat.Prime p ∧ p ∣ m
h : 2 ≤ n
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : n = 0
mne1 : m ≠ 1
mz : m = 0
⊢ False

State before:
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬Nat.Prime m → ∃ p, Nat.Prime p ∧ p ∣ m
h : 2 ≤ n
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : n = 0
mne1 : m ≠ 1
mz : m = 0
⊢ False
Tactic:
linarith
State after:
no goals

State before:
case pos
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬Nat.Prime m → ∃ p, Nat.Prime p ∧ p ∣ m
h : 2 ≤ n
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
this : m ≠ 0
mgt2 : 2 ≤ m
mp : Nat.Prime m
⊢ ∃ p, Nat.Prime p ∧ p ∣ n
Tactic:
use m, mp
State after:
no goals

State before:
case neg
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬Nat.Prime m → ∃ p, Nat.Prime p ∧ p ∣ m
h : 2 ≤ n
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
this : m ≠ 0
mgt2 : 2 ≤ m
mp : ¬Nat.Prime m
⊢ ∃ p, Nat.Prime p ∧ p ∣ n
Tactic:
rcases ih m mltn mgt2 mp with ⟨p, pp, pdvd⟩
State after:
case neg.intro.intro
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬Nat.Prime m → ∃ p, Nat.Prime p ∧ p ∣ m
h : 2 ≤ n
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
this : m ≠ 0
mgt2 : 2 ≤ m
mp : ¬Nat.Prime m
p : ℕ
pp : Nat.Prime p
pdvd : p ∣ m
⊢ ∃ p, Nat.Prime p ∧ p ∣ n

State before:
case neg.intro.intro
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬Nat.Prime m → ∃ p, Nat.Prime p ∧ p ∣ m
h : 2 ≤ n
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
this : m ≠ 0
mgt2 : 2 ≤ m
mp : ¬Nat.Prime m
p : ℕ
pp : Nat.Prime p
pdvd : p ∣ m
⊢ ∃ p, Nat.Prime p ∧ p ∣ n
Tactic:
use p, pp
State after:
case right
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬Nat.Prime m → ∃ p, Nat.Prime p ∧ p ∣ m
h : 2 ≤ n
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
this : m ≠ 0
mgt2 : 2 ≤ m
mp : ¬Nat.Prime m
p : ℕ
pp : Nat.Prime p
pdvd : p ∣ m
⊢ p ∣ n

State before:
case right
n : ℕ
ih : ∀ m < n, 2 ≤ m → ¬Nat.Prime m → ∃ p, Nat.Prime p ∧ p ∣ m
h : 2 ≤ n
np : 2 ≤ n → ∃ m < n, m ∣ n ∧ m ≠ 1
m : ℕ
mltn : m < n
mdvdn : m ∣ n
mne1 : m ≠ 1
this : m ≠ 0
mgt2 : 2 ≤ m
mp : ¬Nat.Prime m
p : ℕ
pp : Nat.Prime p
pdvd : p ∣ m
⊢ p ∣ n
Tactic:
apply pdvd.trans mdvdn
State after:
no goals