α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
⊢ a ≠ 0 → ∃ f, (∀ (b : α), b ∈ f → Irreducible b) ∧ Multiset.prod f ~ᵤ a
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
⊢ a ≠ 0 → ∃ f, (∀ (b : α), b ∈ f → Prime b) ∧ Multiset.prod f ~ᵤ a
simp_rw [← UniqueFactorizationMonoid.irreducible_iff_prime]
no goals
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
a : α
⊢ a ≠ 0 → ∃ f, (∀ (b : α), b ∈ f → Irreducible b) ∧ Multiset.prod f ~ᵤ a
apply WfDvdMonoid.exists_factors a