diff --git a/Mathlib/Data/Set/Prod.lean b/Mathlib/Data/Set/Prod.lean
index 69e909d725786..d2458cb60e7a7 100644
--- a/Mathlib/Data/Set/Prod.lean
+++ b/Mathlib/Data/Set/Prod.lean
@@ -1002,3 +1002,21 @@ theorem sumPiEquivProdPi_symm_preimage_univ_pi (π : ι ⊕ ι' → Type*) (t :
   · rintro ⟨h₁, h₂⟩ (i|i) <;> simp <;> apply_assumption
 
 end Equiv
+
+namespace Equiv.Set
+
+/-- The canonical equivalence between `{a} ×ˢ t` and `t`, considered as types. -/
+def prod_singleton_left {α β : Type*} (a : α) (t : Set β) : ↑({a} ×ˢ t) ≃ ↑t where
+  toFun := fun x ↦ ⟨x.val.snd, (Set.mem_prod.mp x.prop).2⟩
+  invFun := fun b ↦ ⟨(a, b.val), Set.mem_prod.mpr ⟨Set.mem_singleton a, Subtype.mem b⟩⟩
+  left_inv := by simp [Function.LeftInverse]
+  right_inv := by simp [Function.RightInverse, Function.LeftInverse]
+
+/-- The canonical equivalence between `s ×ˢ {b}` and `s`, considered as types. -/
+def prod_singleton_right {α β : Type*} (s : Set α) (b : β) : ↑(s ×ˢ {b}) ≃ ↑s where
+  toFun := fun x ↦ ⟨x.val.fst, (Set.mem_prod.mp x.prop).1⟩
+  invFun := fun a ↦ ⟨(a.val, b), Set.mem_prod.mpr ⟨Subtype.mem a, Set.mem_singleton b⟩⟩
+  left_inv := by simp [Function.LeftInverse]
+  right_inv := by simp [Function.RightInverse, Function.LeftInverse]
+
+end Equiv.Set
diff --git a/Mathlib/Topology/Algebra/InfiniteSum/Basic.lean b/Mathlib/Topology/Algebra/InfiniteSum/Basic.lean
index e8f00715ed372..c98206d014a4e 100644
--- a/Mathlib/Topology/Algebra/InfiniteSum/Basic.lean
+++ b/Mathlib/Topology/Algebra/InfiniteSum/Basic.lean
@@ -1284,8 +1284,27 @@ theorem sum_add_tsum_subtype_compl [T2Space α] {f : β → α} (hf : Summable f
   rfl
 #align sum_add_tsum_subtype_compl sum_add_tsum_subtype_compl
 
+lemma HasSum.tsum_fiberwise [T2Space α] {f : β → α} {a : α} (hf : HasSum f a) (g : β → γ) :
+    HasSum (fun c : γ ↦ ∑' b : g ⁻¹' {c}, f b) a :=
+  (((Equiv.sigmaFiberEquiv g).hasSum_iff).mpr hf).sigma <|
+    fun _ ↦ ((hf.summable.subtype _).hasSum_iff).mpr rfl
+
 end UniformGroup
 
+section prod_singleton
+
+variable [AddCommMonoid γ] [TopologicalSpace γ] [T2Space γ]
+
+lemma tsum_setProd_singleton_left (a : α) (t : Set β) (f : α × β → γ) :
+    (∑' x : {a} ×ˢ t, f x) = ∑' b : t, f (a, b) :=
+  (Equiv.Set.prod_singleton_left a t |>.symm.tsum_eq <| ({a} ×ˢ t).restrict f).symm
+
+lemma tsum_setProd_singleton_right (s : Set α) (b : β) (f : α × β → γ) :
+    (∑' x : s ×ˢ {b}, f x) = ∑' a : s, f (a, b) :=
+  (Equiv.Set.prod_singleton_right s b |>.symm.tsum_eq <| (s ×ˢ {b}).restrict f).symm
+
+end prod_singleton
+
 section TopologicalGroup
 
 variable {G : Type*} [TopologicalSpace G] [AddCommGroup G] [TopologicalAddGroup G] {f : α → G}