PR summary 3666308594

Import changes for modified files

No significant changes to the import graph

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

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

./scripts/technical-debt-metrics.sh pr_summary

Thanks for the help! I had not realised that we usually want either the coe or the apply lemma. Is there a general mathlib rule about which one we prefer?

If I had to make one up, I'd say "when you're fine with either, go for coe" on the grounds that

• replacing the function itself is more powerful, so yields an even simpler result in general
• in some cases, you want to leave the function untouched (so other simp lemmas could apply) --- but still want to simplify an application of the function, in that case use apply

How close is this to the mathlib conventions? (Where would I search for them, if this is documented anywhere?)

I can certainly ask on zulip, if this question is complicated/has a long history.
(Loogling for similar examples, there is certainly not an utterly obvious picture to me.)

Yeah, I think that different conventions are used in different parts of the library. In some cases these differences might actually make sense: maybe in some part of the library you work with the unapplied functions a lot more. But in many cases I think it's mostly arbitrary which one we use.

I agree with the rule "when you're fine with either, go for coe".

This PR/issue depends on:

• [Merged by Bors] - chore(Analysis/Distribution/ContDiffMapSupportedIn): remove _apply le… #31094
  By Dependent Issues (🤖). Happy coding!

bors merge

Pull request successfully merged into master.

Build succeeded:

• Lint style
• Post-Build Step
• Build