mathlib3

deb3d452 - feat(data/mv_polynomial/equiv): generalize ring_equiv_congr (#6420)

feat(data/mv_polynomial/equiv): generalize ring_equiv_congr (#6420) Following the discussion in #6324, I have modified `mv_polynomial.ring_equiv_of_equiv` and `mv_polynomial.ring_equiv_congr`, that are now called `ring_equiv_congr_left` and `ring_equiv_congr_left`: both are proved as special cases of `ring_equiv_congr` (the situation for algebras is exactly the same). This has the side effect that the lemmas automatically generated by `@[simps]` are not in a good form (see for example the lemma `mv_polynomial.alg_equiv_congr_left_apply ` in the current mathlib, where there is an unwanted `alg_equiv.refl.to_ring_equiv`). To avoid this I deleted the `@[simps]` and I wrote the lemmas by hand (also correcting the problem with `mv_polynomial.alg_equiv_congr_left_apply`). I probably don't understand completely `@[simps]`, since I had to manually modified some other proofs that no longer worked (I mean, I had to do something more that just using the new names). If there is some `simp` lemma I forgot I would be happy to write it.