no goals
R : Type u_1
inst✝⁷ : CommSemiring R
M : Submonoid R
S : Type u_4
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)
T : Submonoid P
Q : Type u_3
inst✝² : CommSemiring Q
hy : M ≤ Submonoid.comap g T
inst✝¹ : Algebra P Q
inst✝ : IsLocalization T Q
j : R ≃+* P
H : Submonoid.map (RingEquiv.toMonoidHom j) M = T
x : R
⊢ ↑(ringEquivOfRingEquiv S Q j H) (↑(algebraMap R S) x) = ↑(algebraMap P Q) (↑j x)
simp