no goals
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a : Associates α
b : α
this : Associates.mk b = 0
⊢ FactorSet.prod (factors (Quotient.mk (Associated.setoid α) b)) = Quotient.mk (Associated.setoid α) b
simp [quotient_mk_eq_mk, this]
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a : Associates α
b : α
x✝ : Associates.mk b ≠ 0
this : b ≠ 0
⊢ FactorSet.prod (factors (Quotient.mk (Associated.setoid α) b)) = Quotient.mk (Associated.setoid α) b
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a : Associates α
b : α
x✝ : Associates.mk b ≠ 0
⊢ FactorSet.prod (factors (Quotient.mk (Associated.setoid α) b)) = Quotient.mk (Associated.setoid α) b
have : b ≠ 0 := by simp_all
no goals
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a : Associates α
b : α
x✝ : Associates.mk b ≠ 0
this : b ≠ 0
⊢ FactorSet.prod (factors (Quotient.mk (Associated.setoid α) b)) = Quotient.mk (Associated.setoid α) b
simp [this, quotient_mk_eq_mk, prod_mk,
    mk_eq_mk_iff_associated.2 (UniqueFactorizationMonoid.factors_prod this)]
no goals
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a : Associates α
b : α
x✝ : Associates.mk b ≠ 0
⊢ b ≠ 0
simp_all