∀ {G : Type u_2} {M : Type u_1} [inst : AddGroup G] [inst_1 : AddMonoid M] (f : G →+ M) (x : G),
  ↑{ val := f x, neg := f (-x), val_neg := ⋯, neg_val := ⋯ } =
    ↑{ val := f x, neg := f (-x), val_neg := ⋯, neg_val := ⋯ }