have := Nat.le_of_dvd zero_lt_one this
case intro.intro
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
p : ℕ
pp : p.Prime
pdvd : p ∣ ∏ i ∈ s', i + 1
this✝ : p ∣ ∏ i ∈ s', i
this : p ∣ 1
⊢ False
case intro.intro
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
p : ℕ
pp : p.Prime
pdvd : p ∣ ∏ i ∈ s', i + 1
this✝¹ : p ∣ ∏ i ∈ s', i
this✝ : p ∣ 1
this : p ≤ 1
⊢ False