infinitely many primes satisfying a property

Stream: new members

[Alex Brodbelt]

Hi! I am back again having fun :dancer: with Lean and was wondering how one would simulate the (very satisfying) argument that is done for proving infinitely many primes, but in a more general context:

Problem statement: Prove there are infinitely many primes satisfying the proposition $P$.

Argument I would like to simulate as closely as possible:
Suppose for a contradiction you have a finite set of primes $\{p_1, p_2, \ldots, p_N\}$ satisfying proposition $P$. So the statement would look like:

import Mathlib

theorem infinitely_many_good_primes (P : ℕ → Prop) :
    Infinite { p : ℕ | Nat.Prime p ∧ P p } := by
    by_contra! h
    rw [not_infinite_iff_finite] at h
    sorry

Then using (or not) all the $p_i$ I can generate a new number not divisible by any of the $p_i$ but has a prime divisor $p \ne p_i$ which I can prove satisfies $P$; thus (...not sure how to generate the contradiction here) this finite set is larger than originally presumed since $p \ne p_i$ and by repeating this process it can be made arbitrarily large (this is how I would plausibly try formalise this style of proof).

I suspect I do not even have to phrase it as a contradiction proof in Lean (as I do in the stubbed out statement) since I vaguely recall Infinite typeclass can be shown to hold by providing an injection from the naturals to the set/type, or some variation of this kind.

Thanks :-)

[Edward van de Meent]

i'd say this is the style of the proof here:

import Mathlib

theorem infinitely_many_numbers (P : ℕ → Prop) (f : Finset {p // P p} → {p // P p})
    (hf : ∀ s, f s ∉ s) :
    Infinite { p : ℕ | P p } := by
  by_contra! h
  rw [not_infinite_iff_finite, Set.coe_setOf] at h
  have : Fintype {p : ℕ // P p} := @Fintype.ofFinite _ h
  exact hf _ (Finset.mem_univ _)

[Edward van de Meent]

so basically, "find a function which takes a finite set of numbers with a property, and finds a new one"

[Alex Brodbelt]

ahhh beautiful, I haven't peeked into the details to see whether it is quite what I need... but already :cook:

[Alex Brodbelt]

indeed indeed, I should have trusted the elegance of it. Thanks @Edward van de Meent !