exact not_prime_zero (hl 0 (Multiset.prod_eq_zero_iff.1 hprod))
case intro.intro
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
a : R
ha : a ≠ 0
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hP : Set.Nonempty {r | Prime r}
h : 0 ∈ Submonoid.closure {r | Prime r}
l : Multiset R
hl : ∀ y ∈ l, y ∈ {r | Prime r}
hprod : Multiset.prod l = 0
⊢ False
no goals