exact hq.1.1 $ symm $ (Nat.prime_dvd_prime_iff_eq hp (h q hq.1.2)).mp hq.2
case pos.intro
s : Finset ℕ
h : ∀ p ∈ s, p.Prime
p : ℕ
hp : p.Prime
h_dvd : p ∣ ∏ x ∈ s.erase p, x
hps : p ∈ s
q : ℕ
hq : (q ≠ p ∧ q ∈ s) ∧ p ∣ q
⊢ False
no goals