∀ {α : Type u_2} [inst : SubtractionMonoid α],
  Set.subtractionMonoid =
    { toAddMonoid := Set.addMonoid, toNeg := Set.involutiveNeg.toNeg, toSub := Set.sub, sub_eq_add_neg := ⋯,
      zsmul := zsmulRec, zsmul_zero' := ⋯, zsmul_succ' := ⋯, zsmul_neg' := ⋯, neg_neg := ⋯, neg_add_rev := ⋯,
      neg_eq_of_add := ⋯ }