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

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

State before:
N : ℕ
⊢ ∃ p, p ≥ N ∧ Nat.Prime p
Tactic:
use biggerPrime N
State after:
case h
N : ℕ
⊢ biggerPrime N ≥ N ∧ Nat.Prime (biggerPrime N)

State before:
case h
N : ℕ
⊢ biggerPrime N ≥ N ∧ Nat.Prime (biggerPrime N)
Tactic:
apply And.intro
State after:
case h.left
N : ℕ
⊢ biggerPrime N ≥ N

case h.right
N : ℕ
⊢ Nat.Prime (biggerPrime N)

State before:
case h.left
N : ℕ
⊢ biggerPrime N ≥ N

case h.right
N : ℕ
⊢ Nat.Prime (biggerPrime N)
Tactic:
{ exact biggerPrimeIsBigger _ }
State after:
case h.right
N : ℕ
⊢ Nat.Prime (biggerPrime N)

State before:
case h.right
N : ℕ
⊢ Nat.Prime (biggerPrime N)
Tactic:
{ exact biggerPrimeIsPrime _ }
State after:
no goals

State before:
case h.left
N : ℕ
⊢ biggerPrime N ≥ N
Tactic:
exact biggerPrimeIsBigger _
State after:
no goals

State before:
case h.right
N : ℕ
⊢ Nat.Prime (biggerPrime N)
Tactic:
exact biggerPrimeIsPrime _
State after:
no goals