no goals
R : Type u_1
inst✝⁵ : CommSemiring R
M : Submonoid R
S : Type u_3
inst✝⁴ : CommSemiring S
inst✝³ : Algebra R S
P : Type u_2
inst✝² : CommSemiring P
inst✝¹ : IsLocalization M S
g✝ : R →+* P
hg : ∀ (y : { x // x ∈ M }), IsUnit (↑g✝ ↑y)
inst✝ : Algebra R P
f g : S →ₐ[R] P
⊢ RingHom.comp (↑f) (algebraMap R S) = RingHom.comp (↑g) (algebraMap R S)
rw [f.comp_algebraMap, g.comp_algebraMap]