∀ {R : Type u} {M : Type v} [inst : Monoid R] [inst_1 : MulAction R M] {A : Type u_1} [inst_2 : SetLike A M]
  [hA : SMulMemClass A R M] (S' : A), Function.Injective ⇑(SubMulAction.SMulMemClass.subtype S')