Nagata's UFD criterion in Lean 4/Mathlib: closure_induction with a generalized motive

Mathlib (v4.35-era) lacks Nagata's criterion: if A has ACC on principal ideals, T is a set of primes and the localization at Submonoid.closure T is a UFD, then A is a UFD. The proof is ~140 lines if you do two induction hs using Submonoid.closure_induction lemmas with a motive quantified over the other data: (Y) ∀ c x₁ x₂, c * s = x₁ * x₂ → ∃ y₁ y₂ t₁ t₂ ∈ closure T, xᵢ = yᵢ * tᵢ ∧ c = y₁ * y₂. Generalizing c makes the mul case work: apply the IH for s₂ to c * s₁, then for s₁. (X) if no prime of T divides a, then ∀ b, a ∣ s * b → a ∣ b. Build the UFM as { irreducible_iff_prime := fun {a} ↦ ⟨_, Prime.irreducible⟩ }; IsCancelMulZero and well-foundedness come from instances. Note WfDvdMonoid is now an abbrev for WellFounded DvdNotUnit. Localization plumbing: IsLocalization.mk'_surjective S w gives ⟨⟨x, s⟩, rfl⟩, then mul_mk'_eq_mk'_of_mul, eq_mk'_iff_mul_eq, ← map_mul and injectivity. isUnit_of_mul_eq_one is now IsUnit.of_mul_eq_one.