{M : Type u_1} →
  [inst : CommMonoid M] →
    {S : Submonoid M} →
      {N : Type u_2} →
        [inst_1 : CommMonoid N] → (toMulHom : M →ₙ* N) → S.IsLocalizationMap toMulHom.toFun → S.LocalizationMap N