feat(Topology/Algebra/InfiniteSum/Basic): add some lemmas on tsums (#…

…10038)

This is the fifth PR in a sequence that adds auxiliary lemmas from the [EulerProducts](https://github.com/MichaelStollBayreuth/EulerProducts) project to Mathlib.

It adds three lemmas on `tsum`s:
```lean
lemma HasSum.tsum_fiberwise {α β γ : Type*} [AddCommGroup α] [UniformSpace α] [UniformAddGroup α]
    [T2Space α] [RegularSpace α] [CompleteSpace α] {f : β → α}
    {a : α} (hf : HasSum f a) (g : β → γ) :
    HasSum (fun c : γ ↦ ∑' b : g ⁻¹' {c}, f b) a

lemma tsum_setProd_singleton_left {α β γ : Type*} [AddCommMonoid γ] [TopologicalSpace γ] [T2Space γ]
    (a : α) (t : Set β) (f : α × β → γ) : (∑' x : {a} ×ˢ t, f x) = ∑' b : t, f (a, b)

lemma tsum_setProd_singleton_right {α β γ : Type*} [AddCommMonoid γ] [TopologicalSpace γ] [T2Space γ]
    (s : Set α) (b : β) (f : α × β → γ) : (∑' x : s ×ˢ {b}, f x) = ∑' a : s, f (a, b)
```
and the necessary equivalences
```lean
def prod_singleton_left {α β : Type*} (a : α) (t : Set β) : ↑({a} ×ˢ t) ≃ ↑t

def prod_singleton_right {α β : Type*} (s : Set α) (b : β) : ↑(s ×ˢ {b}) ≃ ↑s
```

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

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}