have heq : p = q := by
  rw [←Nat.prime_dvd_prime_iff_eq hp (h q hq.1)]
  exact hq.2
case neg.intro
s : Finset ℕ
h : ∀ p ∈ s, p.Prime
p : ℕ
hp : p.Prime
h_dvd : p * p ∣ ∏ p ∈ s, p
hps : p ∉ s
this : p ∣ ∏ p ∈ s, p
q : ℕ
hq : q ∈ s ∧ p ∣ q
⊢ False
case neg.intro
s : Finset ℕ
h : ∀ p ∈ s, p.Prime
p : ℕ
hp : p.Prime
h_dvd : p * p ∣ ∏ p ∈ s, p
hps : p ∉ s
this : p ∣ ∏ p ∈ s, p
q : ℕ
hq : q ∈ s ∧ p ∣ q
heq : p = q
⊢ False