I don't know how to fix the conflicts. Just merging naively led to many errors.

Thanks for your contribution. It's great to see that the existence of Riemannian metrics for tangent bundles is now sorry-free. I have two types of questions about this PR.
(1) Which files contain the "real work"? This PR contains many files, some of which I pasted in that seem unused now. Where's the main result; which files do you actually use? (Before merging a PR, we'd certainly like to only merge the files we need. For instance, instead of importing Elaborators.lean, you should be able to use Notation.lean.)
(2) It would be good to generalise this argument to arbitrary vector bundles. Mathematically, there should be no meaningful difference. Would you like help with that/what happens when you try to do so?

Thanks for your contribution. It's great to see that the existence of Riemannian metrics for tangent bundles is now sorry-free. I have two types of questions about this PR. (1) Which files contain the "real work"? This PR contains many files, some of which I pasted in that seem unused now. Where's the main result; which files do you actually use? (Before merging a PR, we'd certainly like to only merge the files we need. For instance, instead of importing Elaborators.lean, you should be able to use Notation.lean.)

The theorem is here:

Great question and I just tried my file with the latest version of master (well of 19 hours ago) and the only thing that seems to be missing is contMDiff_totalSpace_weighted_sum_of_local_sections. Perhaps I should try against the branch which contains this? If that works I am inclined to just copy my file and lose my git history (I am the only one who might ever care about it). What do you think?

EDIT: @grunweg you removed the theorem I rely upon in this commit: 4d14161. What should I do?

(2) It would be good to generalise this argument to arbitrary vector bundles. Mathematically, there should be no meaningful difference. Would you like help with that/what happens when you try to do so?

Yes please but I do use the fact that the trivialisation of the bundle of bilinear forms is essentially given by the trivialisation of the tangent bundle. Maybe this can be generalised but off the top of my head, I don't know how.

To get the conversation going, restoring contMDiff_totalSpace_weighted_sum_of_local_sections (by reverting 4d14161) and adding just your file seems like a fine start --- especially if this allows for a PR with clean diff.

(2) It would be good to generalise this argument to arbitrary vector bundles. Mathematically, there should be no meaningful difference. Would you like help with that/what happens when you try to do so?

Yes please but I do use the fact that the trivialisation of the bundle of bilinear forms is essentially given by the trivialisation of the tangent bundle. Maybe this can be generalised but off the top of my head, I don't know how.

I would think the analogous fact is true in any vector bundle (and this would be a useful lemma to have, independently of this PR --- i.e., a good pre-requisite PR).

To get the conversation going, restoring contMDiff_totalSpace_weighted_sum_of_local_sections (by reverting 4d14161) and adding just your file seems like a fine start --- especially if this allows for a PR with clean diff.

I just tried adding it back as an edit and everything works which is great. I can easily add back in the commit so that the git history is kept.

(2) It would be good to generalise this argument to arbitrary vector bundles. Mathematically, there should be no meaningful difference. Would you like help with that/what happens when you try to do so?

Yes please but I do use the fact that the trivialisation of the bundle of bilinear forms is essentially given by the trivialisation of the tangent bundle. Maybe this can be generalised but off the top of my head, I don't know how.

I would think the analogous fact is true in any vector bundle (and this would be a useful lemma to have, independently of this PR --- i.e., a good pre-requisite PR).

Ok let me think about that.

Superseded by #33714.