help wanted porting Analysis.Calculus.ContDiffDef !4#4256

Stream: mathlib4

[Yury G. Kudryashov]

Hi, there is one timeout left in this file. I tried to fix it several times by moving parts to a new lemma but even some simple-looking lemmas fail to elaborate.

[Yury G. Kudryashov]

Example of what fails (and thus I'm not 100% sure that I got it right):

variable {𝕜 : Type _} [NontriviallyNormedField 𝕜]
  {E : Type _} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
  {G : Type _} [NormedAddCommGroup G] [NormedSpace 𝕜 G] {n : ℕ}

theorem uncurryLeft_uncurryRight (f : E →L[𝕜] (E [×n]→L[𝕜] (E →L[𝕜] G))) :
    f.uncurryLeft.uncurryRight =
      (continuousMultilinearCurryRightEquiv' 𝕜 n E G ∘L f).uncurryLeft := by
  _

[Yury G. Kudryashov]

UPD: I fixed universes, now I have more failures.