feat(Mathlib/Geometry/Manifold): Riemannian metrics exist II

Mathlib.lean

@@ -4492,6 +4492,7 @@ public import Mathlib.Geometry.Manifold.ContMDiffMFDeriv
 public import Mathlib.Geometry.Manifold.ContMDiffMap
 public import Mathlib.Geometry.Manifold.DerivationBundle
 public import Mathlib.Geometry.Manifold.Diffeomorph
+public import Mathlib.Geometry.Manifold.ExistsRiemannianMetric
 public import Mathlib.Geometry.Manifold.GroupLieAlgebra
 public import Mathlib.Geometry.Manifold.HasGroupoid
 public import Mathlib.Geometry.Manifold.Immersion

Mathlib/Algebra/BigOperators/Finprod.lean

@@ -363,6 +363,18 @@ theorem finprod_eq_prod_of_mulSupport_subset (f : α → M) {s : Finset α} (h :
   simp only [Finset.prod_map, Equiv.coe_toEmbedding]
   congr
 
+@[to_additive]
+theorem map_finprod_of_mulSupport_subset (φ : M →* N) (f : α → M) {s : Finset α}
+    (h : mulSupport f ⊆ s) :
+    ∏ᶠ i, φ (f i) = ∏ i ∈ s, φ (f i) := by
+  apply finprod_eq_prod_of_mulSupport_subset
+  intro j hj
+  simp only [mulSupport, ne_eq] at hj
+  have hf : f j ≠ 1 := by
+    contrapose! hj
+    simp [hj]
+  exact h hf
+
 @[to_additive]
 theorem finprod_eq_prod_of_mulSupport_toFinset_subset (f : α → M) (hf : HasFiniteMulSupport f)
     {s : Finset α} (h : hf.toFinset ⊆ s) : ∏ᶠ i, f i = ∏ i ∈ s, f i :=