∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N]
  {f : S.LocalizationMap N} (x : Localization S),
  (Localization.mulEquivOfQuotient f) x = ((Localization.monoidOf S).lift ⋯) x