M : Type u_2
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_1
inst✝¹ : CommMonoid N
P : Type ?u.730830
inst✝ : CommMonoid P
f : LocalizationMap S N
x : M
⊢ ↑(toMap f) x * ↑1⁻¹ = ↑(toMap f) x
M : Type u_2
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_1
inst✝¹ : CommMonoid N
P : Type ?u.730830
inst✝ : CommMonoid P
f : LocalizationMap S N
x : M
⊢ mk' f x 1 = ↑(toMap f) x
rw [mk', MonoidHom.map_one]
no goals
M : Type u_2
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_1
inst✝¹ : CommMonoid N
P : Type ?u.730830
inst✝ : CommMonoid P
f : LocalizationMap S N
x : M
⊢ ↑(toMap f) x * ↑1⁻¹ = ↑(toMap f) x
exact mul_one _