feat(Algebra/InfiniteSum): drop [T2Space _] assumption (#10060)

* Add `CanLift` instance for `Function.Embedding`.
* Assume `Injective i` instead of an equivalent condition in `hasSum_iff_hasSum_of_ne_zero_bij`.
* Add `tsum_eq_sum'`, a version of `tsum_eq_sum` that explicitly mentions `support f`.
* Add `Function.Injective.tsum_eq`, use it to drop `[T2Space _]` assumption in
  - `Equiv.tsum_eq`;
  - `tsum_subtype_eq_of_support_subset`;
  - `tsum_subtype_support`;
  - `tsum_subtype`;
  - `tsum_univ`;
  - `tsum_image`;
  - `tsum_range`;
  - `tsum_setElem_eq_tsum_setElem_diff`;
  - `tsum_eq_tsum_diff_singleton`;
  - `tsum_eq_tsum_of_ne_zero_bij`;
  - `Equiv.tsum_eq_tsum_of_support`;
  - `tsum_extend_zero`;
* Golf some proofs.
* Drop `Equiv.Set.prod_singleton_left` and `Equiv.Set.prod_singleton_right` added in #10038.
  @MichaelStollBayreuth, if you need these `Equiv`s, then please

  - restore them in `Logic/Equiv/Set`, not in `Data/Set/Prod`;
  - call them `Equiv.Set.singletonProd` and `Equiv.Set.prodSingleton`, following the `lowerCamelCase` naming convention for `def`s;
  - reuse the existing `Equiv.Set.prod` and `Equiv.prodUnique`/`Equiv.uniqueProd` in the definitions.

Author: urkud

Mathlib/Data/Set/Prod.lean

@@ -1002,21 +1002,3 @@ 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/Logic/Embedding/Basic.lean

@@ -47,6 +47,9 @@ theorem exists_surjective_iff :
   ⟨fun ⟨f, h⟩ ↦ ⟨⟨f⟩, ⟨⟨_, injective_surjInv h⟩⟩⟩, fun ⟨h, ⟨e⟩⟩ ↦ (nonempty_fun.mp h).elim
     (fun _ ↦ ⟨isEmptyElim, (isEmptyElim <| e ·)⟩) fun _ ↦ ⟨_, invFun_surjective e.inj'⟩⟩
 
+instance : CanLift (α → β) (α ↪ β) (↑) Injective where
+  prf _ h := ⟨⟨_, h⟩, rfl⟩
+
 end Function
 
 section Equiv