rw [RingHom.algebraMap_toAlgebra, IsLocalization.map_comp, RingHomCompTriple.comp_eq]
R : Type u_1
inst✝⁵ : CommRing R
inst✝⁴ : IsIntegrallyClosed R
inst✝³ : IsDomain R
M : Submonoid R
hM : M ≤ R⁰
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
K : Type u_1 := FractionRing R
g : S →+* K := IsLocalization.map K (RingHom.id R) hM
this : Algebra S K := g.toAlgebra
⊢ algebraMap R K = (algebraMap S K).comp (algebraMap R S)
no goals