Move instance to better locations

Author: grunweg

Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean

@@ -936,3 +936,7 @@ theorem FiniteDimensional.of_locallyCompact_manifold
   exact FiniteDimensional.of_locallyCompactSpace 𝕜
 
 end Topology
+
+instance {M : Type*} [TopologicalSpace M] [ChartedSpace H M] {x : M} [FiniteDimensional 𝕜 E] :
+    FiniteDimensional 𝕜 (TangentSpace I x) :=
+  inferInstanceAs (FiniteDimensional 𝕜 E)

Mathlib/Geometry/Manifold/VectorBundle/CovariantDerivative/LeviCivita.lean

@@ -303,12 +303,6 @@ theorem tensorialAt_leviCivitaAuxInner₃
       inner_add_left, inner_add_right]
     ring
 
--- TODO move!
-instance : FiniteDimensional ℝ (TangentSpace I x) := inferInstanceAs (FiniteDimensional ℝ E)
-
--- TODO move!
-instance : CompleteSpace (TangentSpace I x) := FiniteDimensional.complete ℝ _
-
 /-- Almost the function underlying our construction of the Levi-Civita connection:
 this is the desired `(1,1)`-tensor, but without considerations to the junk value when
 applied to non-differentiable vector fields. -/

Mathlib/Geometry/Manifold/VectorBundle/Riemannian.lean

@@ -268,3 +268,14 @@ instance (g : ContMDiffRiemannianMetric IB n F E) :
 end Construction
 
 end Bundle
+
+section
+
+variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] {H : Type*} [TopologicalSpace H]
+  {I : ModelWithCorners ℝ E H} {M : Type*} [TopologicalSpace M] [ChartedSpace H M]
+  [RiemannianBundle (fun (x : M) ↦ TangentSpace I x)]
+
+instance [FiniteDimensional ℝ E] {x : M} : CompleteSpace (TangentSpace I x) :=
+  FiniteDimensional.complete ℝ _
+
+end