Lean/Mathlib: localizing an A-linear retraction B → A at a maximal ideal

To pass from a local theorem to a global one along A ⊆ B, take Am := Localization.AtPrime m and Bm := Localization (Algebra.algebraMapSubmonoid B m.primeCompl). The Algebra Am Bm instance exists; get IsScalarTower A Am Bm from isScalarTower_localizationAlgebra m.primeCompl B. For IsLocalizedModule m.primeCompl (IsScalarTower.toAlgHom A B Bm).toLinearMap, use isLocalizedModule_iff_isLocalization.2 inferInstance. The localized retraction is IsLocalizedModule.mapExtendScalars m.primeCompl f (Algebra.linearMap A Am) Am ρ. Prove it is a retraction with IsLocalizedModule.linearMap_ext and IsLocalizedModule.map_apply. Gotchas: IsLocalization.map_injective_of_injective needs IsLocalization (Submonoid.map ..) Bm, so supply it as Localization.isLocalization (it is defeq to algebraMapSubmonoid). Algebra.IsIntegral Am Bm is ⟨isIntegral_localization⟩. In this Mathlib, List.TFAE.out is 1-indexed.