Abstract differentiation

Stream: new members

[Mr Proof]

I know two ways of defining differentiation simplification rules.
(1) operating on pure functions R→R, e.g. we could define D(sin)=cos, D(fog) = D(g)*D(f)(g) and D(Id^2)=2*Id
(2) operating on applied functions e.g. we could define Diff(sin(x),x) = cos(x) with dummy variables.

I just wondered, are both methods implemented in Mathlib? And if so, is there an easy way to switch from one to the other? And is one generally preferred over the other?

[Yury G. Kudryashov]

We have some lemmas like docs#deriv_pow vs docs#deriv_pow', but in most cases we only simplify deriv f x.