have pne3 : p ≠ 3 := by
  intro peq
  rw [peq, ← Nat.dvd_add_iff_left (dvd_refl 3)] at pdvd
  rw [Nat.prime_three.dvd_mul] at pdvd
  norm_num at pdvd
  have : 3 ∈ s.erase 3 := by
    apply mem_of_dvd_prod_primes Nat.prime_three _ pdvd
    intro n
    simp [← hs n]
    tauto
  simp at this
case intro.intro.intro.intro.intro
n : ℕ
hn : ∀ p > n, p.Prime → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), p.Prime ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i ∈ s.erase 3, i + 3) % 4 = 3
p : ℕ
pp : p.Prime
pdvd : p ∣ 4 * ∏ i ∈ s.erase 3, i + 3
p4eq : p % 4 = 3
ps : p ∈ s
⊢ False
case intro.intro.intro.intro.intro
n : ℕ
hn : ∀ p > n, p.Prime → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), p.Prime ∧ p % 4 = 3 ↔ p ∈ s
h₁ : (4 * ∏ i ∈ s.erase 3, i + 3) % 4 = 3
p : ℕ
pp : p.Prime
pdvd : p ∣ 4 * ∏ i ∈ s.erase 3, i + 3
p4eq : p % 4 = 3
ps : p ∈ s
pne3 : p ≠ 3
⊢ False