intros a b hab
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
⊢ ∀ (x y : R), x * y ∈ closure {r | IsUnit r ∨ Prime r} → x ∈ closure {r | IsUnit r ∨ Prime r}
R : Type u_1
inst✝ : CancelCommMonoidWithZero R
a b : R
hab : a * b ∈ closure {r | IsUnit r ∨ Prime r}
⊢ a ∈ closure {r | IsUnit r ∨ Prime r}