tactic for mfderiv

Stream: mathlib4

[Tomas Skrivan]

I would like to extend my automatic differentiation tactic to mfderiv but what scares me is the I' parameter in mfderiv_comp. When give expression mfderiv I I'' (g ∘ f) how am I supposed to figure out what I'?

Maybe I can forget about using mfderiv_comp and only use theorems in their "compositional form"(as I call it infun_prop) like mfderiv_add which does not introduce a new free variable on rhs. However, to generate efficient code(something I care about) I need to properly handle let bindings and for them I'm forced to use some kind of general composition theorem.

I'm also a bit unsure about the statement of mfderiv_add, on lhs mfderiv I (modelWithCornersSelf 𝕜 E') (f + g) z cannot it happen that I would have a product model instead of (modelWithCornersSelf 𝕜 E')? Then I could not apply mfderiv_add.

I have no experience using mfderiv and I would appreciate someone's opinion on how to deal with I' in mfderiv_comp. Is there some reasonable heuristic that would work in 90% cases we care about?