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

State before:
⊢ ∀ (N : ℕ), Nat.Prime (biggerPrime N)
Tactic:
intro M
State after:
M : ℕ
⊢ Nat.Prime (biggerPrime M)

State before:
M : ℕ
⊢ Nat.Prime (biggerPrime M)
Tactic:
refine' minFac_prime _
State after:
M : ℕ
⊢ M ! + 1 ≠ 1

State before:
M : ℕ
⊢ M ! + 1 ≠ 1
Tactic:
have hn : M ! > 0 := factorial_pos M
State after:
M : ℕ
hn : M ! > 0
⊢ M ! + 1 ≠ 1

State before:
M : ℕ
hn : M ! > 0
⊢ M ! + 1 ≠ 1
Tactic:
linarith
State after:
no goals