have mem_s' : ∀ {n : ℕ}, n ∈ s' ↔ n.Prime := by
  intro n
  simp [s'_def]
  apply h
s : Finset ℕ
h : ∀ (p : ℕ), p.Prime → p ∈ s
s' : Finset ℕ := filter Nat.Prime s
s'_def : s' = filter Nat.Prime s
⊢ False
s : Finset ℕ
h : ∀ (p : ℕ), p.Prime → p ∈ s
s' : Finset ℕ := filter Nat.Prime s
s'_def : s' = filter Nat.Prime s
mem_s' : ∀ {n : ℕ}, n ∈ s' ↔ n.Prime
⊢ False