-- Mathlib/RingTheory/UniqueFactorizationDomain/Basic.lean
theorem prime_factors_unique [CancelCommMonoidWithZero α] :
    ∀ {f g : Multiset α},
      (∀ x ∈ f, Prime x) → (∀ x ∈ g, Prime x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g

Proof state:
case empty
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
⊢ ∀ {g : Multiset α}, (∀ x ∈ 0, Prime x) → (∀ x ∈ g, Prime x) → Multiset.prod 0 ~ᵤ g.prod → Multiset.Rel Associated 0 g

Tactic:
intros g _ hg h

Result:
case empty
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
g : Multiset α
a✝ : ∀ x ∈ 0, Prime x
hg : ∀ x ∈ g, Prime x
h : Multiset.prod 0 ~ᵤ g.prod
⊢ Multiset.Rel Associated 0 g

Proof state:
case empty
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
g : Multiset α
a✝ : ∀ x ∈ 0, Prime x
hg : ∀ x ∈ g, Prime x
h : Multiset.prod 0 ~ᵤ g.prod
⊢ Multiset.Rel Associated 0 g

Tactic:
exact Multiset.rel_zero_left.2 <|
  Multiset.eq_zero_of_forall_not_mem fun x hx =>
    have : IsUnit g.prod := by simpa [associated_one_iff_isUnit] using h.symm
    (hg x hx).not_unit <|
      isUnit_iff_dvd_one.2 <| (Multiset.dvd_prod hx).trans (isUnit_iff_dvd_one.1 this)

Result:
no goals

Proof state:
case cons
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : α
f : Multiset α
ih : ∀ {g : Multiset α}, (∀ x ∈ f, Prime x) → (∀ x ∈ g, Prime x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
g : Multiset α
hf : ∀ x ∈ p ::ₘ f, Prime x
hg : ∀ x ∈ g, Prime x
hfg : (p ::ₘ f).prod ~ᵤ g.prod
b : α
hbg : b ∈ g
hb : p ~ᵤ b
this : DecidableEq α
⊢ Multiset.Rel Associated (p ::ₘ f) g

Tactic:
rw [← Multiset.cons_erase hbg]

Result:
case cons
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : α
f : Multiset α
ih : ∀ {g : Multiset α}, (∀ x ∈ f, Prime x) → (∀ x ∈ g, Prime x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
g : Multiset α
hf : ∀ x ∈ p ::ₘ f, Prime x
hg : ∀ x ∈ g, Prime x
hfg : (p ::ₘ f).prod ~ᵤ g.prod
b : α
hbg : b ∈ g
hb : p ~ᵤ b
this : DecidableEq α
⊢ Multiset.Rel Associated (p ::ₘ f) (b ::ₘ g.erase b)

Proof state:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : α
f : Multiset α
ih : ∀ {g : Multiset α}, (∀ x ∈ f, Prime x) → (∀ x ∈ g, Prime x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
g : Multiset α
hf : ∀ x ∈ p ::ₘ f, Prime x
hg : ∀ x ∈ g, Prime x
hfg : (p ::ₘ f).prod ~ᵤ g.prod
⊢ p ∣ (p ::ₘ f).prod

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
f : Multiset α
⊢ ∀ {g : Multiset α}, (∀ x ∈ f, Prime x) → (∀ x ∈ g, Prime x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g

Tactic:
induction' f using Multiset.induction_on with p f ih

Result:
case empty
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
⊢ ∀ {g : Multiset α}, (∀ x ∈ 0, Prime x) → (∀ x ∈ g, Prime x) → Multiset.prod 0 ~ᵤ g.prod → Multiset.Rel Associated 0 g

case cons
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : α
f : Multiset α
ih : ∀ {g : Multiset α}, (∀ x ∈ f, Prime x) → (∀ x ∈ g, Prime x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
⊢ ∀ {g : Multiset α},
    (∀ x ∈ p ::ₘ f, Prime x) → (∀ x ∈ g, Prime x) → (p ::ₘ f).prod ~ᵤ g.prod → Multiset.Rel Associated (p ::ₘ f) g

Proof state:
case cons
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : α
f : Multiset α
ih : ∀ {g : Multiset α}, (∀ x ∈ f, Prime x) → (∀ x ∈ g, Prime x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
g : Multiset α
hf : ∀ x ∈ p ::ₘ f, Prime x
hg : ∀ x ∈ g, Prime x
hfg : (p ::ₘ f).prod ~ᵤ g.prod
b : α
hbg : b ∈ g
hb : p ~ᵤ b
this : DecidableEq α
⊢ Multiset.Rel Associated (p ::ₘ f) (b ::ₘ g.erase b)

Tactic:
exact
  Multiset.Rel.cons hb
    (ih (fun q hq => hf _ (by simp [hq]))
      (fun {q} (hq : q ∈ g.erase b) => hg q (Multiset.mem_of_mem_erase hq))
      (Associated.of_mul_left
        (by rwa [← Multiset.prod_cons, ← Multiset.prod_cons, Multiset.cons_erase hbg]) hb
        (hf p (by simp)).ne_zero))

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : α
f : Multiset α
ih : ∀ {g : Multiset α}, (∀ x ∈ f, Prime x) → (∀ x ∈ g, Prime x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
g : Multiset α
hf : ∀ x ∈ p ::ₘ f, Prime x
hg : ∀ x ∈ g, Prime x
hfg : (p ::ₘ f).prod ~ᵤ g.prod
b : α
hbg : b ∈ g
hb : p ~ᵤ b
this : DecidableEq α
⊢ p * f.prod ~ᵤ b * (g.erase b).prod

Tactic:
rwa [← Multiset.prod_cons, ← Multiset.prod_cons, Multiset.cons_erase hbg]

Result:
no goals

Proof state:
case cons
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : α
f : Multiset α
ih : ∀ {g : Multiset α}, (∀ x ∈ f, Prime x) → (∀ x ∈ g, Prime x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
⊢ ∀ {g : Multiset α},
    (∀ x ∈ p ::ₘ f, Prime x) → (∀ x ∈ g, Prime x) → (p ::ₘ f).prod ~ᵤ g.prod → Multiset.Rel Associated (p ::ₘ f) g

Tactic:
intros g hf hg hfg

Result:
case cons
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : α
f : Multiset α
ih : ∀ {g : Multiset α}, (∀ x ∈ f, Prime x) → (∀ x ∈ g, Prime x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
g : Multiset α
hf : ∀ x ∈ p ::ₘ f, Prime x
hg : ∀ x ∈ g, Prime x
hfg : (p ::ₘ f).prod ~ᵤ g.prod
⊢ Multiset.Rel Associated (p ::ₘ f) g

Proof state:
case cons
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : α
f : Multiset α
ih : ∀ {g : Multiset α}, (∀ x ∈ f, Prime x) → (∀ x ∈ g, Prime x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
g : Multiset α
hf : ∀ x ∈ p ::ₘ f, Prime x
hg : ∀ x ∈ g, Prime x
hfg : (p ::ₘ f).prod ~ᵤ g.prod
b : α
hbg : b ∈ g
hb : p ~ᵤ b
⊢ Multiset.Rel Associated (p ::ₘ f) g

Tactic:
haveI := Classical.decEq α

Result:
case cons
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : α
f : Multiset α
ih : ∀ {g : Multiset α}, (∀ x ∈ f, Prime x) → (∀ x ∈ g, Prime x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
g : Multiset α
hf : ∀ x ∈ p ::ₘ f, Prime x
hg : ∀ x ∈ g, Prime x
hfg : (p ::ₘ f).prod ~ᵤ g.prod
b : α
hbg : b ∈ g
hb : p ~ᵤ b
this : DecidableEq α
⊢ Multiset.Rel Associated (p ::ₘ f) g

Proof state:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : α
f : Multiset α
ih : ∀ {g : Multiset α}, (∀ x ∈ f, Prime x) → (∀ x ∈ g, Prime x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
g : Multiset α
hf : ∀ x ∈ p ::ₘ f, Prime x
hg : ∀ x ∈ g, Prime x
hfg : (p ::ₘ f).prod ~ᵤ g.prod
⊢ p ∈ p ::ₘ f

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
g : Multiset α
a✝ : ∀ x ∈ 0, Prime x
hg : ∀ x ∈ g, Prime x
h : Multiset.prod 0 ~ᵤ g.prod
x : α
hx : x ∈ g
⊢ IsUnit g.prod

Tactic:
simpa [associated_one_iff_isUnit] using h.symm

Result:
no goals

Proof state:
case cons
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : α
f : Multiset α
ih : ∀ {g : Multiset α}, (∀ x ∈ f, Prime x) → (∀ x ∈ g, Prime x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
g : Multiset α
hf : ∀ x ∈ p ::ₘ f, Prime x
hg : ∀ x ∈ g, Prime x
hfg : (p ::ₘ f).prod ~ᵤ g.prod
⊢ Multiset.Rel Associated (p ::ₘ f) g

Tactic:
let ⟨b, hbg, hb⟩ :=
  (exists_associated_mem_of_dvd_prod (hf p (by simp)) fun q hq => hg _ hq) <|
    hfg.dvd_iff_dvd_right.1 (show p ∣ (p ::ₘ f).prod by simp)

Result:
case cons
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : α
f : Multiset α
ih : ∀ {g : Multiset α}, (∀ x ∈ f, Prime x) → (∀ x ∈ g, Prime x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
g : Multiset α
hf : ∀ x ∈ p ::ₘ f, Prime x
hg : ∀ x ∈ g, Prime x
hfg : (p ::ₘ f).prod ~ᵤ g.prod
b : α
hbg : b ∈ g
hb : p ~ᵤ b
⊢ Multiset.Rel Associated (p ::ₘ f) g

Proof state:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
p : α
f : Multiset α
ih : ∀ {g : Multiset α}, (∀ x ∈ f, Prime x) → (∀ x ∈ g, Prime x) → f.prod ~ᵤ g.prod → Multiset.Rel Associated f g
g : Multiset α
hf : ∀ x ∈ p ::ₘ f, Prime x
hg : ∀ x ∈ g, Prime x
hfg : (p ::ₘ f).prod ~ᵤ g.prod
b : α
hbg : b ∈ g
hb : p ~ᵤ b
this : DecidableEq α
q : α
hq : q ∈ f
⊢ q ∈ p ::ₘ f

Tactic:
simp [hq]

Result:
no goals