case intro.intro.intro
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
f : Multiset α
hi : ∀ (b : α), b ∈ f → Irreducible b
u : αˣ
hn0 : Multiset.prod f * ↑u ≠ 0
hnu : ¬IsUnit (Multiset.prod f * ↑u)
⊢ ∃ f_1, (∀ (b : α), b ∈ f_1 → Irreducible b) ∧ Multiset.prod f_1 = Multiset.prod f * ↑u ∧ f_1 ≠ ∅
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
a : α
hn0 : a ≠ 0
hnu : ¬IsUnit a
⊢ ∃ f, (∀ (b : α), b ∈ f → Irreducible b) ∧ Multiset.prod f = a ∧ f ≠ ∅
obtain ⟨f, hi, u, rfl⟩ := exists_factors a hn0
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
f : Multiset α
hi : ∀ (b : α), b ∈ f → Irreducible b
u : αˣ
hn0 : Multiset.prod f * ↑u ≠ 0
hnu : ¬IsUnit (Multiset.prod f * ↑u)
b : α
h : b ∈ f
⊢ ∃ f_1, (∀ (b : α), b ∈ f_1 → Irreducible b) ∧ Multiset.prod f_1 = Multiset.prod f * ↑u ∧ f_1 ≠ ∅
case intro.intro.intro
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
f : Multiset α
hi : ∀ (b : α), b ∈ f → Irreducible b
u : αˣ
hn0 : Multiset.prod f * ↑u ≠ 0
hnu : ¬IsUnit (Multiset.prod f * ↑u)
⊢ ∃ f_1, (∀ (b : α), b ∈ f_1 → Irreducible b) ∧ Multiset.prod f_1 = Multiset.prod f * ↑u ∧ f_1 ≠ ∅
obtain ⟨b, h⟩ := Multiset.exists_mem_of_ne_zero fun h : f = 0 => hnu <| by simp [h]
no goals
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
f : Multiset α
hi : ∀ (b : α), b ∈ f → Irreducible b
u : αˣ
hn0 : Multiset.prod f * ↑u ≠ 0
hnu : ¬IsUnit (Multiset.prod f * ↑u)
h : f = 0
⊢ IsUnit (Multiset.prod f * ↑u)
simp [h]
case intro.intro.intro.intro.refine'_1
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
f : Multiset α
hi : ∀ (b : α), b ∈ f → Irreducible b
u : αˣ
hn0 : Multiset.prod f * ↑u ≠ 0
hnu : ¬IsUnit (Multiset.prod f * ↑u)
b : α
h : b ∈ f
a : α
ha : a ∈ b * ↑u ::ₘ Multiset.erase f b
⊢ Irreducible a

case intro.intro.intro.intro.refine'_2
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
f : Multiset α
hi : ∀ (b : α), b ∈ f → Irreducible b
u : αˣ
hn0 : Multiset.prod f * ↑u ≠ 0
hnu : ¬IsUnit (Multiset.prod f * ↑u)
b : α
h : b ∈ f
⊢ Multiset.prod (b * ↑u ::ₘ Multiset.erase f b) = Multiset.prod f * ↑u
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
f : Multiset α
hi : ∀ (b : α), b ∈ f → Irreducible b
u : αˣ
hn0 : Multiset.prod f * ↑u ≠ 0
hnu : ¬IsUnit (Multiset.prod f * ↑u)
b : α
h : b ∈ f
⊢ ∃ f_1, (∀ (b : α), b ∈ f_1 → Irreducible b) ∧ Multiset.prod f_1 = Multiset.prod f * ↑u ∧ f_1 ≠ ∅
refine' ⟨(f.erase b).cons (b * u), fun a ha => _, _, Multiset.cons_ne_zero⟩
case intro.intro.intro.intro.refine'_1.inl
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
f : Multiset α
hi : ∀ (b : α), b ∈ f → Irreducible b
u : αˣ
hn0 : Multiset.prod f * ↑u ≠ 0
hnu : ¬IsUnit (Multiset.prod f * ↑u)
b : α
h : b ∈ f
ha : b * ↑u ∈ b * ↑u ::ₘ Multiset.erase f b
⊢ Irreducible (b * ↑u)

case intro.intro.intro.intro.refine'_1.inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
f : Multiset α
hi : ∀ (b : α), b ∈ f → Irreducible b
u : αˣ
hn0 : Multiset.prod f * ↑u ≠ 0
hnu : ¬IsUnit (Multiset.prod f * ↑u)
b : α
h : b ∈ f
a : α
ha✝ : a ∈ b * ↑u ::ₘ Multiset.erase f b
ha : a ∈ Multiset.erase f b
⊢ Irreducible a
case intro.intro.intro.intro.refine'_1
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
f : Multiset α
hi : ∀ (b : α), b ∈ f → Irreducible b
u : αˣ
hn0 : Multiset.prod f * ↑u ≠ 0
hnu : ¬IsUnit (Multiset.prod f * ↑u)
b : α
h : b ∈ f
a : α
ha : a ∈ b * ↑u ::ₘ Multiset.erase f b
⊢ Irreducible a
obtain rfl | ha := Multiset.mem_cons.1 ha
no goals
case intro.intro.intro.intro.refine'_1.inl
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
f : Multiset α
hi : ∀ (b : α), b ∈ f → Irreducible b
u : αˣ
hn0 : Multiset.prod f * ↑u ≠ 0
hnu : ¬IsUnit (Multiset.prod f * ↑u)
b : α
h : b ∈ f
ha : b * ↑u ∈ b * ↑u ::ₘ Multiset.erase f b
⊢ Irreducible (b * ↑u)

case intro.intro.intro.intro.refine'_1.inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
f : Multiset α
hi : ∀ (b : α), b ∈ f → Irreducible b
u : αˣ
hn0 : Multiset.prod f * ↑u ≠ 0
hnu : ¬IsUnit (Multiset.prod f * ↑u)
b : α
h : b ∈ f
a : α
ha✝ : a ∈ b * ↑u ::ₘ Multiset.erase f b
ha : a ∈ Multiset.erase f b
⊢ Irreducible a
exacts [Associated.irreducible ⟨u, rfl⟩ (hi b h), hi a (Multiset.mem_of_mem_erase ha)]
no goals
case intro.intro.intro.intro.refine'_2
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
f : Multiset α
hi : ∀ (b : α), b ∈ f → Irreducible b
u : αˣ
hn0 : Multiset.prod f * ↑u ≠ 0
hnu : ¬IsUnit (Multiset.prod f * ↑u)
b : α
h : b ∈ f
⊢ Multiset.prod (b * ↑u ::ₘ Multiset.erase f b) = Multiset.prod f * ↑u
rw [Multiset.prod_cons, mul_comm b, mul_assoc, Multiset.prod_erase h, mul_comm]