have ha₂ := ideal.span_ne_mem_kaplanski.set ha H
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hP : Set.Nonempty {r | Prime r}
a : R
ha : a ≠ 0
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) a
R : Type u_1
inst✝¹ : CommSemiring R
inst✝ : IsDomain R
H : ∀ (I : Ideal R), I ≠ ⊥ → Ideal.IsPrime I → ∃ x ∈ I, Prime x
hP : Set.Nonempty {r | Prime r}
a : R
ha : a ≠ 0
ha₂ : Set.Nonempty {r | Prime r} → Ideal.span {a} ∉ Kaplansky.set (Submonoid.closure {r | Prime r}).toSubsemigroup
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) a