3709 FTC again

Stream: PR reviews

[Yury G. Kudryashov]

#3709 is ready for review. I'm writing about this here because it's on the second page.

[Johan Commelin]

This is a really cool milestone!

[Johan Commelin]

@Patrick Massot @Sebastien Gouezel there's work for you (-;

[Yury G. Kudryashov]

The file is long because I repeat many lemmas in slightly different settings (left endpoint, right, both; has_strict_(f)deriv_at, has_(f)deriv_at, has_(f)deriv_within_at, (f)deriv(_within) = ...). It would be nice to generate half of the lemmas using some meta def but I'm not good enough at this.

[Patrick Massot]

I think Sébastien is on it (the review work, not metaprogramming).