α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
p q : Multiset (Associates α)
⊢ ∀ (s : Multiset α),
    (∀ (a : Associates α), a ∈ map (Quot.mk Setoid.r) s → Irreducible a) →
      (∀ (a : Associates α), a ∈ q → Irreducible a) →
        prod (map (Quot.mk Setoid.r) s) = prod q → map (Quot.mk Setoid.r) s = q
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
p q : Multiset (Associates α)
⊢ (∀ (a : Associates α), a ∈ p → Irreducible a) →
    (∀ (a : Associates α), a ∈ q → Irreducible a) → prod p = prod q → p = q
apply Multiset.induction_on_multiset_quot p
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
p q : Multiset (Associates α)
⊢ ∀ (s s_1 : Multiset α),
    (∀ (a : Associates α), a ∈ map (Quot.mk Setoid.r) s_1 → Irreducible a) →
      (∀ (a : Associates α), a ∈ map (Quot.mk Setoid.r) s → Irreducible a) →
        prod (map (Quot.mk Setoid.r) s_1) = prod (map (Quot.mk Setoid.r) s) →
          map (Quot.mk Setoid.r) s_1 = map (Quot.mk Setoid.r) s
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
p q : Multiset (Associates α)
⊢ ∀ (s : Multiset α),
    (∀ (a : Associates α), a ∈ map (Quot.mk Setoid.r) s → Irreducible a) →
      (∀ (a : Associates α), a ∈ q → Irreducible a) →
        prod (map (Quot.mk Setoid.r) s) = prod q → map (Quot.mk Setoid.r) s = q
apply Multiset.induction_on_multiset_quot q
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
p q : Multiset (Associates α)
s t : Multiset α
hs : ∀ (a : Associates α), a ∈ map (Quot.mk Setoid.r) t → Irreducible a
ht : ∀ (a : Associates α), a ∈ map (Quot.mk Setoid.r) s → Irreducible a
eq : prod (map (Quot.mk Setoid.r) t) = prod (map (Quot.mk Setoid.r) s)
⊢ map (Quot.mk Setoid.r) t = map (Quot.mk Setoid.r) s
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
p q : Multiset (Associates α)
⊢ ∀ (s s_1 : Multiset α),
    (∀ (a : Associates α), a ∈ map (Quot.mk Setoid.r) s_1 → Irreducible a) →
      (∀ (a : Associates α), a ∈ map (Quot.mk Setoid.r) s → Irreducible a) →
        prod (map (Quot.mk Setoid.r) s_1) = prod (map (Quot.mk Setoid.r) s) →
          map (Quot.mk Setoid.r) s_1 = map (Quot.mk Setoid.r) s
intro s t hs ht eq
case refine'_1
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
p q : Multiset (Associates α)
s t : Multiset α
hs : ∀ (a : Associates α), a ∈ map (Quot.mk Setoid.r) t → Irreducible a
ht : ∀ (a : Associates α), a ∈ map (Quot.mk Setoid.r) s → Irreducible a
eq : prod (map (Quot.mk Setoid.r) t) = prod (map (Quot.mk Setoid.r) s)
⊢ ∀ (x : α), x ∈ t → Irreducible x

case refine'_2
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
p q : Multiset (Associates α)
s t : Multiset α
hs : ∀ (a : Associates α), a ∈ map (Quot.mk Setoid.r) t → Irreducible a
ht : ∀ (a : Associates α), a ∈ map (Quot.mk Setoid.r) s → Irreducible a
eq : prod (map (Quot.mk Setoid.r) t) = prod (map (Quot.mk Setoid.r) s)
⊢ ∀ (x : α), x ∈ s → Irreducible x

case refine'_3
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
p q : Multiset (Associates α)
s t : Multiset α
hs : ∀ (a : Associates α), a ∈ map (Quot.mk Setoid.r) t → Irreducible a
ht : ∀ (a : Associates α), a ∈ map (Quot.mk Setoid.r) s → Irreducible a
eq : prod (map (Quot.mk Setoid.r) t) = prod (map (Quot.mk Setoid.r) s)
⊢ prod t ~ᵤ prod s
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
p q : Multiset (Associates α)
s t : Multiset α
hs : ∀ (a : Associates α), a ∈ map (Quot.mk Setoid.r) t → Irreducible a
ht : ∀ (a : Associates α), a ∈ map (Quot.mk Setoid.r) s → Irreducible a
eq : prod (map (Quot.mk Setoid.r) t) = prod (map (Quot.mk Setoid.r) s)
⊢ map (Quot.mk Setoid.r) t = map (Quot.mk Setoid.r) s
refine' Multiset.map_mk_eq_map_mk_of_rel (UniqueFactorizationMonoid.factors_unique _ _ _)
case refine'_3
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
p q : Multiset (Associates α)
s t : Multiset α
hs : ∀ (a : Associates α), a ∈ map (Quot.mk Setoid.r) t → Irreducible a
ht : ∀ (a : Associates α), a ∈ map (Quot.mk Setoid.r) s → Irreducible a
eq : prod (map (Quot.mk Setoid.r) t) = prod (map (Quot.mk Setoid.r) s)
eq' : Quot.mk Setoid.r = Associates.mk
⊢ prod t ~ᵤ prod s
case refine'_3
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
p q : Multiset (Associates α)
s t : Multiset α
hs : ∀ (a : Associates α), a ∈ map (Quot.mk Setoid.r) t → Irreducible a
ht : ∀ (a : Associates α), a ∈ map (Quot.mk Setoid.r) s → Irreducible a
eq : prod (map (Quot.mk Setoid.r) t) = prod (map (Quot.mk Setoid.r) s)
⊢ prod t ~ᵤ prod s
have eq' : (Quot.mk Setoid.r : α → Associates α) = Associates.mk := funext quot_mk_eq_mk
no goals
case refine'_3
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
p q : Multiset (Associates α)
s t : Multiset α
hs : ∀ (a : Associates α), a ∈ map (Quot.mk Setoid.r) t → Irreducible a
ht : ∀ (a : Associates α), a ∈ map (Quot.mk Setoid.r) s → Irreducible a
eq : prod (map (Quot.mk Setoid.r) t) = prod (map (Quot.mk Setoid.r) s)
eq' : Quot.mk Setoid.r = Associates.mk
⊢ prod t ~ᵤ prod s
rwa [eq', prod_mk, prod_mk, mk_eq_mk_iff_associated] at eq
no goals
case refine'_1
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
p q : Multiset (Associates α)
s t : Multiset α
hs : ∀ (a : Associates α), a ∈ map (Quot.mk Setoid.r) t → Irreducible a
ht : ∀ (a : Associates α), a ∈ map (Quot.mk Setoid.r) s → Irreducible a
eq : prod (map (Quot.mk Setoid.r) t) = prod (map (Quot.mk Setoid.r) s)
⊢ ∀ (x : α), x ∈ t → Irreducible x
exact fun a ha => (irreducible_mk _).1 <| hs _ <| Multiset.mem_map_of_mem _ ha
no goals
case refine'_2
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
dec_irr : (p : Associates α) → Decidable (Irreducible p)
inst✝ : UniqueFactorizationMonoid α
p q : Multiset (Associates α)
s t : Multiset α
hs : ∀ (a : Associates α), a ∈ map (Quot.mk Setoid.r) t → Irreducible a
ht : ∀ (a : Associates α), a ∈ map (Quot.mk Setoid.r) s → Irreducible a
eq : prod (map (Quot.mk Setoid.r) t) = prod (map (Quot.mk Setoid.r) s)
⊢ ∀ (x : α), x ∈ s → Irreducible x
exact fun a ha => (irreducible_mk _).1 <| ht _ <| Multiset.mem_map_of_mem _ ha