rw [←Finset.mul_prod_erase (a:=p) (h := hps), mul_dvd_mul_iff_left (Nat.Prime.ne_zero hp)] at h_dvd
case pos
s : Finset ℕ
h : ∀ p ∈ s, p.Prime
p : ℕ
hp : p.Prime
h_dvd : p * p ∣ ∏ p ∈ s, p
hps : p ∈ s
⊢ False
case pos
s : Finset ℕ
h : ∀ p ∈ s, p.Prime
p : ℕ
hp : p.Prime
h_dvd : p ∣ ∏ x ∈ s.erase p, x
hps : p ∈ s
⊢ False