feat(data/nat/{nth,prime}): add facts about primes (#12560)

Gives `{p | prime p}.infinite` as well as `infinite_of_not_bdd_above` lemma. Also gives simp lemmas for `prime_counting'`.

src/data/nat/nth.lean

@@ -146,6 +146,16 @@ lemma nth_mem_of_infinite (hp : (set_of p).infinite) (n : ℕ) : p (nth p n) :=
 lemma nth_strict_mono (hp : (set_of p).infinite) : strict_mono (nth p) :=
 λ a b, (nth_mem_of_infinite_aux p hp b).2 _
 
+lemma nth_injective_of_infinite (hp : (set_of p).infinite) : function.injective (nth p) :=
+begin
+  intros m n h,
+  wlog h' : m ≤ n,
+  rw le_iff_lt_or_eq at h',
+  obtain (h' | rfl) := h',
+  { simpa [h] using nth_strict_mono p hp h' },
+  { refl },
+end
+
 lemma nth_monotone (hp : (set_of p).infinite) : monotone (nth p) :=
 (nth_strict_mono p hp).monotone
 

src/data/nat/prime.lean

@@ -7,6 +7,7 @@ import data.list.prime
 import data.list.sort
 import data.nat.gcd
 import data.nat.sqrt
+import data.set.finite
 import tactic.norm_num
 import tactic.wlog
 
@@ -20,7 +21,8 @@ This file deals with prime numbers: natural numbers `p ≥ 2` whose only divisor
 - `nat.prime`: the predicate that expresses that a natural number `p` is prime
 - `nat.primes`: the subtype of natural numbers that are prime
 - `nat.min_fac n`: the minimal prime factor of a natural number `n ≠ 1`
-- `nat.exists_infinite_primes`: Euclid's theorem that there exist infinitely many prime numbers
+- `nat.exists_infinite_primes`: Euclid's theorem that there exist infinitely many prime numbers.
+  This also appears as `nat.not_bdd_above_set_of_prime` and `nat.infinite_set_of_prime`.
 - `nat.factors n`: the prime factorization of `n`
 - `nat.factors_unique`: uniqueness of the prime factorisation
 * `nat.prime_iff`: `nat.prime` coincides with the general definition of `prime`
@@ -392,6 +394,19 @@ have np : n ≤ p, from le_of_not_ge $ λ h,
   pp.not_dvd_one h₂,
 ⟨p, np, pp⟩
 
+/-- A version of `nat.exists_infinite_primes` using the `bdd_above` predicate. -/
+lemma not_bdd_above_set_of_prime : ¬ bdd_above {p | prime p} :=
+begin
+  rw not_bdd_above_iff,
+  intro n,
+  obtain ⟨p, hi, hp⟩ := exists_infinite_primes n.succ,
+  exact ⟨p, hp, hi⟩,
+end
+
+/-- A version of `nat.exists_infinite_primes` using the `set.infinite` predicate. -/
+lemma infinite_set_of_prime : {p | prime p}.infinite :=
+set.infinite_of_not_bdd_above not_bdd_above_set_of_prime
+
 lemma prime.eq_two_or_odd {p : ℕ} (hp : prime p) : p = 2 ∨ p % 2 = 1 :=
 p.mod_two_eq_zero_or_one.imp_left
   (λ h, ((hp.eq_one_or_self_of_dvd 2 (dvd_of_mod_eq_zero h)).resolve_left dec_trivial).symm)

src/data/set/finite.lean

@@ -828,6 +828,13 @@ finite.induction_on H
   (by simp only [bUnion_empty, bdd_above_empty, ball_empty_iff])
   (λ a s ha _ hs, by simp only [bUnion_insert, ball_insert_iff, bdd_above_union, hs])
 
+lemma infinite_of_not_bdd_above : ¬ bdd_above s → s.infinite :=
+begin
+  contrapose!,
+  rw not_infinite,
+  apply finite.bdd_above,
+end
+
 end
 
 section
@@ -843,6 +850,13 @@ lemma finite.bdd_below_bUnion {I : set β} {S : β → set α} (H : finite I) :
   (bdd_below (⋃i∈I, S i)) ↔ (∀i ∈ I, bdd_below (S i)) :=
 @finite.bdd_above_bUnion (order_dual α) _ _ _ _ _ H
 
+lemma infinite_of_not_bdd_below : ¬ bdd_below s → s.infinite :=
+begin
+  contrapose!,
+  rw not_infinite,
+  apply finite.bdd_below,
+end
+
 end
 
 end set

src/number_theory/prime_counting.lean

@@ -9,7 +9,7 @@ import data.nat.totient
 import algebra.periodic
 import data.finset.locally_finite
 import data.nat.count
-
+import data.nat.nth
 
 /-!
 # The Prime Counting Function
@@ -56,6 +56,12 @@ lemma monotone_prime_counting' : monotone prime_counting' := count_monotone prim
 lemma monotone_prime_counting : monotone prime_counting :=
 λ a b a_le_b, monotone_prime_counting' (add_le_add_right a_le_b 1)
 
+@[simp] lemma prime_counting'_nth_eq (n : ℕ) : π' (nth prime n) = n :=
+count_nth_of_infinite _ infinite_set_of_prime _
+
+@[simp] lemma prime_nth_prime (n : ℕ) : prime (nth prime n) :=
+nth_mem_of_infinite _ infinite_set_of_prime _
+
 /-- A linear upper bound on the size of the `prime_counting'` function -/
 lemma prime_counting'_add_le {a k : ℕ} (h0 : 0 < a) (h1 : a < k) (n : ℕ) :
   π' (k + n) ≤ π' k + nat.totient a * (n / a + 1) :=