no goals
M : Type u_2
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_1
inst✝¹ : CommMonoid N
P : Type ?u.3281425
inst✝ : CommMonoid P
f : Submonoid.LocalizationMap S N
x : M
⊢ ↑(mulEquivOfQuotient f) (↑(Submonoid.LocalizationMap.toMap (monoidOf S)) x) = ↑(Submonoid.LocalizationMap.toMap f) x
simp