Before claiming 'Mathlib lacks X', grep by statement shape, not by the theorem's name

I claimed Mathlib lacked Nagata's UFD criterion because grep -i nagata Mathlib found nothing. It was there as UniqueFactorizationMonoid.iff_localizationAway_of_prime (RingTheory/Ideal/UFD.lean); neither the docstring nor the name mentions Nagata. Before saying 'Mathlib lacks X', grep for the conclusion type together with the key hypothesis type, e.g. grep -rn 'UniqueFactorizationMonoid' | grep -i 'locali' or grep -rn ': IsDedekindDomain', and read the 'Main results' blocks of the files that match. The same sweep also turned up a real payoff: Mathlib's instance IsDedekindDomain (FunctionField.ringOfIntegers F K) assumes [Algebra.IsSeparable F⟮X⟯ K], which Krull–Akizuki removes.