feat(Logic/Equiv/Basic): sumSigmaDistrib, finSigmaFinEquiv

Mathlib/Algebra/BigOperators/Fin.lean

@@ -388,6 +388,17 @@ theorem finPiFinEquiv_single {m : ℕ} {n : Fin m → ℕ} [∀ i, NeZero (n i)]
   rintro x hx
   rw [Pi.single_eq_of_ne hx, Fin.val_zero', zero_mul]
 
+/-- Equivalence between the Sigma type `(i : Fin m) × Fin (n i)` and `Fin (∑ i : Fin m, n i)`. -/
+def finSigmaFinEquiv {m : ℕ} {n : Fin m → ℕ} : (i : Fin m) × Fin (n i) ≃ Fin (∑ i : Fin m, n i) :=
+  match m with
+  | 0 => @Equiv.equivOfIsEmpty _ _ _ (by simp; exact Fin.isEmpty')
+  | Nat.succ m =>
+    calc _ ≃ _ := (@finSumFinEquiv m 1).sigmaCongrLeft.symm
+      _ ≃ _ := Equiv.sumSigmaDistrib _
+      _ ≃ _ := finSigmaFinEquiv.sumCongr (Equiv.uniqueSigma _)
+      _ ≃ _ := finSumFinEquiv
+      _ ≃ _ := finCongr (Fin.sum_univ_castSucc n).symm
+
 namespace List
 
 section CommMonoid

Mathlib/Logic/Equiv/Basic.lean

@@ -215,6 +215,23 @@ theorem sigmaUnique_symm_apply {α} {β : α → Type*} [∀ a, Unique (β a)] (
     (sigmaUnique α β).symm x = ⟨x, default⟩ :=
   rfl
 
+/-- Any `Unique` type is a left identity for type sigma up to equivalence. Compare with `uniqueProd`
+which is non-dependent. -/
+def uniqueSigma {α} (β : α → Type*) [Unique α] : (i:α) × β i ≃ β default :=
+  ⟨fun p ↦ (Unique.eq_default _).rec p.2,
+   fun b ↦ ⟨default, b⟩,
+   fun _ ↦ Sigma.ext (Unique.default_eq _) (eqRec_heq _ _),
+   fun _ ↦ rfl⟩
+
+theorem uniqueSigma_apply {α} {β : α → Type*} [Unique α] (x : (a : α) × β a) :
+    uniqueSigma β x = (Unique.eq_default _).rec x.2 :=
+  rfl
+
+@[simp]
+theorem uniqueSigma_symm_apply {α} {β : α → Type*} [Unique α] (y : β default) :
+    (uniqueSigma β).symm y = ⟨default, y⟩ :=
+  rfl
+
 /-- `Empty` type is a right absorbing element for type product up to an equivalence. -/
 def prodEmpty (α) : α × Empty ≃ Empty :=
   equivEmpty _
@@ -919,14 +936,27 @@ theorem prodSumDistrib_symm_apply_right {α β γ} (a : α × γ) :
     (prodSumDistrib α β γ).symm (inr a) = (a.1, inr a.2) :=
   rfl
 
-/-- An indexed sum of disjoint sums of types is equivalent to the sum of the indexed sums. -/
+/-- An indexed sum of disjoint sums of types is equivalent to the sum of the indexed sums. Compare
+with `Equiv.sumSigmaDistrib` which is indexed by sums. -/
 @[simps]
 def sigmaSumDistrib {ι} (α β : ι → Type*) :
     (Σ i, α i ⊕ β i) ≃ (Σ i, α i) ⊕ (Σ i, β i) :=
   ⟨fun p => p.2.map (Sigma.mk p.1) (Sigma.mk p.1),
     Sum.elim (Sigma.map id fun _ => Sum.inl) (Sigma.map id fun _ => Sum.inr), fun p => by
     rcases p with ⟨i, a | b⟩ <;> rfl, fun p => by rcases p with (⟨i, a⟩ | ⟨i, b⟩) <;> rfl⟩
 
+/-- A type indexed by  disjoint sums of types is equivalent to the sum of the sums. Compare with
+`Equiv.sigmaSumDistrib` which has the sums as the output type. -/
+@[simps]
+def sumSigmaDistrib {α β} (t : α ⊕ β → Type*) :
+    (Σ i, t i) ≃ (Σ i, t (.inl i)) ⊕ (Σ i, t (.inr i)) :=
+  ⟨(match · with
+   | .mk (.inl x) y => .inl ⟨x, y⟩
+   | .mk (.inr x) y => .inr ⟨x, y⟩),
+  Sum.elim (fun a ↦ ⟨.inl a.1, a.2⟩) (fun b ↦ ⟨.inr b.1, b.2⟩),
+  by rintro ⟨x|x,y⟩ <;> simp,
+  by rintro (⟨x,y⟩|⟨x,y⟩) <;> simp⟩
+
 /-- The product of an indexed sum of types (formally, a `Sigma`-type `Σ i, α i`) by a type `β` is
 equivalent to the sum of products `Σ i, (α i × β)`. -/
 @[simps apply symm_apply]