Argument order inconsistent in Has(M)FDerivAt

Stream: mathlib4

[Michael Rothgang]

Working on lemmas relating mfderiv and fderiv, I noticed the argument order in Has(M)FDerivAt is inconsistent: the former takes arguments like HasFDerivAt f f' x, while the latter takes arguments HasMFDerivAt I I' f x f' --- note the swapped order of $f'$ and $x$. (There's also HasStrictFDerivAt f f' x.) This is a small speed-bump every time I try to adapt a lemma from one setting to the other.

I understand the latter makes writing docs#HasMFDerivAt.mfderiv and docs#ModelWithCorners.hasMFDerivAt more convenient --- at the same time, mathlib should imho optimise for using results, not writing them. I'd be happy to unify these, but which way? (Tossing a coin yielded f f' x.)

[Eric Wieser]

It's not possible to use the f f' x order for the M variants, because the type of f' depends on x