set s' := s.filter Nat.Prime with s'_def
s : Finset ℕ
h : ∀ (p : ℕ), p.Prime → p ∈ s
⊢ False
s : Finset ℕ
h : ∀ (p : ℕ), p.Prime → p ∈ s
s' : Finset ℕ := filter Nat.Prime s
s'_def : s' = filter Nat.Prime s
⊢ False