First calculus prerequisites for Rademacher theorem in #7003.

Add a few lemmas that were available for `FDeriv` but not for `Deriv`, weaken assumptions here and there.

Prerequisite for Rademacher's theorem in #7003

We currently have in mathlib the Fréchet derivative, and the derivative of maps defined on the scalar field. In this PR, we introduce another notion, the derivative along a line. It is more elementary (but less well behaved) than the full Fréchet derivative.

The API is essentially copied from the file on the one-dimensional derivative, with a few additions that have proved useful for Rademacher's theorem. The API could definitely be expanded, but it's already heavy... I have put everything in the single file `LineDeriv/Basic.lean`, mimicking the directory structure for `FDeriv` and `Deriv` and leaving open the possibility to add other files in this folder with more API.

Last prerequisite for Rademacher theorem in #7003.

Along the way, we weaken the second-countability assumptions for strong measurability of the derivative and the right derivative.

We prove Rademacher theorem, stating that a Lipschitz function between finite-dimensional real vector spaces is differentiable almost everywhere.

We prove Rademacher theorem, stating that a Lipschitz function between finite-dimensional real vector spaces is differentiable almost everywhere.

We prove Rademacher theorem, stating that a Lipschitz function between finite-dimensional real vector spaces is differentiable almost everywhere.