[Merged by Bors] - fix(Analysis/Normed/Group): make instance helpers reducible

[eric-wieser]

Zulip thread

This slightly simplifies two downstream proofs, as a bonus.

---

[mattrobball]

Thanks. Once it is green, please send it off.

bors delegate+

[mathlib-bors]

✌️ eric-wieser can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[eric-wieser]

!bench

[j-loreaux]

I'm confused. I think all of these are marked @[to_additive (attr := reducible)]. Is there a reason that doesn't work and we should prefer abbrev?

[leanprover-bot]

Here are the benchmark results for commit 4bee8c1.
There were no significant changes against commit 65037e3.

[mattrobball]

I missed that some of them had reducible also. We should check that indeed these are indeed reducible as are the additive versions.

[mattrobball]

This doesn't solve the example from Zulip right? Either way, it is a principled change given the caveats in my previous comment.

[mattrobball]

Uh oh. Making a separate AddGroupNorm.toNormedAddCommGroup, tagging it with reducible, and deleting the to_additive on GroupNorm.toNormedCommGroup fixes the original example.

[mattrobball]

Oh ok. to_additive and abbrev don't get along. Using to_additive (attr := reducible) is ok also.

[mattrobball]

@eric-wieser can you change from abbrev to to_additive (attr := reducible) in the appropriate places. Ping me if you want me to look again or merge if you feel confident.

[mattrobball]

!bench

[mattrobball]

@j-loreaux and @alreadydone since you both have carefully looked over this once, would mind doing so again? I want to be sure I didn't miss any def's constructing instances and that I didn't do something silly.

If you know what the best way to fix the broken simp proof in Cauchy integrals too, that would be great!

[leanprover-bot]

Here are the benchmark results for commit 07bf220.
There were no significant changes against commit 65037e3.

[eric-wieser]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style