simp [Finset.prod_insert ans, prime_p.dvd_mul] at h₀ h₁
case insert
p : ℕ
prime_p : p.Prime
a : ℕ
s : Finset ℕ
ans : a ∉ s
ih : (∀ n ∈ s, n.Prime) → p ∣ ∏ n ∈ s, n → p ∈ s
h₀ : ∀ n ∈ insert a s, n.Prime
h₁ : p ∣ ∏ n ∈ insert a s, n
⊢ p ∈ insert a s
case insert
p : ℕ
prime_p : p.Prime
a : ℕ
s : Finset ℕ
ans : a ∉ s
ih : (∀ n ∈ s, n.Prime) → p ∣ ∏ n ∈ s, n → p ∈ s
h₀ : a.Prime ∧ ∀ a ∈ s, a.Prime
h₁ : p ∣ a ∨ p ∣ ∏ n ∈ s, n
⊢ p ∈ insert a s