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.2533012
inst✝⁴ : CommSemiring P
inst✝³ : IsLocalization M S
g : R →+* P
hg : ∀ (y : { x // x ∈ M }), IsUnit (↑g ↑y)
Q : Type u_2
inst✝² : CommSemiring Q
inst✝¹ : Algebra R Q
inst✝ : IsLocalization M Q
x : R
y : { x // x ∈ M }
⊢ ↑(algEquiv M S Q) (mk' S x y) = mk' Q x y
simp