α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : DecidableEq α
inst✝ : UniqueFactorizationMonoid α
✝ : Nontrivial α
⊢ factors 1 = 0
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : DecidableEq α
inst✝ : UniqueFactorizationMonoid α
⊢ factors 1 = 0
nontriviality α using factors
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : DecidableEq α
inst✝ : UniqueFactorizationMonoid α
✝ : Nontrivial α
⊢ Multiset.Rel ?m.393736 (factors 1) 0

α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : DecidableEq α
inst✝ : UniqueFactorizationMonoid α
✝ : Nontrivial α
⊢ Type ?u.393733

α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : DecidableEq α
inst✝ : UniqueFactorizationMonoid α
✝ : Nontrivial α
⊢ α → ?m.393735 → Prop
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : DecidableEq α
inst✝ : UniqueFactorizationMonoid α
✝ : Nontrivial α
⊢ factors 1 = 0
rw [← Multiset.rel_zero_right]
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : DecidableEq α
inst✝ : UniqueFactorizationMonoid α
✝ : Nontrivial α
⊢ Multiset.prod (factors 1) ~ᵤ Multiset.prod 0
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : DecidableEq α
inst✝ : UniqueFactorizationMonoid α
✝ : Nontrivial α
⊢ Multiset.Rel ?m.393736 (factors 1) 0

α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : DecidableEq α
inst✝ : UniqueFactorizationMonoid α
✝ : Nontrivial α
⊢ Type ?u.393733

α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : DecidableEq α
inst✝ : UniqueFactorizationMonoid α
✝ : Nontrivial α
⊢ α → ?m.393735 → Prop
refine' factors_unique irreducible_of_factor (fun x hx => (Multiset.not_mem_zero x hx).elim) _
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : DecidableEq α
inst✝ : UniqueFactorizationMonoid α
✝ : Nontrivial α
⊢ Multiset.prod (factors 1) ~ᵤ 1
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : DecidableEq α
inst✝ : UniqueFactorizationMonoid α
✝ : Nontrivial α
⊢ Multiset.prod (factors 1) ~ᵤ Multiset.prod 0
rw [Multiset.prod_zero]
no goals
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : DecidableEq α
inst✝ : UniqueFactorizationMonoid α
✝ : Nontrivial α
⊢ Multiset.prod (factors 1) ~ᵤ 1
exact factors_prod one_ne_zero