no goals
R : Type u_1
inst✝³ : CommSemiring R
M : Submonoid R
S : Type ?u.2872168
inst✝² : CommSemiring S
inst✝¹ : Algebra R S
P : Type ?u.2872335
inst✝ : CommSemiring P
x : R
y : { x // x ∈ M }
⊢ mk x y = mk' (Localization M) x y
rw [mk_eq_monoidOf_mk'_apply, mk', toLocalizationMap_eq_monoidOf]