Autogenerating `differentiable.exp` etc

Stream: metaprogramming / tactics

[Yury G. Kudryashov]

I want to write a tactic (a command and/or an attribute) that will autogenerate lemmas like docs#differentiable.cexp from docs#complex.has_deriv_at_exp

[Yury G. Kudryashov]

Any hints will be very welcome.

[Rob Lewis]

What are the parameters here? Should it work when exp is changed to a different function? Or for the different differentiability statements below?

[Rob Lewis]

One possible example to follow is the is_poly attribute from the Witt vector project. You apply it to a theorem and it derives some related theorems in different forms, basically what you're looking for. https://github.com/leanprover-community/mathlib/blob/master/src/ring_theory/witt_vector/is_poly.lean#L444

[Rob Lewis]

It might not be a perfect comparison though.

[Yury G. Kudryashov]

Yes, it should work for different infinitely smooth functions. Ideally, it should also work with functions like log automatically adding ≠ 0 assumptions but this is not required for the first version of the attribute.