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

State before:
⊢ ∀ (N : ℕ), biggerPrime N ≥ N
Tactic:
intro M
State after:
M : ℕ
⊢ biggerPrime M ≥ M

State before:
M : ℕ
⊢ biggerPrime M ≥ M
Tactic:
by_contra hqM
State after:
M : ℕ
hqM : ¬biggerPrime M ≥ M
⊢ False

State before:
M : ℕ
hqM : ¬biggerPrime M ≥ M
⊢ False
Tactic:
have h1 : (biggerPrime M) ∣ M ! + 1 := minFac_dvd _
State after:
M : ℕ
hqM : ¬biggerPrime M ≥ M
h1 : biggerPrime M ∣ M ! + 1
⊢ False

State before:
M : ℕ
hqM : ¬biggerPrime M ≥ M
h1 : biggerPrime M ∣ M ! + 1
⊢ False
Tactic:
have hqM2 : biggerPrime M ≤ M := by linarith
State after:
M : ℕ
hqM : ¬biggerPrime M ≥ M
h1 : biggerPrime M ∣ M ! + 1
hqM2 : biggerPrime M ≤ M
⊢ False

State before:
M : ℕ
hqM : ¬biggerPrime M ≥ M
h1 : biggerPrime M ∣ M ! + 1
hqM2 : biggerPrime M ≤ M
⊢ False
Tactic:
have hqM3 : biggerPrime M ∣ M ! :=
  Iff.mpr (Prime.dvd_factorial (biggerPrimeIsPrime _)) hqM2
State after:
M : ℕ
hqM : ¬biggerPrime M ≥ M
h1 : biggerPrime M ∣ M ! + 1
hqM2 : biggerPrime M ≤ M
hqM3 : biggerPrime M ∣ M !
⊢ False

State before:
M : ℕ
hqM : ¬biggerPrime M ≥ M
h1 : biggerPrime M ∣ M ! + 1
hqM2 : biggerPrime M ≤ M
hqM3 : biggerPrime M ∣ M !
⊢ False
Tactic:
have hq1 : biggerPrime M ∣ 1 := Iff.mp (Nat.dvd_add_right hqM3) h1
State after:
M : ℕ
hqM : ¬biggerPrime M ≥ M
h1 : biggerPrime M ∣ M ! + 1
hqM2 : biggerPrime M ≤ M
hqM3 : biggerPrime M ∣ M !
hq1 : biggerPrime M ∣ 1
⊢ False

State before:
M : ℕ
hqM : ¬biggerPrime M ≥ M
h1 : biggerPrime M ∣ M ! + 1
hqM2 : biggerPrime M ≤ M
hqM3 : biggerPrime M ∣ M !
hq1 : biggerPrime M ∣ 1
⊢ False
Tactic:
apply Nat.Prime.not_dvd_one (biggerPrimeIsPrime _) hq1
State after:
no goals

State before:
M : ℕ
hqM : ¬biggerPrime M ≥ M
h1 : biggerPrime M ∣ M ! + 1
⊢ biggerPrime M ≤ M
Tactic:
linarith
State after:
no goals