α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : Associates α
h : factors a ≤ factors b
this : FactorSet.prod (factors a) ≤ FactorSet.prod (factors b)
⊢ a ≤ b
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : Associates α
h : factors a ≤ factors b
⊢ a ≤ b
have : a.factors.prod ≤ b.factors.prod := prod_mono h
no goals
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
a b : Associates α
h : factors a ≤ factors b
this : FactorSet.prod (factors a) ≤ FactorSet.prod (factors b)
⊢ a ≤ b
rwa [factors_prod, factors_prod] at this