-- Mathlib/RingTheory/UniqueFactorizationDomain/Basic.lean
theorem WfDvdMonoid.of_exists_prime_factors : WfDvdMonoid α :=
  ⟨by
    classical
      refine RelHomClass.wellFounded
        (RelHom.mk ?_ ?_ : (DvdNotUnit : α → α → Prop) →r ((· < ·) : ℕ∞ → ℕ∞ → Prop)) wellFounded_lt
      · intro a
        by_cases h : a = 0
        · exact ⊤
        exact ↑(Multiset.card (Classical.choose (pf a h)))
      rintro a b ⟨ane0, ⟨c, hc, b_eq⟩⟩
      rw [dif_neg ane0]
      by_cases h : b = 0
      · simp [h, lt_top_iff_ne_top]
      · rw [dif_neg h, Nat.cast_lt]
        have cne0 : c ≠ 0

Proof state:
case neg.calc_2
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
a b : α
ane0 : a ≠ 0
c : α
hc : ¬IsUnit c
b_eq : b = a * c
h : ¬b = 0
cne0 : c ≠ 0
x : α
hadd : x ∈ Classical.choose ⋯ + Classical.choose ⋯
⊢ Prime x

Tactic:
rw [Multiset.mem_add] at hadd

Result:
case neg.calc_2
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
a b : α
ane0 : a ≠ 0
c : α
hc : ¬IsUnit c
b_eq : b = a * c
h : ¬b = 0
cne0 : c ≠ 0
x : α
hadd : x ∈ Classical.choose ⋯ ∨ x ∈ Classical.choose ⋯
⊢ Prime x

Proof state:
case neg.calc_2
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
a b : α
ane0 : a ≠ 0
c : α
hc : ¬IsUnit c
b_eq : b = a * c
h : ¬b = 0
cne0 : c ≠ 0
⊢ ∀ x ∈ Classical.choose ⋯ + Classical.choose ⋯, Prime x

Tactic:
intro x hadd

Result:
case neg.calc_2
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
a b : α
ane0 : a ≠ 0
c : α
hc : ¬IsUnit c
b_eq : b = a * c
h : ¬b = 0
cne0 : c ≠ 0
x : α
hadd : x ∈ Classical.choose ⋯ + Classical.choose ⋯
⊢ Prime x

Proof state:
case neg
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
a b : α
ane0 : a ≠ 0
c : α
hc : ¬IsUnit c
b_eq : b = a * c
h : ¬b = 0
⊢ (Classical.choose ⋯).card < (Classical.choose ⋯).card

Tactic:
have cne0 : c ≠ 0 := by
  refine mt (fun con => ?_) h
  rw [b_eq, con, mul_zero]

Result:
case neg
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
a b : α
ane0 : a ≠ 0
c : α
hc : ¬IsUnit c
b_eq : b = a * c
h : ¬b = 0
cne0 : c ≠ 0
⊢ (Classical.choose ⋯).card < (Classical.choose ⋯).card

Proof state:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
a b : α
ane0 : a ≠ 0
c : α
hc : ¬IsUnit c
b_eq : b = a * c
h : ¬b = 0
cne0 : c ≠ 0
⊢ a * c ~ᵤ (Classical.choose ⋯).prod

Tactic:
rw [← b_eq]

Result:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
a b : α
ane0 : a ≠ 0
c : α
hc : ¬IsUnit c
b_eq : b = a * c
h : ¬b = 0
cne0 : c ≠ 0
⊢ b ~ᵤ (Classical.choose ⋯).prod

Proof state:
case refine_2
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
⊢ ∀ {a b : α},
    DvdNotUnit a b →
      (if h : a = 0 then ⊤ else ↑(Classical.choose ⋯).card) < if h : b = 0 then ⊤ else ↑(Classical.choose ⋯).card

Tactic:
rintro a b ⟨ane0, ⟨c, hc, b_eq⟩⟩

Result:
case refine_2.intro.intro.intro
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
a b : α
ane0 : a ≠ 0
c : α
hc : ¬IsUnit c
b_eq : b = a * c
⊢ (if h : a = 0 then ⊤ else ↑(Classical.choose ⋯).card) < if h : b = 0 then ⊤ else ↑(Classical.choose ⋯).card

Proof state:
case neg
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
a : α
h : ¬a = 0
⊢ ℕ∞

Tactic:
exact ↑(Multiset.card (Classical.choose (pf a h)))

Result:
no goals

Proof state:
case refine_1
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
⊢ α → ℕ∞

Tactic:
intro a

Result:
case refine_1
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
a : α
⊢ ℕ∞

Proof state:
case refine_1
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
a : α
⊢ ℕ∞

Tactic:
by_cases h : a = 0

Result:
case pos
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
a : α
h : a = 0
⊢ ℕ∞

case neg
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
a : α
h : ¬a = 0
⊢ ℕ∞

Proof state:
case refine_2.intro.intro.intro
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
a b : α
ane0 : a ≠ 0
c : α
hc : ¬IsUnit c
b_eq : b = a * c
⊢ (if h : a = 0 then ⊤ else ↑(Classical.choose ⋯).card) < if h : b = 0 then ⊤ else ↑(Classical.choose ⋯).card

Tactic:
rw [dif_neg ane0]

Result:
case refine_2.intro.intro.intro
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
a b : α
ane0 : a ≠ 0
c : α
hc : ¬IsUnit c
b_eq : b = a * c
⊢ ↑(Classical.choose ⋯).card < if h : b = 0 then ⊤ else ↑(Classical.choose ⋯).card

Proof state:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
a b : α
ane0 : a ≠ 0
c : α
hc : ¬IsUnit c
b_eq : b = a * c
h : ¬b = 0
cne0 : c ≠ 0
⊢ (Classical.choose ⋯).prod * (Classical.choose ⋯).prod ~ᵤ a * c

Tactic:
apply Associated.mul_mul <;> apply (Classical.choose_spec (pf _ _)).2 <;> assumption

Result:
no goals

Proof state:
case h.e'_4
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
a b : α
ane0 : a ≠ 0
c : α
hc : ¬IsUnit c
b_eq : b = a * c
h : ¬b = 0
cne0 : c ≠ 0
con : Classical.choose ⋯ = 0
⊢ 1 = (Classical.choose ⋯).prod

Tactic:
rw [con, Multiset.prod_zero]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
pf : ∀ (a : α), a ≠ 0 → ∃ f, (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
a b : α
ane0 : a ≠ 0
c : α
hc : ¬IsUnit c
b_eq : b = a * c
h : ¬b = 0
con : c = 0
⊢ b = 0

Tactic:
rw [b_eq, con, mul_zero]

Result:
no goals