chore(ring_theory/unique_factorization_domain): golf (#13820)
+ Shorten the proof of `exists_irreducible_factor` using `well_founded.has_min` instead of `well_founded.fix`.
+ Remove use of `simp` in `induction_on_irreducible`; now a pure term-mode proof except for the classical instance.
+ Change the proof of `not_unit_iff_exists_factors_eq` (just added in [#13682](https://github.com/leanprover-community/mathlib/pull/13682)) to use induction. The new proof doesn't require the `multiset.prod_erase` introduced in [#13682](https://github.com/leanprover-community/mathlib/pull/13682), but is about as complex as the old one, so I might change it back if reviewers prefer.
