merge Add-MonoidAlgebra

Stream: mathlib4

[Damiano Testa]

I focused the translation discussed here to converting MonoidAlgebra into AddMonoidAlgebra in #12637.

Besides shortening the code, a reason for doing this is the divide Finsupp vs AddMonoidAlgebra: the API for Add-MonoidAlgebra is tied together and splitting one without the other was difficult. Splitting them at the same time was also tricky without automation, so this is the automation to split!

[Damiano Testa]

As you can see, there is a command to_ama that does a syntactic replacement of MonoidAlgebra to AddMonoidAlgebra (and a tiny bit more). I'm hoping that similar tweaks can also be used for other parts of the library.

[Damiano Testa]

For now, this is more of a request for comments and suggestions!