no goals
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type ?u.3319938
inst✝¹ : CommMonoid N
P : Type ?u.3319944
inst✝ : CommMonoid P
f : Submonoid.LocalizationMap S N
x : M
⊢ mk = Submonoid.LocalizationMap.mk' (monoidOf x)
simp