have h₁ : ((4 * ∏ i in erase s 3, i) + 3) % 4 = 3 := by
  rw [add_comm, Nat.add_mul_mod_self_left]
case intro.intro
n : ℕ
hn : ∀ p > n, p.Prime → p % 4 ≠ 3
s : Finset ℕ
hs : ∀ (p : ℕ), p.Prime ∧ p % 4 = 3 ↔ p ∈ s
⊢ False
case 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
⊢ False