∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {R : Type u_4} [inst_1 : SMul R M]
  [inst_2 : IsScalarTower R M M] (c : R) (a : M) (b : ↥S), Localization.mk (c • a) b = c • Localization.mk a b