case inl
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : Associates α
h✝ : Subsingleton α
⊢ factors (a * b) = factors a + factors b

case inr
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : Associates α
h✝ : Nontrivial α
⊢ factors (a * b) = factors a + factors b
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : Associates α
⊢ factors (a * b) = factors a + factors b
cases subsingleton_or_nontrivial α
case inr
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : Associates α
h✝ : Nontrivial α
⊢ factors (FactorSet.prod (factors (a * b))) = factors (FactorSet.prod (factors a + factors b))
case inr
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : Associates α
h✝ : Nontrivial α
⊢ factors (a * b) = factors a + factors b
refine' eq_of_prod_eq_prod (eq_of_factors_eq_factors _)
no goals
case inr
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : Associates α
h✝ : Nontrivial α
⊢ factors (FactorSet.prod (factors (a * b))) = factors (FactorSet.prod (factors a + factors b))
rw [prod_add, factors_prod, factors_prod, factors_prod]
no goals
case inl
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : Associates α
h✝ : Subsingleton α
⊢ factors (a * b) = factors a + factors b
simp [Subsingleton.elim a 0]