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