no goals
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
inst✝ : Nontrivial α
a b : FactorSet α
⊢ FactorSet.prod a ≤ FactorSet.prod b ↔ a ≤ b
classical
  exact
    Iff.intro
      (fun h => by
        have : a.prod.factors ≤ b.prod.factors := factors_mono h
        rwa [prod_factors, prod_factors] at this)
      prod_mono
no goals
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
inst✝ : Nontrivial α
a b : FactorSet α
⊢ FactorSet.prod a ≤ FactorSet.prod b ↔ a ≤ b
exact
  Iff.intro
    (fun h => by
      have : a.prod.factors ≤ b.prod.factors := factors_mono h
      rwa [prod_factors, prod_factors] at this)
    prod_mono
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
inst✝ : Nontrivial α
a b : FactorSet α
h : FactorSet.prod a ≤ FactorSet.prod b
this : factors (FactorSet.prod a) ≤ factors (FactorSet.prod b)
⊢ a ≤ b
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
inst✝ : Nontrivial α
a b : FactorSet α
h : FactorSet.prod a ≤ FactorSet.prod b
⊢ a ≤ b
have : a.prod.factors ≤ b.prod.factors := factors_mono h
no goals
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝¹ : UniqueFactorizationMonoid α
dec : DecidableEq α
dec' : DecidableEq (Associates α)
inst✝ : Nontrivial α
a b : FactorSet α
h : FactorSet.prod a ≤ FactorSet.prod b
this : factors (FactorSet.prod a) ≤ factors (FactorSet.prod b)
⊢ a ≤ b
rwa [prod_factors, prod_factors] at this