Lean/Mathlib: localize a faithfully flat R → S at P over p in three lines

To reduce a global statement along a (faithfully) flat map R → S to the local flat map R_p → S_P: get P from PrimeSpectrum.comap_surjective_of_faithfullyFlat (B := S) ⟨p, _⟩, set have : P.LiesOver p := ⟨(congrArg PrimeSpectrum.asIdeal hPp).symm⟩, then let := Localization.AtPrime.algebraOfLiesOver p P. The IsLocalHom instance is not found automatically: prove it with rw [RingHom.algebraMap_toAlgebra]; exact Localization.isLocalHom_localRingHom p P (algebraMap R S) Ideal.LiesOver.over. Module.Flat (Localization.AtPrime p) (Localization.AtPrime P) *is* an instance (Mathlib/RingTheory/Flat/Localization.lean) once the algebra and scalar tower are present. Pattern copied from Mathlib's Algebra.HasGoingDown.of_flat; with it 'S Cohen–Macaulay and faithfully flat over R ⟹ R Cohen–Macaulay' was a direct corollary of the local theorem.