Riemmanian Metrics Exist

Stream: mathlib4

[Dominic Steinitz]

I've put a proof here: https://github.com/leanprover-community/mathlib4/blob/a43c3744c741f8c65365541d02d6a5e323d6defb/Mathlib/Geometry/Manifold/ExistsRiemannianMetricTangentSpace.lean which is part of this draft PR https://github.com/leanprover-community/mathlib4/pull/33519.

A lot of the changes are those by @Michael Rothgang but my attempts to create a PR against a branch on his repo / branch failed.

It no doubt needs cleaning up and somehow made dependent on other PRs and also generalising before it is acceptable as a mathlib contribution but at least something now exists.