-- Module: Mathlib.RingTheory.UniqueFactorizationDomain.Basic
Goal:
α : Type u_1
inst : CommMonoidWithZero α
inst_1 : IsCancelMulZero α
pf : ∀ (a : α), a ≠ 0 → ∃ (f : Multiset α), (∀ b ∈ f, Prime b) ∧ f.prod ~ᵤ a
refine_1 : α → ℕ∞
refine_2 refine_2₁ :
  ∀ {a b : α},
    DvdNotUnit a b →
      LT.lt (α := ℕ∞)
        (if h : a = 0 then ⊤
        else (↑(Classical.choose (p := fun (x : Multiset α) ↦ (∀ b ∈ x, Prime b) ∧ x.prod ~ᵤ a) ⋯).card : ℕ∞))
        (if h : b = 0 then ⊤
        else (↑(Classical.choose (p := fun (x : Multiset α) ↦ (∀ b ∈ x, Prime b) ∧ x.prod ~ᵤ b) ⋯).card : ℕ∞))
refine_2₂ :
  ∀ {a b : α} (ane0 : a ≠ 0) (c : α) (hc : ¬IsUnit c) (b_eq : b = a * c),
    LT.lt (α := ℕ∞)
      (if h : a = 0 then ⊤
      else (↑(Classical.choose (p := fun (x : Multiset α) ↦ (∀ b ∈ x, Prime b) ∧ x.prod ~ᵤ a) ⋯).card : ℕ∞))
      (if h : b = 0 then ⊤
      else (↑(Classical.choose (p := fun (x : Multiset α) ↦ (∀ b ∈ x, Prime b) ∧ x.prod ~ᵤ b) ⋯).card : ℕ∞))
refine_2₃ :
  ∀ {a b : α} (ane0 : a ≠ 0) (c : α) (hc : ¬IsUnit c) (b_eq : b = a * c),
    LT.lt (α := ℕ∞) (↑(Classical.choose (p := fun (x : Multiset α) ↦ (∀ b ∈ x, Prime b) ∧ x.prod ~ᵤ a) ⋯).card : ℕ∞)
      (if h : b = 0 then ⊤
      else (↑(Classical.choose (p := fun (x : Multiset α) ↦ (∀ b ∈ x, Prime b) ∧ x.prod ~ᵤ b) ⋯).card : ℕ∞))
pos :
  ∀ {a b : α} (ane0 : a ≠ 0) (c : α) (hc : ¬IsUnit c) (b_eq : b = a * c) (h : b = 0),
    LT.lt (α := ℕ∞) (↑(Classical.choose (p := fun (x : Multiset α) ↦ (∀ b ∈ x, Prime b) ∧ x.prod ~ᵤ a) ⋯).card : ℕ∞)
      (if h : b = 0 then ⊤
      else (↑(Classical.choose (p := fun (x : Multiset α) ↦ (∀ b ∈ x, Prime b) ∧ x.prod ~ᵤ b) ⋯).card : ℕ∞))
neg neg₁ :
  ∀ {a b : α} (ane0 : a ≠ 0) (c : α) (hc : ¬IsUnit c) (b_eq : b = a * c) (h : ¬b = 0),
    LT.lt (α := ℕ∞) (↑(Classical.choose (p := fun (x : Multiset α) ↦ (∀ b ∈ x, Prime b) ∧ x.prod ~ᵤ a) ⋯).card : ℕ∞)
      (if h : b = 0 then ⊤
      else (↑(Classical.choose (p := fun (x : Multiset α) ↦ (∀ b ∈ x, Prime b) ∧ x.prod ~ᵤ b) ⋯).card : ℕ∞))
⊢ WellFounded.{u_1 + 1} (α := α) DvdNotUnit

Tactic:
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 := by
          refine mt (fun con => ?_) h
          rw [b_eq, con, mul_zero]
        calc
          Multiset.card (Classical.choose (pf a ane0)) <
              _ + Multiset.card (Classical.choose (pf c cne0)) :=
            lt_add_of_pos_right _
              (Multiset.card_pos.mpr fun con => hc (associated_one_iff_isUnit.mp ?_))
          _ = Multiset.card (Classical.choose (pf a ane0) + Classical.choose (pf c cne0)) :=
            (Multiset.card_add _ _).symm
          _ = Multiset.card (Classical.choose (pf b h)) :=
            Multiset.card_eq_card_of_rel
            (prime_factors_unique ?_ (Classical.choose_spec (pf _ h)).1 ?_)
        · convert! (Classical.choose_spec (pf c cne0)).2.symm
          rw [con, Multiset.prod_zero]
        · intro x hadd
          rw [Multiset.mem_add] at hadd
          rcases hadd with h | h <;> apply (Classical.choose_spec (pf _ _)).1 _ h <;> assumption
        · rw [Multiset.prod_add]
          trans a * c
          · apply Associated.mul_mul <;> apply (Classical.choose_spec (pf _ _)).2 <;> assumption
          · rw [← b_eq]
            apply (Classical.choose_spec (pf _ _)).2.symm; assumption

Premises used: Multiset.prod_zero, RelHomClass.wellFounded, Multiset.card_add, Multiset.mem_add, lt_top_iff_ne_top, Classical.choose_spec, Associated.symm, wellFounded_lt, And.right, Multiset.prod_add, RelHom.mk, Eq.symm, Nat.cast_lt, Associated.mul_mul