M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type ?u.3298538
inst✝ : CommMonoid P
f : Submonoid.LocalizationMap S N
x : M
y : { x // x ∈ S }
⊢ ↑(MulEquiv.symm (mulEquivOfQuotient f)) (Submonoid.LocalizationMap.mk' f x y) =
    Submonoid.LocalizationMap.mk' (monoidOf S) x y
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type ?u.3298538
inst✝ : CommMonoid P
f : Submonoid.LocalizationMap S N
x : M
y : { x // x ∈ S }
⊢ ↑(MulEquiv.symm (mulEquivOfQuotient f)) (Submonoid.LocalizationMap.mk' f x y) = mk x y
rw [mk_eq_monoidOf_mk'_apply]
no goals
M : Type u_1
inst✝² : CommMonoid M
S : Submonoid M
N : Type u_2
inst✝¹ : CommMonoid N
P : Type ?u.3298538
inst✝ : CommMonoid P
f : Submonoid.LocalizationMap S N
x : M
y : { x // x ∈ S }
⊢ ↑(MulEquiv.symm (mulEquivOfQuotient f)) (Submonoid.LocalizationMap.mk' f x y) =
    Submonoid.LocalizationMap.mk' (monoidOf S) x y
exact mulEquivOfQuotient_symm_mk' _ _