have : ∃ s : Finset Nat, ∀ p : ℕ, p.Prime ∧ p % 4 = 3 ↔ p ∈ s := by
  apply ex_finset_of_bounded
  use n
  contrapose! hn
  rcases hn with ⟨p, ⟨pp, p4⟩, pltn⟩
  exact ⟨p, pltn, pp, p4⟩
case intro
n : ℕ
hn : ∀ p > n, p.Prime → p % 4 ≠ 3
⊢ False
case intro
n : ℕ
hn : ∀ p > n, p.Prime → p % 4 ≠ 3
this : ∃ s, ∀ (p : ℕ), p.Prime ∧ p % 4 = 3 ↔ p ∈ s
⊢ False