Sieve.prodDistinctPrimes_squarefree

lemma prodDistinctPrimes_squarefree (s : Finset ℕ) (h : ∀ p ∈ s, p.Prime) :    Squarefree (∏ p ∈ s, p) := by  refine Iff.mpr Nat.squarefree_iff_prime_squarefree ?_  intro p hp; by_contra h_dvd  by_cases hps : p ∈ s  · rw [←Finset.mul_prod_erase (a:=p) (h := hps), mul_dvd_mul_iff_left (Nat.Prime.ne_zero hp)]      at h_dvd    obtain ⟨q, hq⟩ := hp.prime.exists_mem_finset_dvd h_dvd    rw [Finset.mem_erase] at hq    exact hq.1.1 <| symm <| (Nat.prime_dvd_prime_iff_eq hp (h q hq.1.2)).mp hq.2  · have : p ∣ ∏ p ∈ s, p := Trans.trans (dvd_mul_right p p) h_dvd    obtain ⟨q, hq⟩ := hp.prime.exists_mem_finset_dvd this    have heq : p = q := by      rw [←Nat.prime_dvd_prime_iff_eq hp (h q hq.1)]      exact hq.2    rw [heq] at hps; exact hps hq.1