Infinitely Many Primes

import Mathlib

-- There are infinitely many prime numbers.
theorem inf_primes : ∀ n : ℕ, ∃ p : ℕ, n < p ∧ Nat.Prime p := fun n =>
  (Nat.exists_infinite_primes (n + 1)).elim fun p hp =>
    ⟨p, Nat.lt_of_add_one_le hp.left, hp.right⟩