path to calculus

Stream: mathlib4

[Scott Morrison]

@Patrick Massot is eager to have the basics of calculus ported, so he can restore the chapter on calculus and teach from it starting tomorrow. :-) (Not really tomorrow; the MSRI summer school starts tomorrow but presumably it is not calculus on day 1.)

The target is https://leanprover-community.github.io/mathlib-port-status/file/analysis/special_functions/trigonometric/deriv

We have https://github.com/leanprover-community/mathlib4/pull/4642, which is building, but is owned by Yury and he hasn't had a chance to see the latest changes, so I haven't merged it. Reviews, however, are welcome.

Stacked on top of that is https://github.com/leanprover-community/mathlib4/pull/4651, which is still undergoing CI but I have working locally. Again, reviews welcome.

It would be great if we can prioritize merging these soon!

[Scott Morrison]

I just opened https://github.com/leanprover-community/mathlib4/pull/4653 for the last step. In this PR I've done the low hanging fruit (i.e. lots of capitalisation), but there are 4 or so broken proofs where we may have to compare against mathlib3. Please feel free to jump in on this one! Reviews welcome.

[Yury G. Kudryashov]

!4#4642 is ready for review.

[Yury G. Kudryashov]

I left 2 comments to !4#4651