rw [mem_insert]
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
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 = a ∨ p ∈ s