difficulties with `hasFTaylorSeriesUpToOn_succ_iff_right`

Stream: mathlib4

[Kim Morrison]

I'm having trouble fixing the proof of src#hasFTaylorSeriesUpToOn_succ_iff_right in Mathlib/Analysis/Calculus/ContDiff/Defs.lean on the lean-pr-testing-4119 branch. (We're keen to get lean#4119 in soon, as it fixes a bunch of longstanding typeclass inference bugs.)

I'm probably done looking at this branch until after the weekend --- but I'm wondering if anyone would be interested in robustifying the proof on master in any case (and perhaps magically solving my problem).

There's a slightly scary section

        have :
          HasFDerivWithinAt ((continuousMultilinearCurryRightEquiv' 𝕜 m E F).symm ∘ (p · m.succ))
            ((p x).shift m.succ).curryLeft s x := Htaylor.fderivWithin _ A x hx
        rw [LinearIsometryEquiv.comp_hasFDerivWithinAt_iff'] at this
        convert this

in which we are making Lean do quite a lot of work both inferring implicit arguments, and then all the unification that goes into a convert. It's not terrible as proofs go, but I thought I would advertise this as one where I'd love to see a refactor that relies more on explicit terms and rewrites, and less on inference and unification. :-)

If anyone is feeling particularly keen, coming up with a sane proof that still works on the lean-pr-testing-4119 branch would be even better!

[Matthew Ballard]

Does less insane count as sane?

[Yury G. Kudryashov]

I had trouble porting this file (AFAIR, you've fixed some of the issues).