∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
  {f : S.LocalizationMap N} (x : AddLocalization S),
  (AddLocalization.addEquivOfQuotient f) x = ((AddLocalization.addMonoidOf S).lift ⋯) x