simp [← hs n]
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
p4eq : p % 4 = 3
ps : p ∈ s
peq : p = 3
pdvd : 3 ∣ ∏ i ∈ s.erase 3, i
n : ℕ
⊢ n ∈ s.erase 3 → n.Prime
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
p4eq : p % 4 = 3
ps : p ∈ s
peq : p = 3
pdvd : 3 ∣ ∏ i ∈ s.erase 3, i
n : ℕ
⊢ ¬n = 3 → n.Prime → n % 4 = 3 → n.Prime