∀ {M : Type u_5} [inst : AddCommMonoid M] {A : Type u_4} [inst_1 : SetLike A M] [inst_2 : AddSubmonoidClass A M]
  (S : A), AddSubmonoidClass.toAddCommMonoid S = { toAddMonoid := AddSubmonoidClass.toAddMonoid S, add_comm := ⋯ }