[Merged by Bors] - feat(to_additive): unfold lemmas generated by simp

[fpvandoorn]

• This removes a bunch of hacky code
• Thanks to @kmill for the idea
• Also fix a bug in the implementation of @[to_additive (attr := to_additive, x)]
• The removed test tested for an implementation detail. The rest of the test file (and Mathlib) still passes, which shows that it still works as desired.

---

[github-actions]

PR summary 360d18f00a

Import changes for modified files

Dependency changes

File	Base Count	Head Count	Change
Mathlib.Lean.Name	3	4	+1 (+33.33%)
Mathlib.Tactic.ToAdditive	34	39	+5 (+14.71%)

Import changes for all files

Files	Import difference
Too many changes (4249)!

---

Declarations diff

+ Lean.Meta.unfoldAuxLemmas
+ Lean.Name.isAuxLemma
- addSimpAttr
- addSimpAttrFromSyntax
- addSimpTheorem'
- mkSimpTheoremsFromConst'

You can run this locally as follows

## summary with just the declaration names:
./scripts/no_lost_declarations.sh short <optional_commit>

## more verbose report:
./scripts/no_lost_declarations.sh <optional_commit>

[kmill]

Looks good to me. The best kind of feature is one that's implemented by mostly deleting code!

For due diligence, I'll mention that I think the whole auxLemma business is about trying to avoid re-typechecking proof terms, so unfolding auxLemmas defeats this optimization, however I don't believe that simp's auxLemmas tend to be very complicated.

[eric-wieser]

What's the "feat" here? Is there any visible behavior change, or is this just internal cleanup?

[eric-wieser]

!bench

[leanprover-bot]

Here are the benchmark results for commit 360d18f.
There were no significant changes against commit 5b4d457.

[fpvandoorn]

See the issues that reference this: one feature request there is now fixed, another bug might be fixed (haven't tested)

[kim-em]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Lint style