revert a b hm
case intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
a b : R
hab : a * b ∈ closure {r | IsUnit r ∨ Prime r}
m : Multiset R
hm : ∃ (_ : ∀ y ∈ m, y ∈ {r | IsUnit r ∨ Prime r}), Multiset.prod m = a * b
⊢ a ∈ closure {r | IsUnit r ∨ Prime r}
case intro
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
m : Multiset R
⊢ ∀ (a b : R),
    a * b ∈ closure {r | IsUnit r ∨ Prime r} →
      (∃ (_ : ∀ y ∈ m, y ∈ {r | IsUnit r ∨ Prime r}), Multiset.prod m = a * b) → a ∈ closure {r | IsUnit r ∨ Prime r}