mathlib

832acd63 - feat(data/{sym2,sym}) decidable version of sym2.mem.other, filling out some of sym API (#4008)

feat(data/{sym2,sym}) decidable version of sym2.mem.other, filling out some of sym API (#4008) Removes `sym2.vmem` and replaces it with `sym2.mem.other'`, which can get the other element of a pair in the presence of decidable equality. Writing `sym2.mem.other'` was beyond my abilities when I created `sym2.vmem`, and seeing that vmem is extremely specialized and has no immediate use, it's probably best to remove it. Adds some assorted simp lemmas, and also an additional lemma that `sym2.mem.other` is, in some sense, an involution. Adds to the API for `sym`. This is from taking some of the interface for multisets. (I was exploring whether `sym2 α` should be re-implemented as `sym α 2` and trying to add enough to `sym` to pull it off, but it doesn't seem to be worth it in the end.) (I'm not committing a recursor for `sym α n`, which lets you represent elements by vectors of length `n`. It needs some cleanup.)