∀ {G : Type u_1} [inst : AddGroup G] {S : Type u_4} (H : S) [inst_1 : SetLike S G] [inst_2 : AddSubgroupClass S G],
  AddSubgroupClass.toAddGroup H =
    { toAddMonoid := AddSubmonoidClass.toAddMonoid H, toNeg := NegMemClass.neg, toSub := AddSubgroupClass.sub,
      sub_eq_add_neg := ⋯, zsmul := fun n x => n • x, zsmul_zero' := ⋯, zsmul_succ' := ⋯, zsmul_neg' := ⋯,
      neg_add_cancel := ⋯ }