Out of scope comment

Author: idontgetoutmuch

Mathlib/Algebra/BigOperators/Finprod.lean

@@ -362,6 +362,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 : (mulSupport f).Finite)
     {s : Finset α} (h : hf.toFinset ⊆ s) : ∏ᶠ i, f i = ∏ i ∈ s, f i :=

Mathlib/Geometry/Manifold/ExistsRiemannianMetric.lean

@@ -357,19 +357,7 @@ def g_global_bilin_aux (f : SmoothPartitionOfUnity B IB B) (p : B) :
     E p →L[ℝ] (E p →L[ℝ] ℝ) :=
   ∑ᶠ (j : B), (f j) p • g_bilin_aux F j p
 
-lemma finsum_image_eq_sum {B E F : Type*} [AddCommMonoid E] [AddCommMonoid F]
-  (φ : E →+ F) {f : B → E} {h_fin : Finset B}
-  (h1 : Function.support f ⊆ h_fin) :
-  ∑ᶠ j, φ (f j) = ∑ j ∈ h_fin, φ (f j) := by
-    apply finsum_eq_sum_of_support_subset
-    intro j hj
-    simp only [Function.mem_support, ne_eq] at hj
-    have hf : f j ≠ 0 := by
-      contrapose! hj
-      simpa using (map_zero φ).symm ▸ congrArg φ hj
-    exact h1 hf
-
-def evalAt (b : B) (v w : E b) :
+private def evalAt (b : B) (v w : E b) :
     (E b →L[ℝ] (E b →L[ℝ] ℝ)) →+ ℝ where
   toFun f := (f.toFun v).toFun w
   map_zero' := by simp
@@ -401,11 +389,12 @@ lemma riemannian_metric_symm_aux (f : SmoothPartitionOfUnity B IB B) (b : B)
   calc ((∑ j ∈ h1.toFinset, (f j) b • g_bilin_aux F j b).toFun v).toFun w
       = ∑ j ∈ h1.toFinset, (((f j) b • g_bilin_aux F j b).toFun v).toFun w := (h3 v w).symm
     _ = ∑ᶠ (j : B), (((f j) b • g_bilin_aux F j b).toFun v).toFun w :=
-          (finsum_image_eq_sum (evalAt b v w) (f := h) (h_fin := h1.toFinset) h2).symm
+          (map_finsum_of_support_subset (φ := (evalAt b v w : (E b →L[ℝ] (E b →L[ℝ] ℝ)) →+ ℝ))
+            (f := h) (s := h1.toFinset) h2).symm
     _ = ∑ᶠ (j : B), (((f j) b • g_bilin_aux F j b).toFun w).toFun v :=
           finsum_congr (fun j ↦ congrArg (HMul.hMul ((f j) b)) (g_bilin_symm_aux j b v w))
     _ = ∑ j ∈ h1.toFinset, (((f j) b • g_bilin_aux F j b).toFun w).toFun v :=
-          finsum_image_eq_sum (evalAt b w v) (f := h) (h_fin := h1.toFinset) h2
+          map_finsum_of_support_subset (evalAt b w v) (f := h) (s := h1.toFinset) h2
     _ = ((∑ j ∈ h1.toFinset, (f j) b • g_bilin_aux F j b).toFun w).toFun v := h3 w v
 
 lemma riemannian_metric_pos_def_aux (f : SmoothPartitionOfUnity B IB B)
@@ -438,7 +427,7 @@ lemma riemannian_metric_pos_def_aux (f : SmoothPartitionOfUnity B IB B)
     exact mul_ne_zero_iff.mp (mul_ne_zero_iff.mpr hx) |>.1
   have hb : ∑ᶠ i, h' i =
             ∑ j ∈ h1.toFinset, (((f j) b • g_bilin_aux F j b).toFun v).toFun v :=
-    (finsum_image_eq_sum (evalAt b v v) (f := h) (h_fin := h1.toFinset) h3) ▸ rfl
+    (map_finsum_of_support_subset (evalAt b v v) (f := h) (s := h1.toFinset) h3) ▸ rfl
   exact lt_of_lt_of_eq (finsum_pos h7 h8 h9) (hb.trans h2)
 
 lemma riemannian_unit_ball_bounded_aux (f : SmoothPartitionOfUnity B IB B)