simp
case ha
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
⊢ p ∈ s.erase 3
case ha
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
⊢ ¬p = 3 ∧ p ∈ s