-- Mathlib/RingTheory/UniqueFactorizationDomain/FactorSet.lean
theorem FactorSet.unique [Nontrivial α] {p q : FactorSet α} (h : p.prod = q.prod) : p = q

Proof state:
case coe.top
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a✝ : Multiset { a // Irreducible a }
h : prod ↑a✝ = prod ⊤
⊢ ↑a✝ = ⊤

Tactic:
rw [← FactorSet.prod_eq_zero_iff, h, Associates.prod_top]

Result:
no goals

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a✝¹ a✝ : Multiset { a // Irreducible a }
h : prod ↑a✝¹ = prod ↑a✝
⊢ ∀ a ∈ Multiset.map Subtype.val a✝, Irreducible a

Tactic:
intro a ha

Result:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a✝¹ a✝ : Multiset { a // Irreducible a }
h : prod ↑a✝¹ = prod ↑a✝
a : Associates α
ha : a ∈ Multiset.map Subtype.val a✝
⊢ Irreducible a

Proof state:
case coe.coe
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a✝¹ a✝ : Multiset { a // Irreducible a }
h : prod ↑a✝¹ = prod ↑a✝
⊢ ↑a✝¹ = ↑a✝

Tactic:
congr 1

Result:
case coe.coe.e_a
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a✝¹ a✝ : Multiset { a // Irreducible a }
h : prod ↑a✝¹ = prod ↑a✝
⊢ a✝¹ = a✝

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a✝¹ a✝ : Multiset { a // Irreducible a }
h : prod ↑a✝¹ = prod ↑a✝
a : Associates α
ha : a ∈ Multiset.map Subtype.val a✝
⊢ Irreducible a

Tactic:
obtain ⟨⟨a', irred⟩, -, rfl⟩ := Multiset.mem_map.mp ha

Result:
case intro.mk.intro
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a✝¹ a✝ : Multiset { a // Irreducible a }
h : prod ↑a✝¹ = prod ↑a✝
a' : Associates α
irred : Irreducible a'
ha : ↑⟨a', irred⟩ ∈ Multiset.map Subtype.val a✝
⊢ Irreducible ↑⟨a', irred⟩

Proof state:
case coe.coe.e_a
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a✝¹ a✝ : Multiset { a // Irreducible a }
h : prod ↑a✝¹ = prod ↑a✝
⊢ a✝¹ = a✝

Tactic:
rw [← Multiset.map_eq_map Subtype.coe_injective]

Result:
case coe.coe.e_a
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a✝¹ a✝ : Multiset { a // Irreducible a }
h : prod ↑a✝¹ = prod ↑a✝
⊢ Multiset.map (fun a => ↑a) a✝¹ = Multiset.map (fun a => ↑a) a✝

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
p q : FactorSet α
h : p.prod = q.prod
⊢ p = q

Tactic:
unfold FactorSet at p q

Result:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
p q : WithTop (Multiset { a // Irreducible a })
h : prod p = prod q
⊢ p = q

Proof state:
case top.top
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
h : prod ⊤ = prod ⊤
⊢ ⊤ = ⊤

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
p q : WithTop (Multiset { a // Irreducible a })
h : prod p = prod q
⊢ p = q

Tactic:
induction p <;> induction q

Result:
case top.top
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
h : prod ⊤ = prod ⊤
⊢ ⊤ = ⊤

case top.coe
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a✝ : Multiset { a // Irreducible a }
h : prod ⊤ = prod ↑a✝
⊢ ⊤ = ↑a✝

case coe.top
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a✝ : Multiset { a // Irreducible a }
h : prod ↑a✝ = prod ⊤
⊢ ↑a✝ = ⊤

case coe.coe
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a✝¹ a✝ : Multiset { a // Irreducible a }
h : prod ↑a✝¹ = prod ↑a✝
⊢ ↑a✝¹ = ↑a✝

Proof state:
case intro.mk.intro
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a✝¹ a✝ : Multiset { a // Irreducible a }
h : prod ↑a✝¹ = prod ↑a✝
a' : Associates α
irred : Irreducible a'
ha : ↑⟨a', irred⟩ ∈ Multiset.map Subtype.val a✝
⊢ Irreducible ↑⟨a', irred⟩

Tactic:
rwa [Subtype.coe_mk]

Result:
no goals

Proof state:
case top.coe
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
a✝ : Multiset { a // Irreducible a }
h : prod ⊤ = prod ↑a✝
⊢ ⊤ = ↑a✝

Tactic:
rw [eq_comm, ← FactorSet.prod_eq_zero_iff, ← h, Associates.prod_top]

Result:
no goals