have h_p_div_prod : p ∣ ∏ q in S, q := dvd_prod_of_mem (fun (i : ℕ) => i) a
case h
S : Finset ℕ
h : ∀ {q : ℕ}, q ∈ S → q.Prime
n : ℕ := 1 + ∏ q ∈ S, q
p : ℕ := n.minFac
hp : p.Prime
a : p ∈ S
⊢ False
case h
S : Finset ℕ
h : ∀ {q : ℕ}, q ∈ S → q.Prime
n : ℕ := 1 + ∏ q ∈ S, q
p : ℕ := n.minFac
hp : p.Prime
a : p ∈ S
h_p_div_prod : p ∣ ∏ q ∈ S, q
⊢ False