R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.210005
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
x : { x // x ∈ M }
⊢ ↑(↑(toInvSubmonoid M S) x) * ↑(algebraMap R S) ↑x = mk' S 1 x * ↑(algebraMap R S) ↑x
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.210005
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
x : { x // x ∈ M }
⊢ ↑(↑(toInvSubmonoid M S) x) = mk' S 1 x
rw [← (IsLocalization.map_units S x).mul_left_inj]
no goals
R : Type u_1
inst✝⁴ : CommRing R
M : Submonoid R
S : Type u_2
inst✝³ : CommRing S
inst✝² : Algebra R S
P : Type ?u.210005
inst✝¹ : CommRing P
inst✝ : IsLocalization M S
x : { x // x ∈ M }
⊢ ↑(↑(toInvSubmonoid M S) x) * ↑(algebraMap R S) ↑x = mk' S 1 x * ↑(algebraMap R S) ↑x
simp