This talk presents an upcoming extension to the tactic `fun_prop` that is capable of computing derivatives. More generally, `fun_prop` gains the ability to solve goals with metavariables like `HasFDerivAt k f ?f' x` by finding the appropriate derivative `f'` and providing a proof that it is indeed the derivative. We will show how to correctly set up `fun_prop` for `HasFDerivAt`, demonstrate its usage on simple and more advanced derivative computations, and show how to extend `simp` to simplify expressions involving `fderiv`. At the end, we will discuss how to compute gradients using `HasGradientAt` and point out certain technical difficulties preventing us from actually using `fun_prop` in this case. These difficulties can be mitigated and they have been as part of PhysLib. If time allows, we will briefly discuss the formalization of variational calculus in PhysLib, such as the derivation of Euler-Lagrange equations, and what it would take for `fun_prop` to fully automate these calculations as well.