feat: lemmas about Sigma.curry (#12474)

This provides:

* Basic `simp` lemmas for `Equiv.piCurry`
* Algebraic lemmas for `Sigma.curry` and `Sigma.uncurry`
* A `LinearEquiv` version of `Equiv.piCurry`
* A lemma about `Sigma.curry` and `Pi.mulSingle`

The change from `Sort _` to `Type*` is a no-op, the `_` was inferred as `_ + 1`.

Mathlib/Algebra/Group/Pi/Lemmas.lean

@@ -505,3 +505,49 @@ theorem mulSingle_strictMono : StrictMono (Pi.mulSingle i : f i → ∀ i, f i)
 #align pi.single_strict_mono Pi.single_strictMono
 
 end Pi
+
+namespace Sigma
+
+variable {α : Type*} {β : α → Type*} {γ : ∀ a, β a → Type*}
+
+@[to_additive (attr := simp)]
+theorem curry_one [∀ a b, One (γ a b)] : Sigma.curry (1 : (i : Σ a, β a) → γ i.1 i.2) = 1 :=
+  rfl
+
+@[to_additive (attr := simp)]
+theorem uncurry_one [∀ a b, One (γ a b)] : Sigma.uncurry (1 : ∀ a b, γ a b) = 1 :=
+  rfl
+
+@[to_additive (attr := simp)]
+theorem curry_mul [∀ a b, Mul (γ a b)] (x y : (i : Σ a, β a) → γ i.1 i.2) :
+    Sigma.curry (x * y) = Sigma.curry x * Sigma.curry y :=
+  rfl
+
+@[to_additive (attr := simp)]
+theorem uncurry_mul [∀ a b, Mul (γ a b)] (x y : ∀ a b, γ a b) :
+    Sigma.uncurry (x * y) = Sigma.uncurry x * Sigma.uncurry y :=
+  rfl
+
+@[to_additive (attr := simp)]
+theorem curry_inv [∀ a b, Inv (γ a b)] (x : (i : Σ a, β a) → γ i.1 i.2) :
+    Sigma.curry (x⁻¹) = (Sigma.curry x)⁻¹ :=
+  rfl
+
+@[to_additive (attr := simp)]
+theorem uncurry_inv [∀ a b, Inv (γ a b)] (x : ∀ a b, γ a b) :
+    Sigma.uncurry (x⁻¹) = (Sigma.uncurry x)⁻¹ :=
+  rfl
+
+@[to_additive (attr := simp)]
+theorem curry_mulSingle [DecidableEq α] [∀ a, DecidableEq (β a)] [∀ a b, One (γ a b)]
+    (i : Σ a, β a) (x : γ i.1 i.2) :
+    Sigma.curry (Pi.mulSingle i x) = Pi.mulSingle i.1 (Pi.mulSingle i.2 x) := by
+  simp only [Pi.mulSingle, Sigma.curry_update, Sigma.curry_one, Pi.one_apply]
+
+@[to_additive (attr := simp)]
+theorem uncurry_mulSingle_mulSingle [DecidableEq α] [∀ a, DecidableEq (β a)] [∀ a b, One (γ a b)]
+    (a : α) (b : β a) (x : γ a b) :
+    Sigma.uncurry (Pi.mulSingle a (Pi.mulSingle b x)) = Pi.mulSingle (Sigma.mk a b) x := by
+  rw [← curry_mulSingle ⟨a, b⟩, uncurry_curry]
+
+end Sigma

Mathlib/Data/Sigma/Basic.lean

@@ -183,6 +183,24 @@ theorem Sigma.curry_uncurry {γ : ∀ a, β a → Type*} (f : ∀ (x) (y : β x)
   rfl
 #align sigma.curry_uncurry Sigma.curry_uncurry
 
+theorem Sigma.curry_update {γ : ∀ a, β a → Type*} [DecidableEq α] [∀ a, DecidableEq (β a)]
+    (i : Σ a, β a) (f : (i : Σ a, β a) → γ i.1 i.2) (x : γ i.1 i.2) :
+    Sigma.curry (Function.update f i x) =
+      Function.update (Sigma.curry f) i.1 (Function.update (Sigma.curry f i.1) i.2 x) := by
+  obtain ⟨ia, ib⟩ := i
+  ext ja jb
+  unfold Sigma.curry
+  obtain rfl | ha := eq_or_ne ia ja
+  · obtain rfl | hb := eq_or_ne ib jb
+    · simp
+    · simp only [update_same]
+      rw [Function.update_noteq (mt _ hb.symm), Function.update_noteq hb.symm]
+      rintro h
+      injection h
+  · rw [Function.update_noteq (ne_of_apply_ne Sigma.fst _), Function.update_noteq]
+    · exact ha.symm
+    · exact ha.symm
+
 /-- Convert a product type to a Σ-type. -/
 def Prod.toSigma {α β} (p : α × β) : Σ_ : α, β :=
   ⟨p.1, p.2⟩

Mathlib/LinearAlgebra/Pi.lean

@@ -404,6 +404,26 @@ def piCongrLeft (e : ι' ≃ ι) : ((i' : ι') → φ (e i')) ≃ₗ[R] (i : ι)
   (piCongrLeft' R φ e.symm).symm
 #align linear_equiv.Pi_congr_left LinearEquiv.piCongrLeft
 
+/-- `Equiv.piCurry` as a `LinearEquiv`. -/
+def piCurry {ι : Type*} {κ : ι → Type*} (α : ∀ i, κ i → Type*)
+    [∀ i k, AddCommMonoid (α i k)] [∀ i k, Module R (α i k)] :
+    (Π i : Sigma κ, α i.1 i.2) ≃ₗ[R] Π i j, α i j where
+  __ := Equiv.piCurry α
+  map_add' _ _ := rfl
+  map_smul' _ _ := rfl
+
+@[simp] theorem piCurry_apply {ι : Type*} {κ : ι → Type*} (α : ∀ i, κ i → Type*)
+    [∀ i k, AddCommMonoid (α i k)] [∀ i k, Module R (α i k)]
+    (f : ∀ x : Σ i, κ i, α x.1 x.2) :
+    piCurry R α f = Sigma.curry f :=
+  rfl
+
+@[simp] theorem piCurry_symm_apply {ι : Type*} {κ : ι → Type*} (α : ∀ i, κ i → Type*)
+    [∀ i k, AddCommMonoid (α i k)] [∀ i k, Module R (α i k)]
+    (f : ∀ a b, α a b) :
+    (piCurry R α).symm f = Sigma.uncurry f :=
+  rfl
+
 /-- This is `Equiv.piOptionEquivProd` as a `LinearEquiv` -/
 def piOptionEquivProd {ι : Type*} {M : Option ι → Type*} [(i : Option ι) → AddCommGroup (M i)]
     [(i : Option ι) → Module R (M i)] :

Mathlib/Logic/Equiv/Basic.lean

@@ -745,14 +745,24 @@ theorem piComm_symm {φ : α → β → Sort*} : (piComm φ).symm = (piComm <| s
 to the type of dependent functions of two arguments (i.e., functions to the space of functions).
 
 This is `Sigma.curry` and `Sigma.uncurry` together as an equiv. -/
-def piCurry {β : α → Sort _} (γ : ∀ a, β a → Sort _) :
+def piCurry {β : α → Type*} (γ : ∀ a, β a → Type*) :
     (∀ x : Σ i, β i, γ x.1 x.2) ≃ ∀ a b, γ a b where
   toFun := Sigma.curry
   invFun := Sigma.uncurry
   left_inv := Sigma.uncurry_curry
   right_inv := Sigma.curry_uncurry
 #align equiv.Pi_curry Equiv.piCurry
 
+-- `simps` overapplies these but `simps (config := .asFn)` under-applies them
+@[simp] theorem piCurry_apply {β : α → Type*} (γ : ∀ a, β a → Type*)
+    (f : ∀ x : Σ i, β i, γ x.1 x.2) :
+    piCurry γ f = Sigma.curry f :=
+  rfl
+
+@[simp] theorem piCurry_symm_apply {β : α → Type*} (γ : ∀ a, β a → Type*) (f : ∀ a b, γ a b) :
+    (piCurry γ).symm f = Sigma.uncurry f :=
+  rfl
+
 end
 
 section prodCongr