revert a hl hl₂
case intro.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
a : R
l : Multiset R
hl : ∀ y ∈ l, y ∈ {r | IsUnit r ∨ Prime r}
hl₂ : Multiset.prod l = a
⊢ ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) a
case intro.intro
R : Type u_1
inst✝ : CommMonoidWithZero R
l : Multiset R
⊢ ∀ (a : R),
    (∀ y ∈ l, y ∈ {r | IsUnit r ∨ Prime r}) →
      Multiset.prod l = a → ∃ f, (∀ b ∈ f, Prime b) ∧ Associated (Multiset.prod f) a