how to express and use derivatives in Lean4

Stream: new members

[oishi]

I've been trying to convert the proof from the link into Lean4, and I've encountered some issues. I don't know how to properly express and use derivatives in Lean4. The materials I've found related to derivatives are mostly abstract forms, and I haven't found examples with specific functions like in the link. Can anyone help me? Thank you very much!

How do you prove that [math]\sum_ {k=0} ^n (-1) ^k {n \choose k} (n-k) ^n =n! [/math]? - Quora

[Daniel Weber]

Have you read https://leanprover-community.github.io/mathematics_in_lean/C10_Differential_Calculus.html ?