diff --git a/SciLean/Algebra/IsAddGroupHom.lean b/SciLean/Algebra/IsAddGroupHom.lean
index 36ce1213..d7327a81 100644
--- a/SciLean/Algebra/IsAddGroupHom.lean
+++ b/SciLean/Algebra/IsAddGroupHom.lean
@@ -128,11 +128,11 @@ theorem HSub.hSub.arg_a0a1.IsAddGroupHom_rule
   · simp [hf.map_neg,hg.map_neg,add_comm,←neg_add_eq_sub]
 
 
--- IndexType.sum ----------------------------------------------------------------
+-- sum ----------------------------------------------------------------
 --------------------------------------------------------------------------------
 
 @[fun_prop]
-theorem IndexType.sum.arg_f.IsAddGroupHom_rule
+theorem sum.arg_f.IsAddGroupHom_rule
   [IndexType ι]
   (f : X → ι → Y) (hf : ∀ i, IsAddGroupHom (f · i))
   : IsAddGroupHom fun x => ∑ i, f x i := by have := hf; sorry_proof
diff --git a/SciLean/Algebra/IsAffineMap.lean b/SciLean/Algebra/IsAffineMap.lean
index cd5c925c..4344d719 100644
--- a/SciLean/Algebra/IsAffineMap.lean
+++ b/SciLean/Algebra/IsAffineMap.lean
@@ -172,11 +172,11 @@ theorem HMul.hMul.arg_a1.IsAffineMap_rule
   (f : X → R) (hf : IsAffineMap R f) (y' : R) : IsAffineMap 𝕜 fun x => y' * f x := sorry_proof
 
 
--- IndexType.sum ----------------------------------------------------------------
+-- sum ----------------------------------------------------------------
 --------------------------------------------------------------------------------
 
 @[fun_prop]
-theorem IndexType.sum.arg_f.IsAffineMap_rule
+theorem sum.arg_f.IsAffineMap_rule
   (f : X → ι → Y) (hf : ∀ i, IsAffineMap R (f · i))
   : IsAffineMap R fun x => ∑ i, f x i := by sorry_proof
 
diff --git a/SciLean/Algebra/IsLinearMap.lean b/SciLean/Algebra/IsLinearMap.lean
index f28b1c01..f2ebba83 100644
--- a/SciLean/Algebra/IsLinearMap.lean
+++ b/SciLean/Algebra/IsLinearMap.lean
@@ -266,11 +266,11 @@ theorem HSMul.hSMul.arg_a1.IsLinearMap_rule_int
   intro x y; simp[hf.1]
   intro c x; simp[hf.2]; rw [@smul_comm]
 
--- IndexType.sum ----------------------------------------------------------------
+-- sum ----------------------------------------------------------------
 --------------------------------------------------------------------------------
 
 @[fun_prop]
-theorem IndexType.sum.arg_f.IsLinearMap_rule
+theorem sum.arg_f.IsLinearMap_rule
   (f : X → ι → Y) (hf : ∀ i, IsLinearMap R (f · i))
   : IsLinearMap R fun x => ∑ i, f x i := by sorry_proof
 
diff --git a/SciLean/Analysis/AdjointSpace/Adjoint.lean b/SciLean/Analysis/AdjointSpace/Adjoint.lean
index 1f533cd4..d103cdff 100644
--- a/SciLean/Analysis/AdjointSpace/Adjoint.lean
+++ b/SciLean/Analysis/AdjointSpace/Adjoint.lean
@@ -210,7 +210,7 @@ theorem pi_rule
     (f : X → (i : ι) → E i) (hf : ∀ i, IsContinuousLinearMap K (f · i)) :
     (fun (x : X) (i : ι) => f x i)†
     =
-    (fun x' => IndexType.sum fun i => ((f · i)†) (x' i)) := by
+    (fun x' => sum fun i => ((f · i)†) (x' i)) := by
 
   rw[← (eq_adjoint_iff _ _ (by fun_prop)).2]
   intro x y
@@ -406,11 +406,11 @@ by
 
 
 @[fun_trans]
-theorem IndexType.sum.arg_f.adjoint_rule {ι} [IndexType ι]
+theorem sum.arg_f.adjoint_rule {ι} [IndexType ι]
   (f : X → ι → Y) (hf : ∀ i, IsContinuousLinearMap K (f · i))
-  : (fun x => IndexType.sum fun i => f x i)†
+  : (fun x => sum fun i => f x i)†
     =
-    (fun y => IndexType.sum fun i => ((f · i)†) y) :=
+    (fun y => sum fun i => ((f · i)†) y) :=
 by
   rw[← (eq_adjoint_iff _ _ (by fun_prop)).2]
   sorry_proof
diff --git a/SciLean/Analysis/AdjointSpace/AdjointProj.lean b/SciLean/Analysis/AdjointSpace/AdjointProj.lean
index 260be5e5..6363ab51 100644
--- a/SciLean/Analysis/AdjointSpace/AdjointProj.lean
+++ b/SciLean/Analysis/AdjointSpace/AdjointProj.lean
@@ -643,7 +643,7 @@ def HPow.hPow.arg_a0.adjointProjUpdate_rule
   unfold adjointProjUpdate; fun_trans
 
 
--- IndexType.sum ----------------------------------------------------------------
+-- sum ----------------------------------------------------------------
 --------------------------------------------------------------------------------
 
 section IndexTypeSum
@@ -652,7 +652,7 @@ variable {ι : Type} [IndexType ι]
 
 
 @[fun_trans]
-theorem IndexType.sum.arg_f.adjointProj_rule [DecidableEq ι]
+theorem sum.arg_f.adjointProj_rule [DecidableEq ι]
     (f : X → ι → Y') (hf : ∀ i, IsContinuousLinearMap K (fun x => f x i)) :
     adjointProj K Yi (fun x => ∑ i, f x i)
     =
@@ -670,7 +670,7 @@ theorem IndexType.sum.arg_f.adjointProj_rule [DecidableEq ι]
 
 
 @[fun_trans]
-theorem IndexType.sum.arg_f.adjointProjUpdate_rule [DecidableEq ι]
+theorem sum.arg_f.adjointProjUpdate_rule [DecidableEq ι]
     (f : X → ι → Y') (hf : ∀ i, IsContinuousLinearMap K (fun x => f x i)) :
     adjointProjUpdate K Yi (fun x => ∑ i, f x i)
     =
diff --git a/SciLean/Analysis/AdjointSpace/Basic.lean b/SciLean/Analysis/AdjointSpace/Basic.lean
index 4f1804b4..fe6d87dc 100644
--- a/SciLean/Analysis/AdjointSpace/Basic.lean
+++ b/SciLean/Analysis/AdjointSpace/Basic.lean
@@ -305,8 +305,8 @@ instance : AdjointSpace 𝕜 ((i : ι) → E i) where
     -- apply Exists.intro (∑ i, d i ^ 2)
     sorry_proof
   conj_symm := by simp; sorry_proof
-  add_left := by simp[inner_add_left,SciLean.IndexType.sum_add_distrib]
-  smul_left := by simp[inner_smul_left,SciLean.IndexType.mul_sum]
+  add_left := by simp[inner_add_left,SciLean.sum_add_distrib]
+  smul_left := by simp[inner_smul_left,SciLean.mul_sum]
 
 
 theorem inner_prod_split (x y : X×Y) : ⟪x,y⟫_𝕜 = ⟪x.1,y.1⟫_𝕜 + ⟪x.2,y.2⟫_𝕜 := by rfl
diff --git a/SciLean/Analysis/Calculus/CDeriv.lean b/SciLean/Analysis/Calculus/CDeriv.lean
index b09c03bf..d1c69b0d 100644
--- a/SciLean/Analysis/Calculus/CDeriv.lean
+++ b/SciLean/Analysis/Calculus/CDeriv.lean
@@ -450,11 +450,11 @@ def HPow.hPow.arg_a0.cderiv_rule (n : Nat)
   funext x; fun_trans
 
 
--- IndexType.sum ----------------------------------------------------------------
+-- sum ----------------------------------------------------------------
 --------------------------------------------------------------------------------
 
 @[fun_trans]
-theorem IndexType.sum.arg_f.cderiv_rule_at
+theorem sum.arg_f.cderiv_rule_at
   (f : X → ι → Y) (x : X) (hf : ∀ i, CDifferentiableAt K (f · i) x)
   : cderiv K (fun x => ∑ i, f x i) x
     =
@@ -465,7 +465,7 @@ by
 
 
 @[fun_trans]
-theorem IndexType.sum.arg_f.cderiv_rule
+theorem sum.arg_f.cderiv_rule
   (f : X → ι → Y) (hf : ∀ i, CDifferentiable K (f · i))
   : cderiv K (fun x => ∑ i, f x i)
     =
diff --git a/SciLean/Analysis/Calculus/FDeriv.lean b/SciLean/Analysis/Calculus/FDeriv.lean
index 953bc3bf..8a9a1c18 100644
--- a/SciLean/Analysis/Calculus/FDeriv.lean
+++ b/SciLean/Analysis/Calculus/FDeriv.lean
@@ -390,12 +390,12 @@ by
 --------------------------------------------------------------------------------
 
 @[fun_trans]
-theorem IndexType.sum.arg_f.fderiv_rule_at {ι} [IndexType ι]
+theorem sum.arg_f.fderiv_rule_at {ι} [IndexType ι]
   (x : X) (f : X → ι → Y) (hf : ∀ i, DifferentiableAt K (f · i) x)
-  : fderiv K (fun x => IndexType.sum fun i => f x i) x
+  : fderiv K (fun x => sum fun i => f x i) x
     =
     fun dx =>L[K]
-      IndexType.sum fun i =>
+      sum fun i =>
         let dy := fderiv K (f · i) x dx
         dy :=
 by
@@ -405,12 +405,12 @@ by
   apply hf
 
 @[fun_trans]
-theorem IndexType.sum.arg_f.fderiv_rule {ι} [IndexType ι]
+theorem sum.arg_f.fderiv_rule {ι} [IndexType ι]
   (f : X → ι → Y) (hf : ∀ i, Differentiable K (f · i))
-  : fderiv K (fun x => IndexType.sum fun i => f x i)
+  : fderiv K (fun x => sum fun i => f x i)
     =
     fun x => fun dx =>L[K]
-      IndexType.sum fun i =>
+      sum fun i =>
         let dy := fderiv K (f · i) x dx
         dy :=
 by
diff --git a/SciLean/Analysis/Calculus/FwdCDeriv.lean b/SciLean/Analysis/Calculus/FwdCDeriv.lean
index cd6e3814..c0efadf0 100644
--- a/SciLean/Analysis/Calculus/FwdCDeriv.lean
+++ b/SciLean/Analysis/Calculus/FwdCDeriv.lean
@@ -364,11 +364,11 @@ def HPow.hPow.arg_a0.fwdCDeriv_rule (n : Nat)
   unfold fwdCDeriv; fun_trans
 
 
--- IndexType.sum ----------------------------------------------------------------
+-- sum ----------------------------------------------------------------
 --------------------------------------------------------------------------------
 
 @[fun_trans]
-theorem IndexType.sum.arg_f.fwdCDeriv_rule_at (x : X)
+theorem sum.arg_f.fwdCDeriv_rule_at (x : X)
     (f : X → ι → Y) (hf : ∀ i, CDifferentiableAt K (f · i) x) :
     fwdCDeriv K (fun x => ∑ i, f x i) x
     =
@@ -378,7 +378,7 @@ theorem IndexType.sum.arg_f.fwdCDeriv_rule_at (x : X)
   unfold fwdCDeriv; fun_trans; sorry_proof -- need linearity of prod.mk
 
 @[fun_trans]
-theorem IndexType.sum.arg_f.fwdCDeriv_rule
+theorem sum.arg_f.fwdCDeriv_rule
     (f : X → ι → Y) (hf : ∀ i, CDifferentiable K (f · i)) :
     fwdCDeriv K (fun x => ∑ i, f x i)
     =
diff --git a/SciLean/Analysis/Calculus/FwdFDeriv.lean b/SciLean/Analysis/Calculus/FwdFDeriv.lean
index deaa888b..75d6e58f 100644
--- a/SciLean/Analysis/Calculus/FwdFDeriv.lean
+++ b/SciLean/Analysis/Calculus/FwdFDeriv.lean
@@ -385,7 +385,7 @@ def HPow.hPow.arg_a0.fwdFDeriv_rule (n : Nat) :
   unfold fwdFDeriv; fun_trans
 
 
--- IndexType.sum ----------------------------------------------------------------
+-- sum ----------------------------------------------------------------
 --------------------------------------------------------------------------------
 
 open BigOperators in
@@ -403,12 +403,12 @@ theorem FinType.sum.arg_f.fwdFDeriv_rule_at (x : X) (A : Finset ι)
 
 
 @[fun_trans]
-theorem IndexType.sum.arg_f.fwdFDeriv_rule_at {ι} [IndexType ι]
+theorem sum.arg_f.fwdFDeriv_rule_at {ι} [IndexType ι]
   (x : X) (f : X → ι → Y) (hf : ∀ i, DifferentiableAt K (f · i) x)
-  : fwdFDeriv K (fun x => IndexType.sum fun i => f x i) x
+  : fwdFDeriv K (fun x => sum fun i => f x i) x
     =
     fun dx =>
-      IndexType.sum fun i =>
+      sum fun i =>
         let ydy := fwdFDeriv K (f · i) x dx
         ydy :=
 by
@@ -417,12 +417,12 @@ by
 
 
 @[fun_trans]
-theorem IndexType.sum.arg_f.fwdFDeriv_rule {ι} [IndexType ι]
+theorem sum.arg_f.fwdFDeriv_rule {ι} [IndexType ι]
   (f : X → ι → Y) (hf : ∀ i, Differentiable K (f · i))
-  : fwdFDeriv K (fun x => IndexType.sum fun i => f x i)
+  : fwdFDeriv K (fun x => sum fun i => f x i)
     =
     fun x dx =>
-      IndexType.sum fun i =>
+      sum fun i =>
         let ydy := fwdFDeriv K (f · i) x dx
         ydy :=
 by
diff --git a/SciLean/Analysis/Calculus/RevCDeriv.lean b/SciLean/Analysis/Calculus/RevCDeriv.lean
index 25666e10..d78a4b76 100644
--- a/SciLean/Analysis/Calculus/RevCDeriv.lean
+++ b/SciLean/Analysis/Calculus/RevCDeriv.lean
@@ -222,7 +222,7 @@ theorem pi_rule
   fun_trans;
   funext x; simp
   rw[cderiv.pi_rule (hf:=by fun_prop)]; fun_trans
-  simp[revCDerivUpdate,revCDeriv,IndexType.sum]
+  simp[revCDerivUpdate,revCDeriv,sum]
   sorry_proof
 
 end revCDeriv
@@ -1176,7 +1176,7 @@ def HPow.hPow.arg_a0.revCDerivProjUpdate_rule
   unfold revCDerivProjUpdate; fun_trans; simp[oneHot,structMake,revCDerivUpdate]
 
 
--- IndexType.sum ----------------------------------------------------------------
+-- sum ----------------------------------------------------------------
 --------------------------------------------------------------------------------
 
 section IndexTypeSum
@@ -1184,7 +1184,7 @@ section IndexTypeSum
 variable {ι : Type} [IndexType ι]
 
 @[fun_trans]
-theorem IndexType.sum.arg_f.revCDeriv_rule
+theorem sum.arg_f.revCDeriv_rule
   (f : X → ι → Y) (hf : ∀ i, HasAdjDiff K (fun x => f x i))
   : revCDeriv K (fun x => ∑ i, f x i)
     =
@@ -1202,7 +1202,7 @@ by
 
 
 @[fun_trans]
-theorem IndexType.sum.arg_f.revCDerivUpdate_rule
+theorem sum.arg_f.revCDerivUpdate_rule
     (f : X → ι → Y) (hf : ∀ i, HasAdjDiff K (fun x => f x i)) :
     revCDerivUpdate K (fun x => ∑ i, f x i)
     =
@@ -1215,7 +1215,7 @@ theorem IndexType.sum.arg_f.revCDerivUpdate_rule
   fun_trans
 
 @[fun_trans]
-theorem IndexType.sum.arg_f.revCDerivProj_rule [DecidableEq ι]
+theorem sum.arg_f.revCDerivProj_rule [DecidableEq ι]
     (f : X → ι → Y') (hf : ∀ i, HasAdjDiff K (fun x => f x i)) :
     revCDerivProj K Yi (fun x => ∑ i, f x i)
     =
@@ -1233,7 +1233,7 @@ theorem IndexType.sum.arg_f.revCDerivProj_rule [DecidableEq ι]
 
 
 @[fun_trans]
-theorem IndexType.sum.arg_f.revCDerivProjUpdate_rule [DecidableEq ι]
+theorem sum.arg_f.revCDerivProjUpdate_rule [DecidableEq ι]
     (f : X → ι → Y') (hf : ∀ i, HasAdjDiff K (fun x => f x i)) :
     revCDerivProjUpdate K Yi (fun x => ∑ i, f x i)
     =
diff --git a/SciLean/Analysis/Calculus/RevFDeriv.lean b/SciLean/Analysis/Calculus/RevFDeriv.lean
index d2f1f59c..4e84ca56 100644
--- a/SciLean/Analysis/Calculus/RevFDeriv.lean
+++ b/SciLean/Analysis/Calculus/RevFDeriv.lean
@@ -118,7 +118,7 @@ theorem pi_rule
     =
     fun x =>
       (fun i => f x i,
-       fun dy => IndexType.sum fun i =>
+       fun dy => sum fun i =>
          let dx := (revFDeriv K (f · i) x).2 (dy i)
          dx)
        := by
@@ -169,7 +169,7 @@ theorem pi_rule_at
     (revFDeriv K fun (x : X) (i : ι) => f x i) x
     =
     (fun i => f x i,
-     fun dy => IndexType.sum fun i =>
+     fun dy => sum fun i =>
        let dx := (revFDeriv K (f · i) x).2 (dy i)
        dx) := by
   unfold revFDeriv
@@ -504,13 +504,13 @@ def HPow.hPow.arg_a0.revFDeriv_rule
 --------------------------------------------------------------------------------
 
 @[fun_trans]
-theorem IndexType.sum.arg_f.revFDeriv_rule_at {ι} [IndexType ι]
+theorem sum.arg_f.revFDeriv_rule_at {ι} [IndexType ι]
   (x : X) (f : X → ι → Y) (hf : ∀ i, DifferentiableAt K (f · i) x)
-  : revFDeriv K (fun x => IndexType.sum fun i => f x i) x
+  : revFDeriv K (fun x => sum fun i => f x i) x
     =
-    (IndexType.sum fun i => f x i,
+    (sum fun i => f x i,
      fun dy =>
-       IndexType.sum fun i =>
+       sum fun i =>
          let dx := adjointFDeriv K (f · i) x dy
          dx) :=
 
@@ -520,13 +520,13 @@ by
 
 
 @[fun_trans]
-theorem IndexType.sum.arg_f.revFDeriv_rule {ι} [IndexType ι]
+theorem sum.arg_f.revFDeriv_rule {ι} [IndexType ι]
   (f : X → ι → Y) (hf : ∀ i, Differentiable K (f · i))
-  : revFDeriv K (fun x => IndexType.sum fun i => f x i)
+  : revFDeriv K (fun x => sum fun i => f x i)
     =
     fun x =>
-    (IndexType.sum fun i => f x i,
+    (sum fun i => f x i,
      fun dy =>
-       IndexType.sum fun i =>
+       sum fun i =>
          let dx := adjointFDeriv K (f · i) x dy
          dx) := by funext x; fun_trans
diff --git a/SciLean/Analysis/Calculus/RevFDerivProj.lean b/SciLean/Analysis/Calculus/RevFDerivProj.lean
index 0d701158..c18a4a47 100644
--- a/SciLean/Analysis/Calculus/RevFDerivProj.lean
+++ b/SciLean/Analysis/Calculus/RevFDerivProj.lean
@@ -837,14 +837,14 @@ def HPow.hPow.arg_a0.revFDerivProjUpdate_rule
   unfold revFDerivProjUpdate; fun_trans
 
 
--- IndexType.sum ----------------------------------------------------------------
+-- sum ----------------------------------------------------------------
 --------------------------------------------------------------------------------
 
 section IndexTypeSum
 
 
 @[fun_trans]
-theorem IndexType.sum.arg_f.revFDerivProj_rule
+theorem sum.arg_f.revFDerivProj_rule
     (f : X → ι → Y') (hf : ∀ i, Differentiable K (fun x => f x i)) :
     revFDerivProj K Yi (fun x => ∑ i, f x i)
     =
@@ -859,7 +859,7 @@ theorem IndexType.sum.arg_f.revFDerivProj_rule
 
 
 @[fun_trans]
-theorem IndexType.sum.arg_f.revFDerivProjUpdate_rule
+theorem sum.arg_f.revFDerivProjUpdate_rule
     (f : X → ι → Y') (hf : ∀ i, Differentiable K (fun x => f x i)) :
     revFDerivProjUpdate K Yi (fun x => ∑ i, f x i)
     =
diff --git a/SciLean/Analysis/Convenient/CDifferentiable.lean b/SciLean/Analysis/Convenient/CDifferentiable.lean
index cdc8a349..9fe837db 100644
--- a/SciLean/Analysis/Convenient/CDifferentiable.lean
+++ b/SciLean/Analysis/Convenient/CDifferentiable.lean
@@ -348,12 +348,12 @@ def HPow.hPow.arg_a0.CDifferentiableAt_rule
 
 
 
--- IndexType.sum ----------------------------------------------------------------
+-- sum ----------------------------------------------------------------
 ---------------------------------------------------------------------------------
 
 
 @[fun_prop]
-theorem IndexType.sum.arg_f.CDifferentiableAt_rule
+theorem sum.arg_f.CDifferentiableAt_rule
   (f : X → ι → Y) (x : X) (hf : ∀ i, CDifferentiableAt K (fun x => f x i) x)
   : CDifferentiableAt K (fun x => ∑ i, f x i) x :=
 by
@@ -361,7 +361,7 @@ by
 
 
 @[fun_prop]
-theorem IndexType.sum.arg_f.CDifferentiable_rule
+theorem sum.arg_f.CDifferentiable_rule
   (f : X → ι → Y) (hf : ∀ i, CDifferentiable K (fun x => f x i))
   : CDifferentiable K (fun x => ∑ i, f x i) :=
 by
diff --git a/SciLean/Analysis/Convenient/ContCDiff.lean b/SciLean/Analysis/Convenient/ContCDiff.lean
index a0774629..23ffd21a 100644
--- a/SciLean/Analysis/Convenient/ContCDiff.lean
+++ b/SciLean/Analysis/Convenient/ContCDiff.lean
@@ -331,17 +331,17 @@ def HPow.hPow.arg_a0.ContCDiff_rule
     ContCDiff K n (fun x => f x ^ m) := by intro x; fun_prop
 
 
--- IndexType.sum ----------------------------------------------------------------
+-- sum ----------------------------------------------------------------
 --------------------------------------------------------------------------------
 
 @[fun_prop]
-theorem IndexType.sum.arg_f.ContCDiffAt_rule
+theorem sum.arg_f.ContCDiffAt_rule
   (f : X → ι → Y) (x : X) (hf : ∀ i, ContCDiffAt K n (fun x => f x i) x)
   : ContCDiffAt K n (fun x => ∑ i, f x i) x := by sorry_proof
 
 
 @[fun_prop]
-theorem IndexType.sum.arg_f.ContCDiff_rule
+theorem sum.arg_f.ContCDiff_rule
   (f : X → ι → Y) (hf : ∀ i, ContCDiff K n (fun x => f x i))
   : ContCDiff K n (fun x => ∑ i, f x i) := by intro x; fun_prop
 
diff --git a/SciLean/Analysis/Convenient/HasAdjDiff.lean b/SciLean/Analysis/Convenient/HasAdjDiff.lean
index 543b3f51..3f25317d 100644
--- a/SciLean/Analysis/Convenient/HasAdjDiff.lean
+++ b/SciLean/Analysis/Convenient/HasAdjDiff.lean
@@ -352,17 +352,17 @@ def HPow.hPow.arg_a0.HasAdjDiff_rule
   intro x; fun_prop
 
 
--- IndexType.sum ---------------------------------------------------------------
+-- sum ---------------------------------------------------------------
 --------------------------------------------------------------------------------
 
 @[fun_prop]
-theorem IndexType.sum.arg_f.HasAdjDiffAt_rule (x : X)
+theorem sum.arg_f.HasAdjDiffAt_rule (x : X)
     (f : X → ι → Y) (hf : ∀ i, HasAdjDiffAt K (f · i) x) :
     HasAdjDiffAt K (fun x => ∑ i, f x i) x := by
   constructor; fun_prop; fun_trans; fun_prop
 
 @[fun_prop]
-theorem IndexType.sum.arg_f.HasAdjDiff_rule
+theorem sum.arg_f.HasAdjDiff_rule
     (f : X → ι → Y) (hf : ∀ i, HasAdjDiff K (f · i)) :
     HasAdjDiff K (fun x => ∑ i, f x i) := by
   intro x; fun_prop
diff --git a/SciLean/Analysis/Convenient/HasSemiAdjoint.lean b/SciLean/Analysis/Convenient/HasSemiAdjoint.lean
index f7884cb6..5315d9a9 100644
--- a/SciLean/Analysis/Convenient/HasSemiAdjoint.lean
+++ b/SciLean/Analysis/Convenient/HasSemiAdjoint.lean
@@ -334,7 +334,7 @@ by
 --------------------------------------------------------------------------------
 
 @[fun_prop]
-theorem SciLean.IndexType.sum.arg_f.HasSemiAdjoint_rule
+theorem SciLean.sum.arg_f.HasSemiAdjoint_rule
   (f : X → ι → Y) (hf : ∀ i, HasSemiAdjoint K fun x : X => f x i)
   : HasSemiAdjoint K fun x => ∑ i, f x i :=
 by
diff --git a/SciLean/Analysis/Convenient/IsSmoothLinearMap.lean b/SciLean/Analysis/Convenient/IsSmoothLinearMap.lean
index 93964fcc..b198e0ad 100644
--- a/SciLean/Analysis/Convenient/IsSmoothLinearMap.lean
+++ b/SciLean/Analysis/Convenient/IsSmoothLinearMap.lean
@@ -179,11 +179,11 @@ theorem HSMul.hSMul.arg_a1.IsSmoothLinearMap_rule_int
   constructor <;> fun_prop
 
 
--- IndexType.sum ----------------------------------------------------------------
+-- sum ----------------------------------------------------------------
 --------------------------------------------------------------------------------
 
 @[fun_prop]
-theorem IndexType.sum.arg_f.IsSmoothLinearMap_rule
+theorem sum.arg_f.IsSmoothLinearMap_rule
     (f : X → ι → Y) (hf : ∀ i, IsSmoothLinearMap K (f · i)) :
     IsSmoothLinearMap K fun x => ∑ i, f x i := by constructor <;> fun_prop
 
diff --git a/SciLean/Analysis/Convenient/SemiAdjoint.lean b/SciLean/Analysis/Convenient/SemiAdjoint.lean
index 26da0132..bb75f215 100644
--- a/SciLean/Analysis/Convenient/SemiAdjoint.lean
+++ b/SciLean/Analysis/Convenient/SemiAdjoint.lean
@@ -241,11 +241,11 @@ by
   sorry_proof
 
 
--- IndexType.sum ------------------------------------------------------------------
+-- sum ------------------------------------------------------------------
 --------------------------------------------------------------------------------
 
 @[fun_trans]
-theorem IndexType.sum.arg_f.semiAdjoint_rule
+theorem sum.arg_f.semiAdjoint_rule
   (f : X → ι → Y) (hf : ∀ i, HasSemiAdjoint K (f · i))
   : semiAdjoint K (fun x => ∑ i, f x i)
     =
diff --git a/SciLean/Analysis/Normed/IsContinuousLinearMap.lean b/SciLean/Analysis/Normed/IsContinuousLinearMap.lean
index ae207867..8f12891c 100644
--- a/SciLean/Analysis/Normed/IsContinuousLinearMap.lean
+++ b/SciLean/Analysis/Normed/IsContinuousLinearMap.lean
@@ -407,9 +407,9 @@ theorem Finset.sum.arg_f.IsContinuousLinearMap_rule
 }
 
 @[fun_prop]
-theorem SciLean.IndexType.sum.arg_f.IsContinuousLinearMap_rule {ι} [IndexType ι]
+theorem SciLean.sum.arg_f.IsContinuousLinearMap_rule {ι} [IndexType ι]
   (f : X → ι → Y) (_ : ∀ i, IsContinuousLinearMap R fun x : X => f x i)
-  : IsContinuousLinearMap R fun x => IndexType.sum (f x) :=
+  : IsContinuousLinearMap R fun x => sum (f x) :=
 {
   linear := sorry_proof
   cont := sorry_proof
diff --git a/SciLean/Data/DataArray/Operations/Cross.lean b/SciLean/Data/DataArray/Operations/Cross.lean
index 61c121b5..72d3d8d1 100644
--- a/SciLean/Data/DataArray/Operations/Cross.lean
+++ b/SciLean/Data/DataArray/Operations/Cross.lean
@@ -37,7 +37,7 @@ abbrev_fun_trans cross in y : adjoint R by
     intro y
     rw[← adjoint_ex _ (by fun_prop)]
     simp[DataArrayN.inner_def, DataArrayN.cross,
-         sum_over_prod, sum_pull]
+         sum_prod_eq_sum_sum, sum_pull]
     -- expand the sum explicitely and call ring
     sorry_proof
 
diff --git a/SciLean/Data/DataArray/Operations/Curry.lean b/SciLean/Data/DataArray/Operations/Curry.lean
index da20512d..ffe6c1be 100644
--- a/SciLean/Data/DataArray/Operations/Curry.lean
+++ b/SciLean/Data/DataArray/Operations/Curry.lean
@@ -38,7 +38,7 @@ abbrev_fun_trans curry in x
     apply AdjointSpace.ext_inner_left R
     intro z
     rw[← adjoint_ex _ (by fun_prop)]
-    simp only [inner, curry_def, ArrayType.get_ofFn', uncurry_def, sum_over_prod, uncurry_appply2]
+    simp only [inner, curry_def, ArrayType.get_ofFn', uncurry_def, sum_prod_eq_sum_sum, uncurry_appply2]
 
 abbrev_fun_trans curry in x
     {R} [RCLike R] [NormedAddCommGroup α] [AdjointSpace R α] [CompleteSpace α] :
diff --git a/SciLean/Data/DataArray/Operations/Diag.lean b/SciLean/Data/DataArray/Operations/Diag.lean
index b988780a..c4bfe1d2 100644
--- a/SciLean/Data/DataArray/Operations/Diag.lean
+++ b/SciLean/Data/DataArray/Operations/Diag.lean
@@ -27,7 +27,7 @@ abbrev_fun_trans diag in x : adjoint R by
     rw[← adjoint_ex _ (by fun_prop)]
     simp[DataArrayN.inner_def,Function.HasUncurry.uncurry,
          DataArrayN.diag,DataArrayN.diagonal,
-         sum_over_prod, sum_ite']
+         sum_prod_eq_sum_sum, sum_ite']
 
 abbrev_fun_trans diag in x : revFDeriv R by
   unfold revFDeriv
diff --git a/SciLean/Data/DataArray/Operations/Diagonal.lean b/SciLean/Data/DataArray/Operations/Diagonal.lean
index f8a5c033..27db8f6a 100644
--- a/SciLean/Data/DataArray/Operations/Diagonal.lean
+++ b/SciLean/Data/DataArray/Operations/Diagonal.lean
@@ -31,7 +31,7 @@ abbrev_fun_trans diagonal in x [DecidableEq I] [RealScalar R] : adjoint R by
     rw[← adjoint_ex _ (by fun_prop)]
     simp[DataArrayN.inner_def,Function.HasUncurry.uncurry,
          DataArrayN.diagonal,DataArrayN.diag,
-         sum_over_prod, sum_ite']
+         sum_prod_eq_sum_sum, sum_ite']
 
 abbrev_fun_trans diagonal in x [DecidableEq I] [RealScalar R] : revFDeriv R by
   unfold revFDeriv
diff --git a/SciLean/Data/DataArray/Operations/Dot.lean b/SciLean/Data/DataArray/Operations/Dot.lean
index 86184bb7..c343bc61 100644
--- a/SciLean/Data/DataArray/Operations/Dot.lean
+++ b/SciLean/Data/DataArray/Operations/Dot.lean
@@ -27,7 +27,7 @@ abbrev_fun_trans dot in x : adjoint R by
     intro z
     rw[← adjoint_ex _ (by fun_prop)]
     simp[DataArrayN.inner_def, DataArrayN.dot,
-         sum_over_prod, Function.HasUncurry.uncurry, sum_pull]
+         sum_prod_eq_sum_sum, Function.HasUncurry.uncurry, sum_pull]
     ac_rfl
 
 abbrev_fun_trans dot in y : adjoint R by
@@ -37,7 +37,7 @@ abbrev_fun_trans dot in y : adjoint R by
     intro z
     rw[← adjoint_ex _ (by fun_prop)]
     simp[DataArrayN.inner_def, DataArrayN.dot,
-         sum_over_prod, Function.HasUncurry.uncurry, sum_pull]
+         Function.HasUncurry.uncurry, sum_pull]
     ac_rfl
 
 abbrev_fun_trans dot in x y : revFDeriv R by
diff --git a/SciLean/Data/DataArray/Operations/Matmul.lean b/SciLean/Data/DataArray/Operations/Matmul.lean
index a91c23c6..e7d1b9d6 100644
--- a/SciLean/Data/DataArray/Operations/Matmul.lean
+++ b/SciLean/Data/DataArray/Operations/Matmul.lean
@@ -27,7 +27,7 @@ abbrev_fun_trans matmul in A : adjoint R by
     intro D
     rw[← adjoint_ex _ (by fun_prop)]
     simp[DataArrayN.inner_def, DataArrayN.matmul, DataArrayN.transpose,
-         sum_over_prod, Function.HasUncurry.uncurry, sum_pull]
+         sum_prod_eq_sum_sum, Function.HasUncurry.uncurry, sum_pull]
     conv => lhs; enter[1,i]; rw[sum_swap]
     ac_rfl
 
@@ -38,7 +38,7 @@ abbrev_fun_trans matmul in B : adjoint R by
     intro D
     rw[← adjoint_ex _ (by fun_prop)]
     simp[DataArrayN.inner_def, DataArrayN.matmul, DataArrayN.transpose,
-         sum_over_prod, Function.HasUncurry.uncurry, sum_pull]
+         sum_prod_eq_sum_sum, Function.HasUncurry.uncurry, sum_pull]
     conv => lhs; enter[1,i]; rw[sum_swap]
     rw[sum_swap]
     conv => lhs; enter[1,i]; rw[sum_swap]
diff --git a/SciLean/Data/DataArray/Operations/Outerprod.lean b/SciLean/Data/DataArray/Operations/Outerprod.lean
index 5ecff27f..e493f53c 100644
--- a/SciLean/Data/DataArray/Operations/Outerprod.lean
+++ b/SciLean/Data/DataArray/Operations/Outerprod.lean
@@ -33,7 +33,7 @@ abbrev_fun_trans outerprod in x : adjoint R by
     intro z
     rw[← adjoint_ex _ (by fun_prop)]
     simp[DataArrayN.inner_def, DataArrayN.outerprod, DataArrayN.vecmul,
-         sum_over_prod, sum_pull]
+         sum_prod_eq_sum_sum, sum_pull]
     ac_rfl
 
 abbrev_fun_trans outerprod in y : adjoint R by
@@ -43,7 +43,7 @@ abbrev_fun_trans outerprod in y : adjoint R by
     intro z
     rw[← adjoint_ex _ (by fun_prop)]
     simp[DataArrayN.inner_def, DataArrayN.outerprod, DataArrayN.vecmul, DataArrayN.transpose,
-         sum_over_prod, sum_pull]
+         sum_prod_eq_sum_sum, sum_pull]
     rw[sum_swap]
     ac_rfl
 
diff --git a/SciLean/Data/DataArray/Operations/Simps.lean b/SciLean/Data/DataArray/Operations/Simps.lean
index 43e6f351..a78443e7 100644
--- a/SciLean/Data/DataArray/Operations/Simps.lean
+++ b/SciLean/Data/DataArray/Operations/Simps.lean
@@ -1,4 +1,5 @@
 import SciLean.Data.DataArray.Operations
+import SciLean.Data.ArrayType.Properties
 
 /-! Basic simp theorems about matrix operations -/
 
@@ -7,24 +8,6 @@ namespace SciLean
 
 section Missing
 
-
-theorem sum_over_prod' {R} [AddCommMonoid R] {I J : Type*} [IndexType I] [IndexType J]
-    {f : I → J → R} : ∑ i j, f i j = ∑ (i : I×J), f i.1 i.2  := sorry
-
-theorem sum_over_prod {R} [AddCommMonoid R] {I J : Type*} [IndexType I] [IndexType J]
-    {f : I×J → R} : ∑ i, f i = ∑ i j, f (i,j)  := sorry
-
-@[rsimp]
-theorem sum_ite {R} [AddCommMonoid R] {I : Type*} [IndexType I] [DecidableEq I]
-    {f : I → R} (j : I) : (∑ i, if i = j then f i else 0) = f j  := sorry
-
-@[rsimp]
-theorem sum_ite' {R} [AddCommMonoid R] {I : Type*} [IndexType I] [DecidableEq I]
-    {f : I → R} (j : I) : (∑ i, if j = i then f i else 0) = f j  := sorry
-
-theorem sum_swap {R} [AddCommMonoid R] {I J : Type*} [IndexType I] [IndexType J]
-    {f : I → J → R} : ∑ i j, f i j = ∑ j i, f i j  := sorry
-
 @[simp,simp_core]
 theorem uncurry_appply2 (f : α → β → γ) (x : α) (y : β) :
     (↿f) (x,y) = f x y := rfl
@@ -131,11 +114,10 @@ theorem matmul_neg_pull_right (A : R^[I,J]) (B : R^[J,K]) :
     A*-B = -(A*B) := by
   ext i; cases i;
   simp [neg_pull,matmul_def]
-  sorry_proof
 
 @[neg_push]
 theorem vecmul_neg_push (A : R^[I,J]) (x : R^[J]) :
-    -(A*x) = -A*x := by
+    -(A*x) = A*(-x) := by
   ext i
   simp[vecmul_def]
   sorry_proof
@@ -143,16 +125,25 @@ theorem vecmul_neg_push (A : R^[I,J]) (x : R^[J]) :
 @[neg_pull]
 theorem vecmul_neg_pull_left (A : R^[I,J]) (x : R^[J]) :
     -A*x = -(A*x) := by
-  simp only [neg_push]
+  ext i
+  simp only [neg_pull,vecmul_def]
+
+  sorry_proof
+
+@[neg_push]
+theorem neg_fun_push [Neg X] (f : α → X) :
+    - f = fun x => - (f x) := by rfl
 
 @[neg_pull]
 theorem vecmul_neg_pull_right (A : R^[I,J]) (x : R^[J]) :
     A*-x = -(A*x) := by
   ext i
-  simp [neg_pull,vecmul_def]
+  simp only [neg_pull,vecmul_def]
+  conv => rhs; simp only [neg_push]
   sorry_proof
 
 
+
 theorem vecmul_normalize (A : R^[I,J]) (B : R^[J,K]) :
     A.matmul B = A * B := rfl
 
diff --git a/SciLean/Data/DataArray/Operations/Solve.lean b/SciLean/Data/DataArray/Operations/Solve.lean
index e320e3fc..139c28b5 100644
--- a/SciLean/Data/DataArray/Operations/Solve.lean
+++ b/SciLean/Data/DataArray/Operations/Solve.lean
@@ -89,7 +89,7 @@ theorem solve.arg_A.fwdFDeriv_rule :
   fun_trans (disch:=apply hA')
   cases fwdFDeriv R A x dx; cases fwdFDeriv R b x dx;
   dsimp
-  simp[matmul_assoc,vecmul_assoc,neg_push]
+  simp[matmul_assoc,vecmul_assoc,neg_pull]
 
 
 include hA hA' hB in
diff --git a/SciLean/Data/DataArray/Operations/Sum.lean b/SciLean/Data/DataArray/Operations/Sum.lean
index d81d5c88..a7337ade 100644
--- a/SciLean/Data/DataArray/Operations/Sum.lean
+++ b/SciLean/Data/DataArray/Operations/Sum.lean
@@ -9,15 +9,15 @@ variable
 
 open DataArrayN
 
-def_fun_prop sum in x with_transitive : IsContinuousLinearMap R
+def_fun_prop DataArrayN.sum in x with_transitive : IsContinuousLinearMap R
 
 #generate_linear_map_simps DataArrayN.sum.arg_x.IsLinearMap_rule
 
-abbrev_fun_trans sum in x : fderiv R by fun_trans
+abbrev_fun_trans DataArrayN.sum in x : fderiv R by fun_trans
 
-abbrev_fun_trans sum in x : fwdFDeriv R by autodiff
+abbrev_fun_trans DataArrayN.sum in x : fwdFDeriv R by autodiff
 
-abbrev_fun_trans sum in x : adjoint R by
+abbrev_fun_trans DataArrayN.sum in x : adjoint R by
   equals (fun x' => x' • 1) =>
     funext x
     apply AdjointSpace.ext_inner_left R
@@ -26,14 +26,14 @@ abbrev_fun_trans sum in x : adjoint R by
     simp[DataArrayN.inner_def,Function.HasUncurry.uncurry,
          DataArrayN.sum, sum_pull]
 
-abbrev_fun_trans sum in x : revFDeriv R by
+abbrev_fun_trans DataArrayN.sum in x : revFDeriv R by
   unfold revFDeriv
   autodiff
 
-abbrev_fun_trans sum in x : revFDerivProj R Unit by
+abbrev_fun_trans DataArrayN.sum in x : revFDerivProj R Unit by
   unfold revFDerivProj
   autodiff
 
-abbrev_fun_trans sum in x : revFDerivProjUpdate R Unit by
+abbrev_fun_trans DataArrayN.sum in x : revFDerivProjUpdate R Unit by
   unfold revFDerivProjUpdate
   autodiff
diff --git a/SciLean/Data/DataArray/Operations/Trace.lean b/SciLean/Data/DataArray/Operations/Trace.lean
index d76df4f5..694dadc8 100644
--- a/SciLean/Data/DataArray/Operations/Trace.lean
+++ b/SciLean/Data/DataArray/Operations/Trace.lean
@@ -22,6 +22,6 @@ abbrev_fun_trans trace in A [DecidableEq I] : adjoint R by
     intro z
     rw[← adjoint_ex _ (by fun_prop)]
     simp[DataArrayN.inner_def,Function.uncurry,
-         DataArrayN.trace,identity, sum_pull, sum_over_prod, sum_ite']
+         DataArrayN.trace,identity, sum_pull, sum_prod_eq_sum_sum, sum_ite']
 
 abbrev_fun_trans trace in A : revFDeriv R by unfold revFDeriv; autodiff
diff --git a/SciLean/Data/DataArray/Operations/Transpose.lean b/SciLean/Data/DataArray/Operations/Transpose.lean
index 7c55ed21..adb1c5c8 100644
--- a/SciLean/Data/DataArray/Operations/Transpose.lean
+++ b/SciLean/Data/DataArray/Operations/Transpose.lean
@@ -1,13 +1,9 @@
 import SciLean.Data.DataArray.Operations.Diag
+import SciLean.Data.DataArray.Operations.Vecmul
+import SciLean.Data.DataArray.Operations.Matmul
 
 namespace SciLean
 
-variable
-  {I : Type*} [IndexType I] [DecidableEq I]
-  {J : Type*} [IndexType J] [DecidableEq J]
-  {R : Type*} [RealScalar R] [PlainDataType R]
-
-
 open DataArrayN
 
 def_fun_prop transpose in A
@@ -28,7 +24,58 @@ abbrev_fun_trans transpose in A [RealScalar R] : adjoint R by
     intro z
     rw[← adjoint_ex _ (by fun_prop)]
     simp[DataArrayN.inner_def,Function.HasUncurry.uncurry,
-         DataArrayN.transpose,sum_over_prod]
+         DataArrayN.transpose,sum_prod_eq_sum_sum]
     rw[sum_swap]
 
 abbrev_fun_trans transpose in A [RealScalar R] : revFDeriv R by unfold revFDeriv; autodiff
+
+
+
+variable
+  {I : Type} [IndexType I]
+  {J : Type} [IndexType J]
+  {R : Type} [RealScalar R] [PlainDataType R]
+
+set_default_scalar R
+
+variable (A : R^[I,J]) (x y : R^[I]) (u v : R^[J])
+
+omit [RealScalar R] in
+@[simp, simp_core]
+theorem transpose_transpose : Aᵀᵀ = A := by ext i; cases i; simp[transpose]
+
+-- TODO: move this
+@[sum_pull]
+theorem ArrayType.ofFn.arg_f.sum_pull (f : I → J → R) : ⊞ i => ∑ j, f i j = ∑ j, ⊞ i => f i j := by
+  ext
+  simp
+
+-- TODO: move this
+@[sum_pull]
+theorem ArrayType.get.arg_cont.sum_pull {X} [AddCommGroup X] [ArrayType Cont I X] (i : I)
+  (f : J → Cont) : ArrayType.get (∑ j, f j) i = ∑ j, ArrayType.get (f j) i := sorry_proof
+
+theorem inner_transpose_right : ⟪x, A*v⟫ = ⟪Aᵀ*x, v⟫ := by
+  rw[← adjoint_inner_left _ (by fun_prop)]
+  fun_trans
+
+theorem inner_transpose_left : ⟪A*u, y⟫ = ⟪u, Aᵀ*y⟫ := by
+  rw[← adjoint_inner_right _ (by fun_prop)]
+  fun_trans
+
+
+-- TODO: remove simp from this!
+#check ArrayType.sum_ofFn
+--set_option trace.Meta.Tactic.simp.unify true in
+
+theorem inner_AAT_right : ⟪x, A*(Aᵀ*y)⟫ = ⟪Aᵀ*x,Aᵀ*y⟫ := by
+  rw[inner_transpose_right]
+theorem inner_AAT_letft : ⟪A*(Aᵀ*x), y⟫ = ⟪Aᵀ*x,Aᵀ*y⟫ := by
+  rw[inner_transpose_left]
+
+theorem inner_ATA_right : ⟪u, Aᵀ*(A*v)⟫ = ⟪A*u,A*v⟫ := by
+  rw[inner_transpose_right]
+  simp
+theorem inner_ATA_letft : ⟪Aᵀ*(A*u), v⟫ = ⟪A*u,A*v⟫ := by
+  rw[inner_transpose_left]
+  simp
diff --git a/SciLean/Data/DataArray/Operations/Uncurry.lean b/SciLean/Data/DataArray/Operations/Uncurry.lean
index 23ded6c8..fff7611f 100644
--- a/SciLean/Data/DataArray/Operations/Uncurry.lean
+++ b/SciLean/Data/DataArray/Operations/Uncurry.lean
@@ -38,7 +38,7 @@ abbrev_fun_trans uncurry in x
     apply AdjointSpace.ext_inner_left R
     intro z
     rw[← adjoint_ex _ (by fun_prop)]
-    simp only [inner, uncurry_def, ArrayType.get_ofFn', sum_over_prod, uncurry_appply2, curry_def]
+    simp only [inner, uncurry_def, ArrayType.get_ofFn', sum_prod_eq_sum_sum, uncurry_appply2, curry_def]
 
 abbrev_fun_trans uncurry in x
     {R} [RCLike R] [NormedAddCommGroup α] [AdjointSpace R α] [CompleteSpace α] :
diff --git a/SciLean/Data/DataArray/Operations/Vecmul.lean b/SciLean/Data/DataArray/Operations/Vecmul.lean
index 94c66607..2861a83c 100644
--- a/SciLean/Data/DataArray/Operations/Vecmul.lean
+++ b/SciLean/Data/DataArray/Operations/Vecmul.lean
@@ -27,7 +27,7 @@ abbrev_fun_trans vecmul in A : adjoint R by
     intro z
     rw[← adjoint_ex _ (by fun_prop)]
     simp[DataArrayN.inner_def, DataArrayN.vecmul, DataArrayN.outerprod,
-         sum_over_prod, Function.HasUncurry.uncurry, sum_pull]
+         sum_prod_eq_sum_sum, Function.HasUncurry.uncurry, sum_pull]
     ac_rfl
 
 abbrev_fun_trans vecmul in x : adjoint R by
@@ -37,7 +37,7 @@ abbrev_fun_trans vecmul in x : adjoint R by
     intro z
     rw[← adjoint_ex _ (by fun_prop)]
     simp[DataArrayN.inner_def, DataArrayN.vecmul, DataArrayN.transpose,
-         sum_over_prod, Function.HasUncurry.uncurry, sum_pull]
+         sum_prod_eq_sum_sum, Function.HasUncurry.uncurry, sum_pull]
     rw[sum_swap]
     ac_rfl
 
diff --git a/SciLean/Data/IndexType/SumProduct.lean b/SciLean/Data/IndexType/SumProduct.lean
index f794c1d3..f7eaea21 100644
--- a/SciLean/Data/IndexType/SumProduct.lean
+++ b/SciLean/Data/IndexType/SumProduct.lean
@@ -2,8 +2,6 @@ import SciLean.Data.IndexType.Operations
 
 namespace SciLean
 
-namespace IndexType
-
 variable {ι : Type*} [IndexType ι]
 
 @[specialize] def sum {α : Type u} [Zero α] [Add α] (f : ι → α) : α :=
@@ -38,6 +36,8 @@ macro (priority:=high) " ∏ " xs:Lean.explicitBinders ", " b:term:66 : term =>
   | _  => throw ()
 
 
+theorem sum_swap {R} [AddCommMonoid R] {I J : Type*} [IndexType I] [IndexType J]
+    {f : I → J → R} : ∑ i j, f i j = ∑ j i, f i j  := sorry_proof
 
 @[sum_push]
 theorem sum_pair {I X : Type _} [Add X] [Zero X] [Add Y] [Zero Y] [IndexType I]
@@ -58,6 +58,20 @@ theorem sum_linearize {I X : Type _} [Add X] [Zero X] [IndexType I] (f : I → X
     ∑ i : Fin (size I), f (fromFin i) := by simp only [sum]; rw[reduce_linearize]
 
 
+theorem sum_sum_eq_sum_prod {R} [AddCommMonoid R] {I J : Type*} [IndexType I] [IndexType J]
+    {f : I → J → R} : ∑ i j, f i j = ∑ (i : I×J), f i.1 i.2  := sorry_proof
+
+theorem sum_prod_eq_sum_sum {R} [AddCommMonoid R] {I J : Type*} [IndexType I] [IndexType J]
+    {f : I×J → R} : ∑ i, f i = ∑ i j, f (i,j)  := sorry_proof
+
+@[rsimp]
+theorem sum_ite {R} [AddCommMonoid R] {I : Type*} [IndexType I] [DecidableEq I]
+    {f : I → R} (j : I) : (∑ i, if i = j then f i else 0) = f j  := sorry_proof
+
+@[rsimp]
+theorem sum_ite' {R} [AddCommMonoid R] {I : Type*} [IndexType I] [DecidableEq I]
+    {f : I → R} (j : I) : (∑ i, if j = i then f i else 0) = f j  := sorry_proof
+
 
 variable {I : Type*} [IndexType I]
 
@@ -72,6 +86,17 @@ theorem add_sum (f g : I → α) : (∑ i, f i) + (∑ i, g i) = ∑ i , (f i +
 
 end OnMonoid
 
+section OnGroup
+variable [AddCommGroup α]
+
+@[neg_push, sum_pull]
+theorem neg_sum (f : I → α) : -(∑ i, f i) = ∑ i , -(f i) := by sorry_proof
+
+@[neg_pull, sum_push]
+theorem sum_neg (f : I → α) : (∑ i, -f i) = - ∑ i , (f i) := by simp only [neg_push]
+
+end OnGroup
+
 
 
 section OnSemiring
diff --git a/SciLean/Tactic/DataSynth/HasRevFDerivUpdate.lean b/SciLean/Tactic/DataSynth/HasRevFDerivUpdate.lean
index b86f58eb..7fc8481b 100644
--- a/SciLean/Tactic/DataSynth/HasRevFDerivUpdate.lean
+++ b/SciLean/Tactic/DataSynth/HasRevFDerivUpdate.lean
@@ -290,7 +290,7 @@ theorem HPow.hPow.arg_a0.HasRevFDerivUpdate_rule
 
 
 @[data_synth]
-theorem IndexType.sum.arg_f.HasRevFDerivUpdate
+theorem sum.arg_f.HasRevFDerivUpdate
   {I : Type} [IndexType I]
   (f : W → I → X) (f' : I → _) (hz : ∀ i, HasRevFDerivUpdate R (f · i) (f' i)) :
   HasRevFDerivUpdate R