chore(logic/embedding): reuse proofs from `data.*` (#3341)
Other changes:
* rename `injective.prod` to `injective.prod_map`;
* add `surjective.prod_map`;
* redefine `sigma.map` without pattern matching;
* rename `sigma_map_injective` to `injective.sigma_map`;
* add `surjective.sigma_map`;
* add `injective.sum_map` and `surjective.sum_map`;
* rename `embedding.prod_congr` to `embedding.prod_map`;
* rename `embedding.sum_congr` to `embedding.sum_map`;
* delete `embedding.sigma_congr_right`, add more
general `embedding.sigma_map`.
