This claim is waiting to be formalized in the library in `group-theory.symmetric-concrete-groups`: - [ ] Equivalent sets have isomorphic symmetric concrete groups