∀ {M : Type u_1} {R : Type u_3} [inst : Monoid M] [inst_1 : Semiring R] [inst_2 : MulSemiringAction M R] {S : Type u_2}
  [inst_3 : SetLike S M] (s : S) [inst_4 : SubmonoidClass S M] (r : ↥s), r • 1 = 1