-- Mathlib/RingTheory/UniqueFactorizationDomain/Basic.lean
theorem unique' {p q : Multiset (Associates α)} :
    (∀ a ∈ p, Irreducible a) → (∀ a ∈ q, Irreducible a) → p.prod = q.prod → p = q

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
p q : Multiset (Associates α)
⊢ ∀ (s : Multiset α),
    (∀ a ∈ map (Quot.mk ⇑(Associated.setoid α)) s, Irreducible a) →
      (∀ a ∈ q, Irreducible a) →
        (map (Quot.mk ⇑(Associated.setoid α)) s).prod = q.prod → map (Quot.mk ⇑(Associated.setoid α)) s = q

Tactic:
apply Multiset.induction_on_multiset_quot q

Result:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
p q : Multiset (Associates α)
⊢ ∀ (s s_1 : Multiset α),
    (∀ a ∈ map (Quot.mk ⇑(Associated.setoid α)) s_1, Irreducible a) →
      (∀ a ∈ map (Quot.mk ⇑(Associated.setoid α)) s, Irreducible a) →
        (map (Quot.mk ⇑(Associated.setoid α)) s_1).prod = (map (Quot.mk ⇑(Associated.setoid α)) s).prod →
          map (Quot.mk ⇑(Associated.setoid α)) s_1 = map (Quot.mk ⇑(Associated.setoid α)) s

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
p q : Multiset (Associates α)
⊢ ∀ (s s_1 : Multiset α),
    (∀ a ∈ map (Quot.mk ⇑(Associated.setoid α)) s_1, Irreducible a) →
      (∀ a ∈ map (Quot.mk ⇑(Associated.setoid α)) s, Irreducible a) →
        (map (Quot.mk ⇑(Associated.setoid α)) s_1).prod = (map (Quot.mk ⇑(Associated.setoid α)) s).prod →
          map (Quot.mk ⇑(Associated.setoid α)) s_1 = map (Quot.mk ⇑(Associated.setoid α)) s

Tactic:
intro s t hs ht eq

Result:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
p q : Multiset (Associates α)
s t : Multiset α
hs : ∀ a ∈ map (Quot.mk ⇑(Associated.setoid α)) t, Irreducible a
ht : ∀ a ∈ map (Quot.mk ⇑(Associated.setoid α)) s, Irreducible a
eq : (map (Quot.mk ⇑(Associated.setoid α)) t).prod = (map (Quot.mk ⇑(Associated.setoid α)) s).prod
⊢ map (Quot.mk ⇑(Associated.setoid α)) t = map (Quot.mk ⇑(Associated.setoid α)) s

Proof state:
case refine_3
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
p q : Multiset (Associates α)
s t : Multiset α
hs : ∀ a ∈ map (Quot.mk ⇑(Associated.setoid α)) t, Irreducible a
ht : ∀ a ∈ map (Quot.mk ⇑(Associated.setoid α)) s, Irreducible a
eq : (map (Quot.mk ⇑(Associated.setoid α)) t).prod = (map (Quot.mk ⇑(Associated.setoid α)) s).prod
eq' : Quot.mk ⇑(Associated.setoid α) = Associates.mk
⊢ t.prod ~ᵤ s.prod

Tactic:
rwa [eq', prod_mk, prod_mk, mk_eq_mk_iff_associated] at eq

Result:
no goals

Proof state:
case refine_2
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
p q : Multiset (Associates α)
s t : Multiset α
hs : ∀ a ∈ map (Quot.mk ⇑(Associated.setoid α)) t, Irreducible a
ht : ∀ a ∈ map (Quot.mk ⇑(Associated.setoid α)) s, Irreducible a
eq : (map (Quot.mk ⇑(Associated.setoid α)) t).prod = (map (Quot.mk ⇑(Associated.setoid α)) s).prod
⊢ ∀ x ∈ s, Irreducible x

Tactic:
exact fun a ha => irreducible_mk.1 <| ht _ <| Multiset.mem_map_of_mem _ ha

Result:
no goals

Proof state:
case refine_1
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
p q : Multiset (Associates α)
s t : Multiset α
hs : ∀ a ∈ map (Quot.mk ⇑(Associated.setoid α)) t, Irreducible a
ht : ∀ a ∈ map (Quot.mk ⇑(Associated.setoid α)) s, Irreducible a
eq : (map (Quot.mk ⇑(Associated.setoid α)) t).prod = (map (Quot.mk ⇑(Associated.setoid α)) s).prod
⊢ ∀ x ∈ t, Irreducible x

Tactic:
exact fun a ha => irreducible_mk.1 <| hs _ <| Multiset.mem_map_of_mem _ ha

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
p q : Multiset (Associates α)
s t : Multiset α
hs : ∀ a ∈ map (Quot.mk ⇑(Associated.setoid α)) t, Irreducible a
ht : ∀ a ∈ map (Quot.mk ⇑(Associated.setoid α)) s, Irreducible a
eq : (map (Quot.mk ⇑(Associated.setoid α)) t).prod = (map (Quot.mk ⇑(Associated.setoid α)) s).prod
⊢ map (Quot.mk ⇑(Associated.setoid α)) t = map (Quot.mk ⇑(Associated.setoid α)) s

Tactic:
refine Multiset.map_mk_eq_map_mk_of_rel (UniqueFactorizationMonoid.factors_unique ?_ ?_ ?_)

Result:
case refine_1
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
p q : Multiset (Associates α)
s t : Multiset α
hs : ∀ a ∈ map (Quot.mk ⇑(Associated.setoid α)) t, Irreducible a
ht : ∀ a ∈ map (Quot.mk ⇑(Associated.setoid α)) s, Irreducible a
eq : (map (Quot.mk ⇑(Associated.setoid α)) t).prod = (map (Quot.mk ⇑(Associated.setoid α)) s).prod
⊢ ∀ x ∈ t, Irreducible x

case refine_2
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
p q : Multiset (Associates α)
s t : Multiset α
hs : ∀ a ∈ map (Quot.mk ⇑(Associated.setoid α)) t, Irreducible a
ht : ∀ a ∈ map (Quot.mk ⇑(Associated.setoid α)) s, Irreducible a
eq : (map (Quot.mk ⇑(Associated.setoid α)) t).prod = (map (Quot.mk ⇑(Associated.setoid α)) s).prod
⊢ ∀ x ∈ s, Irreducible x

case refine_3
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
p q : Multiset (Associates α)
s t : Multiset α
hs : ∀ a ∈ map (Quot.mk ⇑(Associated.setoid α)) t, Irreducible a
ht : ∀ a ∈ map (Quot.mk ⇑(Associated.setoid α)) s, Irreducible a
eq : (map (Quot.mk ⇑(Associated.setoid α)) t).prod = (map (Quot.mk ⇑(Associated.setoid α)) s).prod
⊢ t.prod ~ᵤ s.prod

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
p q : Multiset (Associates α)
⊢ (∀ a ∈ p, Irreducible a) → (∀ a ∈ q, Irreducible a) → p.prod = q.prod → p = q

Tactic:
apply Multiset.induction_on_multiset_quot p

Result:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
p q : Multiset (Associates α)
⊢ ∀ (s : Multiset α),
    (∀ a ∈ map (Quot.mk ⇑(Associated.setoid α)) s, Irreducible a) →
      (∀ a ∈ q, Irreducible a) →
        (map (Quot.mk ⇑(Associated.setoid α)) s).prod = q.prod → map (Quot.mk ⇑(Associated.setoid α)) s = q

Proof state:
case refine_3
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
p q : Multiset (Associates α)
s t : Multiset α
hs : ∀ a ∈ map (Quot.mk ⇑(Associated.setoid α)) t, Irreducible a
ht : ∀ a ∈ map (Quot.mk ⇑(Associated.setoid α)) s, Irreducible a
eq : (map (Quot.mk ⇑(Associated.setoid α)) t).prod = (map (Quot.mk ⇑(Associated.setoid α)) s).prod
⊢ t.prod ~ᵤ s.prod

Tactic:
have eq' : (Quot.mk Setoid.r : α → Associates α) = Associates.mk := funext quot_mk_eq_mk

Result:
case refine_3
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : UniqueFactorizationMonoid α
p q : Multiset (Associates α)
s t : Multiset α
hs : ∀ a ∈ map (Quot.mk ⇑(Associated.setoid α)) t, Irreducible a
ht : ∀ a ∈ map (Quot.mk ⇑(Associated.setoid α)) s, Irreducible a
eq : (map (Quot.mk ⇑(Associated.setoid α)) t).prod = (map (Quot.mk ⇑(Associated.setoid α)) s).prod
eq' : Quot.mk ⇑(Associated.setoid α) = Associates.mk
⊢ t.prod ~ᵤ s.prod