expand_exists improvements

[robertylewis]

Reported by @RemyDegenne on Zulip:

I am testing the new expand_exists attribute, which looks like a very useful tool, and I have two remarks/questions:

• The names given to the new lemmas are interpreted as being names in the _root_ namespace. For example, if I have the namespace measure_theory open and use [expand_exists def_name] I do not get measure_theory.def_name, but _root_.def_name. I expected the opposite behaviour. Is it an intentional design decision?
• The attribute creates a def and lemmas, but the def does not have a docstring and the linter complains. Is there a way to give a dosctring when using the attribute?

• Namespacing the new declarations can be done mimicking the logic of to_additive.
• Doc strings can also be taken with approximately the syntax of to_additive. This is a little ugly/tricky to parse, so as a stopgap (or permanently, alongside this solution), we should mention add_decl_doc in the doc string for expand_exists.

@0x182d4454fb211940 are you interested in taking on these feature requests?

[0x182d4454fb211940]

Yeah I'll be happy to work on this. I'll start when I have some free time (likely tomorrow).