{M' : Type u_1} →
  {α : Type u_2} →
    {S' : Type u_4} →
      [inst : SetLike S' M'] →
        (s : S') → [inst_1 : Monoid M'] → [inst_2 : SubmonoidClass S' M'] → [MulAction M' α] → MulAction (↥s) α