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](#13682)) to use induction. The new proof doesn't require the `multiset.prod_erase` introduced in [#13682](#13682), but is about as complex as the old one, so I might change it back if reviewers prefer.

src/ring_theory/unique_factorization_domain.lean

@@ -71,41 +71,32 @@ local attribute [elab_as_eliminator] well_founded.fix
 
 lemma exists_irreducible_factor {a : α} (ha : ¬ is_unit a) (ha0 : a ≠ 0) :
   ∃ i, irreducible i ∧ i ∣ a :=
-(irreducible_or_factor a ha).elim (λ hai, ⟨a, hai, dvd_rfl⟩)
-  (well_founded.fix
-    well_founded_dvd_not_unit
-    (λ a ih ha ha0 ⟨x, y, hx, hy, hxy⟩,
-      have hx0 : x ≠ 0, from λ hx0, ha0 (by rw [← hxy, hx0, zero_mul]),
-      (irreducible_or_factor x hx).elim
-        (λ hxi, ⟨x, hxi, hxy ▸ by simp⟩)
-        (λ hxf, let ⟨i, hi⟩ := ih x ⟨hx0, y, hy, hxy.symm⟩ hx hx0 hxf in
-          ⟨i, hi.1, hi.2.trans (hxy ▸ by simp)⟩)) a ha ha0)
+let ⟨b, hs, hr⟩ := well_founded_dvd_not_unit.has_min {b | b ∣ a ∧ ¬ is_unit b} ⟨a, dvd_rfl, ha⟩ in
+⟨b, ⟨hs.2, λ c d he, let h := dvd_trans ⟨d, he⟩ hs.1 in or_iff_not_imp_left.2 $
+  λ hc, of_not_not $ λ hd, hr c ⟨h, hc⟩ ⟨ne_zero_of_dvd_ne_zero ha0 h, d, hd, he⟩⟩, hs.1⟩
 
 @[elab_as_eliminator] lemma induction_on_irreducible {P : α → Prop} (a : α)
   (h0 : P 0) (hu : ∀ u : α, is_unit u → P u)
   (hi : ∀ a i : α, a ≠ 0 → irreducible i → P a → P (i * a)) :
   P a :=
 by haveI := classical.dec; exact
-well_founded.fix well_founded_dvd_not_unit
-  (λ a ih, if ha0 : a = 0 then ha0.symm ▸ h0
+well_founded_dvd_not_unit.fix
+  (λ a ih, if ha0 : a = 0 then ha0.substr h0
     else if hau : is_unit a then hu a hau
-    else let ⟨i, hii, ⟨b, hb⟩⟩ := exists_irreducible_factor hau ha0 in
-      have hb0 : b ≠ 0, from λ hb0, by simp * at *,
-      hb.symm ▸ hi _ _ hb0 hii (ih _ ⟨hb0, i,
-        hii.1, by rw [hb, mul_comm]⟩))
+    else let ⟨i, hii, b, hb⟩ := exists_irreducible_factor hau ha0,
+      hb0 : b ≠ 0 := ne_zero_of_dvd_ne_zero ha0 ⟨i, mul_comm i b ▸ hb⟩ in
+      hb.symm ▸ hi b i hb0 hii $ ih b ⟨hb0, i, hii.1, mul_comm i b ▸ hb⟩)
   a
 
 lemma exists_factors (a : α) : a ≠ 0 →
   ∃ f : multiset α, (∀ b ∈ f, irreducible b) ∧ associated f.prod a :=
 induction_on_irreducible a
   (λ h, (h rfl).elim)
-  (λ u hu _, ⟨0, ⟨by simp [hu], associated.symm (by simp [hu, associated_one_iff_is_unit])⟩⟩)
-  (λ a i ha0 hii ih hia0,
+  (λ u hu _, ⟨0, λ _ h, h.elim, hu.unit, one_mul _⟩)
+  (λ a i ha0 hi ih _,
     let ⟨s, hs⟩ := ih ha0 in
-    ⟨i ::ₘ s, ⟨by clear _let_match;
-    { intros b H, cases (multiset.mem_cons.mp H), { convert hii }, { exact hs.1 b h } },
-      by { rw multiset.prod_cons,
-           exact hs.2.mul_left _ }⟩⟩)
+    ⟨i ::ₘ s, λ b H, (multiset.mem_cons.1 H).elim (λ h, h.symm ▸ hi) (hs.1 b),
+      by { rw s.prod_cons i, exact hs.2.mul_left i }⟩)
 
 lemma not_unit_iff_exists_factors_eq (a : α) (hn0 : a ≠ 0) :
   ¬ is_unit a ↔ ∃ f : multiset α, (∀ b ∈ f, irreducible b) ∧ f.prod = a ∧ f ≠ ∅ :=
@@ -117,8 +108,8 @@ lemma not_unit_iff_exists_factors_eq (a : α) (hn0 : a ≠ 0) :
     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] },
 end,
-λ ⟨f,hi,he,hne⟩, let ⟨b, h⟩ := multiset.exists_mem_of_ne_zero hne in
-  not_is_unit_of_not_is_unit_dvd (hi b h).not_unit (he.subst $ multiset.dvd_prod h)⟩
+λ ⟨f, hi, he, hne⟩, let ⟨b, h⟩ := multiset.exists_mem_of_ne_zero hne in
+  not_is_unit_of_not_is_unit_dvd (hi b h).not_unit $ he ▸ multiset.dvd_prod h⟩
 
 end wf_dvd_monoid