diff --git a/Mathlib/Geometry/Manifold/Algebra/Monoid.lean b/Mathlib/Geometry/Manifold/Algebra/Monoid.lean
index 8e319601d783c..c05bcc0029a51 100644
--- a/Mathlib/Geometry/Manifold/Algebra/Monoid.lean
+++ b/Mathlib/Geometry/Manifold/Algebra/Monoid.lean
@@ -299,16 +299,39 @@ instance : ContinuousMapClass (SmoothMonoidMorphism I I' G G') G G' where
 
 end Monoid
 
+/-! ### Differentiability of finite point-wise sums and products
+
+  Finite point-wise products (resp. sums) of differentiable/smooth functions `M → G` (at `x`/on `s`)
+  into a commutative monoid `G` are differentiable/smooth at `x`/on `s`. -/
 section CommMonoid
 
+open Function
 open scoped BigOperators
 
-variable {ι 𝕜 : Type*} [NontriviallyNormedField 𝕜] {H : Type*} [TopologicalSpace H] {E : Type*}
-  [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type*} [CommMonoid G]
-  [TopologicalSpace G] [ChartedSpace H G] [SmoothMul I G] {E' : Type*} [NormedAddCommGroup E']
-  [NormedSpace 𝕜 E'] {H' : Type*} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
-  {M : Type*} [TopologicalSpace M] [ChartedSpace H' M] {s : Set M} {x : M} {t : Finset ι}
-  {f : ι → M → G} {n : ℕ∞} {p : ι → Prop}
+variable {ι 𝕜 : Type*} [NontriviallyNormedField 𝕜] {H : Type*} [TopologicalSpace H]
+  {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H}
+  {G : Type*} [CommMonoid G] [TopologicalSpace G] [ChartedSpace H G] [SmoothMul I G]
+  {E' : Type*} [NormedAddCommGroup E'] [NormedSpace 𝕜 E']
+  {H' : Type*} [TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
+  {M : Type*} [TopologicalSpace M] [ChartedSpace H' M]
+  {s : Set M} {x x₀ : M} {t : Finset ι} {f : ι → M → G} {n : ℕ∞} {p : ι → Prop}
+
+@[to_additive]
+theorem ContMDiffWithinAt.prod (h : ∀ i ∈ t, ContMDiffWithinAt I' I n (f i) s x₀) :
+    ContMDiffWithinAt I' I n (fun x ↦ ∏ i in t, f i x) s x₀ := by
+  classical
+  induction' t using Finset.induction_on with i K iK IH
+  · simp [contMDiffWithinAt_const]
+  · simp only [iK, Finset.prod_insert, not_false_iff]
+    exact (h _ (Finset.mem_insert_self i K)).mul (IH fun j hj ↦ h _ <| Finset.mem_insert_of_mem hj)
+
+@[to_additive]
+theorem contMDiffWithinAt_finprod (lf : LocallyFinite fun i ↦ mulSupport <| f i) {x₀ : M}
+    (h : ∀ i, ContMDiffWithinAt I' I n (f i) s x₀) :
+    ContMDiffWithinAt I' I n (fun x ↦ ∏ᶠ i, f i x) s x₀ :=
+  let ⟨_I, hI⟩ := finprod_eventually_eq_prod lf x₀
+  (ContMDiffWithinAt.prod fun i _hi ↦ h i).congr_of_eventuallyEq
+    (eventually_nhdsWithin_of_eventually_nhds hI) hI.self_of_nhds
 
 @[to_additive]
 theorem contMDiffWithinAt_finset_prod' (h : ∀ i ∈ t, ContMDiffWithinAt I' I n (f i) s x) :
@@ -318,26 +341,6 @@ theorem contMDiffWithinAt_finset_prod' (h : ∀ i ∈ t, ContMDiffWithinAt I' I
 #align cont_mdiff_within_at_finset_prod' contMDiffWithinAt_finset_prod'
 #align cont_mdiff_within_at_finset_sum' contMDiffWithinAt_finset_sum'
 
-@[to_additive]
-theorem contMDiffAt_finset_prod' (h : ∀ i ∈ t, ContMDiffAt I' I n (f i) x) :
-    ContMDiffAt I' I n (∏ i in t, f i) x :=
-  contMDiffWithinAt_finset_prod' h
-#align cont_mdiff_at_finset_prod' contMDiffAt_finset_prod'
-#align cont_mdiff_at_finset_sum' contMDiffAt_finset_sum'
-
-@[to_additive]
-theorem contMDiffOn_finset_prod' (h : ∀ i ∈ t, ContMDiffOn I' I n (f i) s) :
-    ContMDiffOn I' I n (∏ i in t, f i) s := fun x hx =>
-  contMDiffWithinAt_finset_prod' fun i hi => h i hi x hx
-#align cont_mdiff_on_finset_prod' contMDiffOn_finset_prod'
-#align cont_mdiff_on_finset_sum' contMDiffOn_finset_sum'
-
-@[to_additive]
-theorem contMDiff_finset_prod' (h : ∀ i ∈ t, ContMDiff I' I n (f i)) :
-    ContMDiff I' I n (∏ i in t, f i) := fun x => contMDiffAt_finset_prod' fun i hi => h i hi x
-#align cont_mdiff_finset_prod' contMDiff_finset_prod'
-#align cont_mdiff_finset_sum' contMDiff_finset_sum'
-
 @[to_additive]
 theorem contMDiffWithinAt_finset_prod (h : ∀ i ∈ t, ContMDiffWithinAt I' I n (f i) s x) :
     ContMDiffWithinAt I' I n (fun x => ∏ i in t, f i x) s x := by
@@ -346,6 +349,25 @@ theorem contMDiffWithinAt_finset_prod (h : ∀ i ∈ t, ContMDiffWithinAt I' I n
 #align cont_mdiff_within_at_finset_prod contMDiffWithinAt_finset_prod
 #align cont_mdiff_within_at_finset_sum contMDiffWithinAt_finset_sum
 
+@[to_additive]
+theorem ContMDiffAt.prod (h : ∀ i ∈ t, ContMDiffAt I' I n (f i) x₀) :
+    ContMDiffAt I' I n (fun x ↦ ∏ i in t, f i x) x₀ := by
+  simp only [← contMDiffWithinAt_univ] at *
+  exact ContMDiffWithinAt.prod h
+
+@[to_additive]
+theorem contMDiffAt_finprod
+    (lf : LocallyFinite fun i ↦ mulSupport <| f i) (h : ∀ i, ContMDiffAt I' I n (f i) x₀) :
+    ContMDiffAt I' I n (fun x ↦ ∏ᶠ i, f i x) x₀ :=
+  contMDiffWithinAt_finprod lf h
+
+@[to_additive]
+theorem contMDiffAt_finset_prod' (h : ∀ i ∈ t, ContMDiffAt I' I n (f i) x) :
+    ContMDiffAt I' I n (∏ i in t, f i) x :=
+  contMDiffWithinAt_finset_prod' h
+#align cont_mdiff_at_finset_prod' contMDiffAt_finset_prod'
+#align cont_mdiff_at_finset_sum' contMDiffAt_finset_sum'
+
 @[to_additive]
 theorem contMDiffAt_finset_prod (h : ∀ i ∈ t, ContMDiffAt I' I n (f i) x) :
     ContMDiffAt I' I n (fun x => ∏ i in t, f i x) x :=
@@ -353,6 +375,19 @@ theorem contMDiffAt_finset_prod (h : ∀ i ∈ t, ContMDiffAt I' I n (f i) x) :
 #align cont_mdiff_at_finset_prod contMDiffAt_finset_prod
 #align cont_mdiff_at_finset_sum contMDiffAt_finset_sum
 
+@[to_additive]
+theorem contMDiffOn_finprod
+    (lf : LocallyFinite fun i ↦ Function.mulSupport <| f i) (h : ∀ i, ContMDiffOn I' I n (f i) s) :
+    ContMDiffOn I' I n (fun x ↦ ∏ᶠ i, f i x) s := fun x hx ↦
+  contMDiffWithinAt_finprod lf fun i ↦ h i x hx
+
+@[to_additive]
+theorem contMDiffOn_finset_prod' (h : ∀ i ∈ t, ContMDiffOn I' I n (f i) s) :
+    ContMDiffOn I' I n (∏ i in t, f i) s := fun x hx =>
+  contMDiffWithinAt_finset_prod' fun i hi => h i hi x hx
+#align cont_mdiff_on_finset_prod' contMDiffOn_finset_prod'
+#align cont_mdiff_on_finset_sum' contMDiffOn_finset_sum'
+
 @[to_additive]
 theorem contMDiffOn_finset_prod (h : ∀ i ∈ t, ContMDiffOn I' I n (f i) s) :
     ContMDiffOn I' I n (fun x => ∏ i in t, f i x) s := fun x hx =>
@@ -360,6 +395,17 @@ theorem contMDiffOn_finset_prod (h : ∀ i ∈ t, ContMDiffOn I' I n (f i) s) :
 #align cont_mdiff_on_finset_prod contMDiffOn_finset_prod
 #align cont_mdiff_on_finset_sum contMDiffOn_finset_sum
 
+@[to_additive]
+theorem ContMDiff.prod (h : ∀ i ∈ t, ContMDiff I' I n (f i)) :
+    ContMDiff I' I n fun x ↦ ∏ i in t, f i x :=
+  fun x ↦ ContMDiffAt.prod fun j hj ↦ h j hj x
+
+@[to_additive]
+theorem contMDiff_finset_prod' (h : ∀ i ∈ t, ContMDiff I' I n (f i)) :
+    ContMDiff I' I n (∏ i in t, f i) := fun x => contMDiffAt_finset_prod' fun i hi => h i hi x
+#align cont_mdiff_finset_prod' contMDiff_finset_prod'
+#align cont_mdiff_finset_sum' contMDiff_finset_sum'
+
 @[to_additive]
 theorem contMDiff_finset_prod (h : ∀ i ∈ t, ContMDiff I' I n (f i)) :
     ContMDiff I' I n fun x => ∏ i in t, f i x := fun x =>
@@ -368,31 +414,33 @@ theorem contMDiff_finset_prod (h : ∀ i ∈ t, ContMDiff I' I n (f i)) :
 #align cont_mdiff_finset_sum contMDiff_finset_sum
 
 @[to_additive]
-theorem smoothWithinAt_finset_prod' (h : ∀ i ∈ t, SmoothWithinAt I' I (f i) s x) :
-    SmoothWithinAt I' I (∏ i in t, f i) s x :=
-  contMDiffWithinAt_finset_prod' h
-#align smooth_within_at_finset_prod' smoothWithinAt_finset_prod'
-#align smooth_within_at_finset_sum' smoothWithinAt_finset_sum'
+theorem contMDiff_finprod (h : ∀ i, ContMDiff I' I n (f i))
+    (hfin : LocallyFinite fun i => mulSupport (f i)) : ContMDiff I' I n fun x => ∏ᶠ i, f i x :=
+  fun x ↦ contMDiffAt_finprod hfin fun i ↦ h i x
+#align cont_mdiff_finprod contMDiff_finprod
+#align cont_mdiff_finsum contMDiff_finsum
 
 @[to_additive]
-theorem smoothAt_finset_prod' (h : ∀ i ∈ t, SmoothAt I' I (f i) x) :
-    SmoothAt I' I (∏ i in t, f i) x :=
-  contMDiffAt_finset_prod' h
-#align smooth_at_finset_prod' smoothAt_finset_prod'
-#align smooth_at_finset_sum' smoothAt_finset_sum'
+theorem contMDiff_finprod_cond (hc : ∀ i, p i → ContMDiff I' I n (f i))
+    (hf : LocallyFinite fun i => mulSupport (f i)) :
+    ContMDiff I' I n fun x => ∏ᶠ (i) (_ : p i), f i x := by
+  simp only [← finprod_subtype_eq_finprod_cond]
+  exact contMDiff_finprod (fun i => hc i i.2) (hf.comp_injective Subtype.coe_injective)
+#align cont_mdiff_finprod_cond contMDiff_finprod_cond
+#align cont_mdiff_finsum_cond contMDiff_finsum_cond
 
 @[to_additive]
-theorem smoothOn_finset_prod' (h : ∀ i ∈ t, SmoothOn I' I (f i) s) :
-    SmoothOn I' I (∏ i in t, f i) s :=
-  contMDiffOn_finset_prod' h
-#align smooth_on_finset_prod' smoothOn_finset_prod'
-#align smooth_on_finset_sum' smoothOn_finset_sum'
+theorem smoothAt_finprod
+    (lf : LocallyFinite fun i ↦ mulSupport <| f i) (h : ∀ i, SmoothAt I' I (f i) x₀) :
+    SmoothAt I' I (fun x ↦ ∏ᶠ i, f i x) x₀ :=
+  contMDiffWithinAt_finprod lf h
 
 @[to_additive]
-theorem smooth_finset_prod' (h : ∀ i ∈ t, Smooth I' I (f i)) : Smooth I' I (∏ i in t, f i) :=
-  contMDiff_finset_prod' h
-#align smooth_finset_prod' smooth_finset_prod'
-#align smooth_finset_sum' smooth_finset_sum'
+theorem smoothWithinAt_finset_prod' (h : ∀ i ∈ t, SmoothWithinAt I' I (f i) s x) :
+    SmoothWithinAt I' I (∏ i in t, f i) s x :=
+  contMDiffWithinAt_finset_prod' h
+#align smooth_within_at_finset_prod' smoothWithinAt_finset_prod'
+#align smooth_within_at_finset_sum' smoothWithinAt_finset_sum'
 
 @[to_additive]
 theorem smoothWithinAt_finset_prod (h : ∀ i ∈ t, SmoothWithinAt I' I (f i) s x) :
@@ -401,6 +449,13 @@ theorem smoothWithinAt_finset_prod (h : ∀ i ∈ t, SmoothWithinAt I' I (f i) s
 #align smooth_within_at_finset_prod smoothWithinAt_finset_prod
 #align smooth_within_at_finset_sum smoothWithinAt_finset_sum
 
+@[to_additive]
+theorem smoothAt_finset_prod' (h : ∀ i ∈ t, SmoothAt I' I (f i) x) :
+    SmoothAt I' I (∏ i in t, f i) x :=
+  contMDiffAt_finset_prod' h
+#align smooth_at_finset_prod' smoothAt_finset_prod'
+#align smooth_at_finset_sum' smoothAt_finset_sum'
+
 @[to_additive]
 theorem smoothAt_finset_prod (h : ∀ i ∈ t, SmoothAt I' I (f i) x) :
     SmoothAt I' I (fun x => ∏ i in t, f i x) x :=
@@ -408,6 +463,13 @@ theorem smoothAt_finset_prod (h : ∀ i ∈ t, SmoothAt I' I (f i) x) :
 #align smooth_at_finset_prod smoothAt_finset_prod
 #align smooth_at_finset_sum smoothAt_finset_sum
 
+@[to_additive]
+theorem smoothOn_finset_prod' (h : ∀ i ∈ t, SmoothOn I' I (f i) s) :
+    SmoothOn I' I (∏ i in t, f i) s :=
+  contMDiffOn_finset_prod' h
+#align smooth_on_finset_prod' smoothOn_finset_prod'
+#align smooth_on_finset_sum' smoothOn_finset_sum'
+
 @[to_additive]
 theorem smoothOn_finset_prod (h : ∀ i ∈ t, SmoothOn I' I (f i) s) :
     SmoothOn I' I (fun x => ∏ i in t, f i x) s :=
@@ -415,6 +477,12 @@ theorem smoothOn_finset_prod (h : ∀ i ∈ t, SmoothOn I' I (f i) s) :
 #align smooth_on_finset_prod smoothOn_finset_prod
 #align smooth_on_finset_sum smoothOn_finset_sum
 
+@[to_additive]
+theorem smooth_finset_prod' (h : ∀ i ∈ t, Smooth I' I (f i)) : Smooth I' I (∏ i in t, f i) :=
+  contMDiff_finset_prod' h
+#align smooth_finset_prod' smooth_finset_prod'
+#align smooth_finset_sum' smooth_finset_sum'
+
 @[to_additive]
 theorem smooth_finset_prod (h : ∀ i ∈ t, Smooth I' I (f i)) :
     Smooth I' I fun x => ∏ i in t, f i x :=
@@ -422,26 +490,6 @@ theorem smooth_finset_prod (h : ∀ i ∈ t, Smooth I' I (f i)) :
 #align smooth_finset_prod smooth_finset_prod
 #align smooth_finset_sum smooth_finset_sum
 
-open Function Filter
-
-@[to_additive]
-theorem contMDiff_finprod (h : ∀ i, ContMDiff I' I n (f i))
-    (hfin : LocallyFinite fun i => mulSupport (f i)) : ContMDiff I' I n fun x => ∏ᶠ i, f i x := by
-  intro x
-  rcases finprod_eventually_eq_prod hfin x with ⟨s, hs⟩
-  exact (contMDiff_finset_prod (fun i _ => h i) x).congr_of_eventuallyEq hs
-#align cont_mdiff_finprod contMDiff_finprod
-#align cont_mdiff_finsum contMDiff_finsum
-
-@[to_additive]
-theorem contMDiff_finprod_cond (hc : ∀ i, p i → ContMDiff I' I n (f i))
-    (hf : LocallyFinite fun i => mulSupport (f i)) :
-    ContMDiff I' I n fun x => ∏ᶠ (i) (_ : p i), f i x := by
-  simp only [← finprod_subtype_eq_finprod_cond]
-  exact contMDiff_finprod (fun i => hc i i.2) (hf.comp_injective Subtype.coe_injective)
-#align cont_mdiff_finprod_cond contMDiff_finprod_cond
-#align cont_mdiff_finsum_cond contMDiff_finsum_cond
-
 @[to_additive]
 theorem smooth_finprod (h : ∀ i, Smooth I' I (f i))
     (hfin : LocallyFinite fun i => mulSupport (f i)) : Smooth I' I fun x => ∏ᶠ i, f i x :=