α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : DecidableEq α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
⊢ x * y ~ᵤ Multiset.prod (factors x + factors y)
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : DecidableEq α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
⊢ Multiset.Rel Associated (factors (x * y)) (factors x + factors y)
refine'
  factors_unique irreducible_of_factor
    (fun a ha =>
      (Multiset.mem_add.mp ha).by_cases (irreducible_of_factor _) (irreducible_of_factor _))
    ((factors_prod (mul_ne_zero hx hy)).trans _)
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : DecidableEq α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
⊢ x * y ~ᵤ Multiset.prod (factors x) * Multiset.prod (factors y)
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : DecidableEq α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
⊢ x * y ~ᵤ Multiset.prod (factors x + factors y)
rw [Multiset.prod_add]
no goals
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : DecidableEq α
inst✝ : UniqueFactorizationMonoid α
x y : α
hx : x ≠ 0
hy : y ≠ 0
⊢ x * y ~ᵤ Multiset.prod (factors x) * Multiset.prod (factors y)
exact (Associated.mul_mul (factors_prod hx) (factors_prod hy)).symm