refactor(data/mv_polynomial): cleanup equivs (#6589)
This:
* Replaces `alg_equiv_congr_left` with `rename_equiv` (to match `rename`)
* Removes `ring_equiv_congr_left` (it's now `rename_equiv.to_ring_equiv`)
* Renames `alg_equiv_congr_right` to `map_alg_equiv` (to match `map`) and removes the `comap` from the definition
* Renames `ring_equiv_congr_right` to `map_equiv` (to match `map`)
* Removes `alg_equiv_congr` (it's now `(map_alg_equiv R e).trans $ (rename_equiv e_var).restrict_scalars _`, which while longer is never used anyway)
* Removes `ring_equiv_congr` (it's now `(map_equiv R e).trans $ (rename_equiv e_var).to_ring_equiv`, which while longer is never used anyway)
* Replaces `punit_ring_equiv` with `punit_alg_equiv`
* Removes `comap` from the definition of `sum_alg_equiv`
* Promotes `option_equiv_left`, `option_equiv_right`, and `fin_succ_equiv` to `alg_equiv`s
This is a follow-up to #6420
