[Merged by Bors] - chore: add some simp and fun_prop attributes

[fpvandoorn]

• Also add a test file that uses the simp lemmas.
• Add/move the fun_prop lemmas to the compositional lemmas.

Zulip

---

[github-actions]

PR summary 7456389336

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

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

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

The doc-module for script/declarations_diff.sh contains some details about this script.

[grunweg]

Looks innocuous, and useful enough. Two nits; please address before merging. Thanks!
maintainer delegate

[github-actions]

🚀 Pull request has been placed on the maintainer queue by grunweg.

[j-loreaux]

It turns out that these are not actually the most useful lemmas to tag with fun_prop in practice (although doing these doesn't really hurt; I know mainly what you are adding is simp. What you actually want are the compositional forms of all of these lemmas. That is: we actually want things like Differentiable.exp to be marked with fun_prop. While we're here do you mind marking those accordingly?

[fpvandoorn]

It turns out that these are not actually the most useful lemmas to tag with fun_prop in practice (although doing these doesn't really hurt; I know mainly what you are adding is simp. What you actually want are the compositional forms of all of these lemmas. That is: we actually want things like Differentiable.exp to be marked with fun_prop. While we're here do you mind marking those accordingly?

I've noticed that the number of failures of fun_prop actually increases when tracing its output, so I expect it is important not to tag them both for performance reasons.

I applied the fun_prop attributes to the compositional forms only, and therefore I removed some fun_prop attributes in Trigonometric.Deriv.

[j-loreaux]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Lint style
• Build