have hp : Nat.Prime p := by
  have hn : 0 < ∏ q in S, q := by
    refine' Finset.prod_pos _
    intros q hq
    refine' Prime.pos <| h hq
  exact Nat.minFac_prime <| Nat.ne_of_gt <| lt_add_of_pos_right 1 hn
case h
S : Finset ℕ
h : ∀ {q : ℕ}, q ∈ S → q.Prime
n : ℕ := 1 + ∏ q ∈ S, q
p : ℕ := n.minFac
⊢ p.Prime ∧ p ∉ S
case h
S : Finset ℕ
h : ∀ {q : ℕ}, q ∈ S → q.Prime
n : ℕ := 1 + ∏ q ∈ S, q
p : ℕ := n.minFac
hp : p.Prime
⊢ p.Prime ∧ p ∉ S