Every finite set of natural numbers cannot contain all prime numbers

[thielema]

Theorem C05_Elementary_Number_Theory.S03_Infinitely_Many_Primes.primes_infinite' claims that any finite set of natural numbers misses at least one prime. However, I'd expected to prove the theorem that any finite set of primes misses at least one other prime. The proof for this theorem is also simpler since we can omit the set s' := s.filter Nat.Prime with s'_def.

I suggest to change the type of the theorem as follows:

-theorem primes_infinite' : ∀ s : Finset Nat, ∃ p, Nat.Prime p ∧ p ∉ s := by
+theorem primes_infinite' : ∀ s : Finset Nat, (∀ q∈s, Nat.Prime q) → ∃ p, Nat.Prime p ∧ p ∉ s := by

I am working with leanprover-community/mathematics_in_lean@45b50b9 .