fix(transform_decl): fix namespace bug (#8733)
* The problem was that when writing `@[to_additive] def foo ...` every declaration used in `foo` in namespace `foo` would be additivized without changing the last part of the name. This behavior was intended to translate automatically generated declarations like `foo._proof_1`. However, if `foo` contains a non-internal declaration `foo.bar` and `add_foo.bar` didn't exist yet, it would also create a declaration `add_foo.bar` additivizing `foo.bar`.
* This PR changes the behavior: if `foo.bar` has the `@[to_additive]` attribute (potentially with a custom additive name), then we won't create a second additive version of `foo.bar`, and succeed normally. However, if `foo.bar` doesn't have the `@[to_additive]` attribute, then we fail with a nice error message. We could potentially support this behavior, but it doesn't seem that worthwhile and it would require changing a couple low-level definitions that `@[to_additive]` uses (e.g. by replacing `name.map_prefix` so that it only maps prefixes if the name is `internal`).
* So far this didn't happen in the library yet. There are currently 5 non-internal declarations `foo.bar` that are used in `foo` where `foo` has the `@[to_additive]` attribute, but all of these declarations were already had an additive version `add_foo.bar`.
* These 5 declarations are `[Mon.has_limits.limit_cone, Mon.has_limits.limit_cone_is_limit, con_gen.rel, magma.free_semigroup.r, localization.r]`
* This fixes the error in #8707 and resolves the Zulip thread https://leanprover.zulipchat.com/#narrow/stream/144837-PR-reviews/topic/.238707.20linter.20weirdness
* I also added some documentation / comments to the function `transform_decl_with_prefix_fun_aux`, made it non-private, and rewrote some steps.
