`to_additive` feature requests / issues

This is a single issue for issues or feature requests for to_additive, that I'll try to keep up-to-date. Feel free to comment with other suggestions

• Reorder arguments using an arbitrary permutation. This can be used to fix some to_additive connections in #1056
• Improve output of to_additive?, showing the type of the generated declaration (and not the body for lemmas)
• Even more reorder features, so that we can reorder Pow.mk to SMul.mk (requires re-ordering the function arguments in a particular argument)
• to_additive (attr := scoped simp) can scope the additive version in the wrong namespace (Zulip).
• [bug] additivize lemmas generated by norm_cast (and other attributes).
• Allow specifying types where to_additive doesn't translate operations. Zulip 1 2 -- fixed by #19297
• [probably wontfix]: to_additive does not support match ... with. Zulip, also filed as #1428
• noncomputable definitions in a noncomputable sections won't be translated properly unless you explicitly specify noncomputable (this is https://github.com/leanprover/lean4/pull/2610)
• The congr can generate complicated terms involving Eq.rec that to_additive has a hard time to additivize. E.g. MeasureTheory.Measure.haar.prehaar_sup_eq
• Apparently to_additive doesn't work well with private: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/.60.40.5Bto_additive.5D.60.20bug.3F
• to_additive doesn't copy the docstring of alias: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/to_additive.20and.20deprecated.20alias
• #19424
• to_additive should additivize structures (warning: requires syntax for adding docstrings to constructors)
• to_additive should additivize instances created by the extends-clause for structures (i.e. put these instances into the translation dictionary). This is possible since https://github.com/leanprover/lean4/pull/5853 -- fixed in #19302
• Improve the to_additive heuristic so that we can support lemmas that have both a variable ring-like type (that should not be additivized) and a variable monoid-like type (that should be). This would allow writing a multiplicative version of MeasureTheory.convolution where G is multiplicative and to_additive additivizes it (without touching 𝕜) (Zulip, and there are probably more).
  Note: We now have the option dont_translate to work around limitations of the heuristic.
• (low priority) More robustly reorder universe variables
• Allow for a declaration to have multiple to_additive translations, depending on the "relevant" arguments (the types where we additivize functions). We can already specify which ones to translate using dont_translate, and this would require finding the right translation, and maybe automatically generating the names of the various additive versions.
• (hard) somehow translate from G →* Multiplicative H to Additive G →+ H
• to_dual and to_additive interaction, and potentially with a third translation attribute (or simps)
• Make guessName hashmaps into environment extesions

Start by choosing one unchecked to_additive item and reading its linked Zulip discussion or referenced issue, such as #1428. Define completion for that single request before changing anything; this umbrella issue is addressed only when the selected behavior is implemented and its stated limitation is resolved.