-- Mathlib/RingTheory/UniqueFactorizationDomain/Defs.lean
theorem not_unit_iff_exists_factors_eq (a : α) (hn0 : a ≠ 0) :
    ¬IsUnit a ↔ ∃ f : Multiset α, (∀ b ∈ f, Irreducible b) ∧ f.prod = a ∧ f ≠ ∅ :=
  ⟨fun hnu => by
    obtain ⟨f, hi, u, rfl⟩ := exists_factors a hn0
    obtain ⟨b, h⟩ := Multiset.exists_mem_of_ne_zero fun h : f = 0 => hnu <| by simp [h]
    classical
      refine ⟨(f.erase b).cons (b * u), fun a ha => ?_, ?_, Multiset.cons_ne_zero⟩
      · obtain rfl | ha := Multiset.mem_cons.1 ha
        exacts [Associated.irreducible ⟨u, rfl⟩ (hi b h), hi a (Multiset.mem_of_mem_erase ha)]
      · rw [Multiset.prod_cons, mul_comm b, mul_assoc, Multiset.prod_erase h, mul_comm],
    fun ⟨_, hi, he, hne⟩ =>
    let ⟨b, h⟩ := Multiset.exists_mem_of_ne_zero hne
    not_isUnit_of_not_isUnit_dvd (hi b h).not_unit <| he ▸ Multiset.dvd_prod h⟩

Proof state:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
a : α
hn0 : a ≠ 0
hnu : ¬IsUnit a
⊢ ∃ f, (∀ b ∈ f, Irreducible b) ∧ f.prod = a ∧ f ≠ ∅

Tactic:
obtain ⟨f, hi, u, rfl⟩ := exists_factors a hn0

Result:
case intro.intro.intro
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
f : Multiset α
hi : ∀ b ∈ f, Irreducible b
u : αˣ
hn0 : f.prod * ↑u ≠ 0
hnu : ¬IsUnit (f.prod * ↑u)
⊢ ∃ f_1, (∀ b ∈ f_1, Irreducible b) ∧ f_1.prod = f.prod * ↑u ∧ f_1 ≠ ∅

Proof state:
case intro.intro.intro.intro.refine_1
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
f : Multiset α
hi : ∀ b ∈ f, Irreducible b
u : αˣ
hn0 : f.prod * ↑u ≠ 0
hnu : ¬IsUnit (f.prod * ↑u)
b : α
h : b ∈ f
a : α
ha : a ∈ b * ↑u ::ₘ f.erase b
⊢ Irreducible a

Tactic:
obtain rfl | ha := Multiset.mem_cons.1 ha

Result:
case intro.intro.intro.intro.refine_1.inl
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
f : Multiset α
hi : ∀ b ∈ f, Irreducible b
u : αˣ
hn0 : f.prod * ↑u ≠ 0
hnu : ¬IsUnit (f.prod * ↑u)
b : α
h : b ∈ f
ha : b * ↑u ∈ b * ↑u ::ₘ f.erase b
⊢ Irreducible (b * ↑u)

case intro.intro.intro.intro.refine_1.inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
f : Multiset α
hi : ∀ b ∈ f, Irreducible b
u : αˣ
hn0 : f.prod * ↑u ≠ 0
hnu : ¬IsUnit (f.prod * ↑u)
b : α
h : b ∈ f
a : α
ha✝ : a ∈ b * ↑u ::ₘ f.erase b
ha : a ∈ f.erase b
⊢ Irreducible a

Proof state:
case intro.intro.intro.intro.refine_1.inl
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
f : Multiset α
hi : ∀ b ∈ f, Irreducible b
u : αˣ
hn0 : f.prod * ↑u ≠ 0
hnu : ¬IsUnit (f.prod * ↑u)
b : α
h : b ∈ f
ha : b * ↑u ∈ b * ↑u ::ₘ f.erase b
⊢ Irreducible (b * ↑u)

case intro.intro.intro.intro.refine_1.inr
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
f : Multiset α
hi : ∀ b ∈ f, Irreducible b
u : αˣ
hn0 : f.prod * ↑u ≠ 0
hnu : ¬IsUnit (f.prod * ↑u)
b : α
h : b ∈ f
a : α
ha✝ : a ∈ b * ↑u ::ₘ f.erase b
ha : a ∈ f.erase b
⊢ Irreducible a

Tactic:
exacts [Associated.irreducible ⟨u, rfl⟩ (hi b h), hi a (Multiset.mem_of_mem_erase ha)]

Result:
no goals

Proof state:
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
f : Multiset α
hi : ∀ b ∈ f, Irreducible b
u : αˣ
hn0 : f.prod * ↑u ≠ 0
hnu : ¬IsUnit (f.prod * ↑u)
b : α
h : b ∈ f
⊢ ∃ f_1, (∀ b ∈ f_1, Irreducible b) ∧ f_1.prod = f.prod * ↑u ∧ f_1 ≠ ∅

Tactic:
refine ⟨(f.erase b).cons (b * u), fun a ha => ?_, ?_, Multiset.cons_ne_zero⟩

Result:
case intro.intro.intro.intro.refine_1
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
f : Multiset α
hi : ∀ b ∈ f, Irreducible b
u : αˣ
hn0 : f.prod * ↑u ≠ 0
hnu : ¬IsUnit (f.prod * ↑u)
b : α
h : b ∈ f
a : α
ha : a ∈ b * ↑u ::ₘ f.erase b
⊢ Irreducible a

case intro.intro.intro.intro.refine_2
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
f : Multiset α
hi : ∀ b ∈ f, Irreducible b
u : αˣ
hn0 : f.prod * ↑u ≠ 0
hnu : ¬IsUnit (f.prod * ↑u)
b : α
h : b ∈ f
⊢ (b * ↑u ::ₘ f.erase b).prod = f.prod * ↑u

Proof state:
case intro.intro.intro
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
f : Multiset α
hi : ∀ b ∈ f, Irreducible b
u : αˣ
hn0 : f.prod * ↑u ≠ 0
hnu : ¬IsUnit (f.prod * ↑u)
⊢ ∃ f_1, (∀ b ∈ f_1, Irreducible b) ∧ f_1.prod = f.prod * ↑u ∧ f_1 ≠ ∅

Tactic:
obtain ⟨b, h⟩ := Multiset.exists_mem_of_ne_zero fun h : f = 0 => hnu <| by simp [h]

Result:
case intro.intro.intro.intro
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
f : Multiset α
hi : ∀ b ∈ f, Irreducible b
u : αˣ
hn0 : f.prod * ↑u ≠ 0
hnu : ¬IsUnit (f.prod * ↑u)
b : α
h : b ∈ f
⊢ ∃ f_1, (∀ b ∈ f_1, Irreducible b) ∧ f_1.prod = f.prod * ↑u ∧ f_1 ≠ ∅

Proof state:
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
f : Multiset α
hi : ∀ b ∈ f, Irreducible b
u : αˣ
hn0 : f.prod * ↑u ≠ 0
hnu : ¬IsUnit (f.prod * ↑u)
h : f = 0
⊢ IsUnit (f.prod * ↑u)

Tactic:
simp [h]

Result:
no goals

Proof state:
case intro.intro.intro.intro.refine_2
α : Type u_1
inst✝¹ : CommMonoidWithZero α
inst✝ : WfDvdMonoid α
f : Multiset α
hi : ∀ b ∈ f, Irreducible b
u : αˣ
hn0 : f.prod * ↑u ≠ 0
hnu : ¬IsUnit (f.prod * ↑u)
b : α
h : b ∈ f
⊢ (b * ↑u ::ₘ f.erase b).prod = f.prod * ↑u

Tactic:
rw [Multiset.prod_cons, mul_comm b, mul_assoc, Multiset.prod_erase h, mul_comm]

Result:
no goals