have : 2 ≤ (∏ i in s', i) + 1 := by
  apply Nat.succ_le_succ
  apply Nat.succ_le_of_lt
  apply Finset.prod_pos
  intro n ns'
  apply (mem_s'.mp ns').pos
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
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
this : 2 ≤ ∏ i ∈ s', i + 1
⊢ False