have hsubset : Submonoid.closure {r : R | Prime r} ≤
    Submonoid.closure {r : R | IsUnit r ∨ Prime r} := by
  refine' Submonoid.closure_mono (Set.setOf_subset_setOf.2 (fun _ ha => _))
  right
  exact ha
case intro.intro.intro
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}) ∩ ↑(Submonoid.closure {r | Prime r}).toSubsemigroup ≠ ∅
x : R
hx : x ∈ ↑(Ideal.span {a})
b : R
hx₂ : a * b ∈ ↑(Submonoid.closure {r | Prime r}).toSubsemigroup
hb : b * a = x
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) a
case intro.intro.intro
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}) ∩ ↑(Submonoid.closure {r | Prime r}).toSubsemigroup ≠ ∅
x : R
hx : x ∈ ↑(Ideal.span {a})
b : R
hx₂ : a * b ∈ ↑(Submonoid.closure {r | Prime r}).toSubsemigroup
hb : b * a = x
hsubset : Submonoid.closure {r | Prime r} ≤ Submonoid.closure {r | IsUnit r ∨ Prime r}
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) a