Instance synthesis issue working with Riemannian bundles

Stream: lean4

[Michael Rothgang]

Sébastien Gouëzel said:

Wow, Levi-Civita, that's awesome! Did the Riemannian manifold definition work well for you, or did you have to tweak the definition somehow to make it better?

I just hit a first roadblock, working with the new definition: trying to prove lemmas of the form "given a C^n metric, the point-wise scalar product of two MDifferentiable sections is MDifferentiable in #26921 yields an error that doesn't make sense to me. Can you take a look and tell me if I'm doing something wrong?

[Sébastien Gouëzel]

It's because the typeclass assumption h is not available in the proof, because the variable n is not present. You should replace the typeclass with

  [h : IsContMDiffRiemannianBundle IB 1 F E]

[Michael Rothgang]

:bulb: Yes, of course! Fixed, and thanks a lot!