diff --git a/SciLean/Core/FunctionTransformations/RevCDeriv.lean b/SciLean/Core/FunctionTransformations/RevCDeriv.lean
index 6e879ad6..ee8be755 100644
--- a/SciLean/Core/FunctionTransformations/RevCDeriv.lean
+++ b/SciLean/Core/FunctionTransformations/RevCDeriv.lean
@@ -50,6 +50,13 @@ theorem revCDeriv_fst (f : X → Y) (x : X)
 by
   rfl
 
+@[simp, ftrans_simp]
+theorem revCDeriv_snd_zero (f : X → Y) (x : X)
+  : (revCDeriv K f x).2 0 = 0 := 
+by
+  simp[revCDeriv]
+
+
 @[ftrans]
 theorem semiAdjoint.arg_a3.cderiv_rule
   (f : X → Y) (a0 : W → Y) (ha0 : IsDifferentiable K a0)
diff --git a/SciLean/Core/FunctionTransformations/RevDerivProj.lean b/SciLean/Core/FunctionTransformations/RevDerivProj.lean
index b5b828a5..a5c3bd30 100644
--- a/SciLean/Core/FunctionTransformations/RevDerivProj.lean
+++ b/SciLean/Core/FunctionTransformations/RevDerivProj.lean
@@ -22,6 +22,7 @@ variable
   [SemiInnerProductSpace K F] [∀ j, SemiInnerProductSpace K (FJ j)]
   [SemiInnerProductSpaceStruct K F J FJ]
 
+
 noncomputable
 def revDerivProj
   (f : X → E) (x : X) : E×((i : I)→EI i→X) :=
@@ -37,19 +38,42 @@ def revDerivProjUpdate
   (ydf'.1, fun i de dx => dx + ydf'.2 i de)
 
 
-
 @[simp, ftrans_simp]
 theorem revDerivProj_fst (f : X → E) (x : X)
   : (revDerivProj K f x).1 = f x :=
 by
   rfl
 
+@[simp, ftrans_simp]
+theorem revDerivProj_snd_zero (f : X → E) (x : X) (i : I)
+  : (revDerivProj K f x).2 i 0 = 0 := 
+by
+  simp[revDerivProj]
+  conv in (StructLike.make _) => 
+    equals (0:E) =>
+      apply StructLike.ext
+      intro i'; simp
+      if h : i=i' then subst h; simp else simp[h]
+  simp
+
 @[simp, ftrans_simp]
 theorem revDerivProjUpdate_fst (f : X → E) (x : X)
   : (revDerivProjUpdate K f x).1 = f x :=
 by
   rfl
 
+@[simp, ftrans_simp]
+theorem revDerivProjUpdate_snd_zero (f : X → E) (x dx : X) (i : I)
+  : (revDerivProjUpdate K f x).2 i 0 dx = dx := 
+by
+  simp[revDerivProjUpdate]
+
+@[simp, ftrans_simp]
+theorem revDerivProjUpdate_snd_zero' (f : X → Y) (x : X) (dy : Y)
+  : (revDerivUpdate K f x).2 dy 0 = (revCDeriv K f x).2 dy := 
+by
+  simp[revDerivUpdate]
+
 
 --------------------------------------------------------------------------------
 
@@ -182,6 +206,7 @@ theorem revDerivProj.comp_rule
 by
   simp[revDerivProj]
   ftrans
+  rfl 
 
 
 theorem revDerivProjUpdate.comp_rule
@@ -198,15 +223,7 @@ theorem revDerivProjUpdate.comp_rule
 by
   funext x
   simp[revDerivProjUpdate,revDerivProj.comp_rule _ _ _ hf hg]
-  constructor
-  . sorry
-  . 
-    funext i de dx
-    if h :i=i' then
-      subst h; simp
-    else
-      simp[h]
-
+  rfl
 
 theorem revDerivProj.let_rule
   (f : X → Y → E) (g : X → Y)
@@ -219,10 +236,11 @@ theorem revDerivProj.let_rule
       (zdf'.1,
        fun i dei => 
          let dxy := zdf'.2 i dei
-         ydg'.2 dxy.2 1 dxy.1) := 
+         ydg'.2 dxy.2 dxy.1) := 
 by
-  sorry_proof
-
+  unfold revDerivProj
+  ftrans
+  rfl
 
 theorem revDerivProjUpdate.let_rule
   (f : X → Y → E) (g : X → Y)
@@ -235,28 +253,46 @@ theorem revDerivProjUpdate.let_rule
       (zdf'.1,
        fun i dei dx => 
          let dxy := zdf'.2 i dei (dx,0)
-         ydg'.2 dxy.2 1 dxy.1) := 
+         ydg'.2 dxy.2 dxy.1) := 
 by
-  sorry_proof
+  unfold revDerivProjUpdate
+  simp [revDerivProj.let_rule _ _ _ hf hg,add_assoc,add_comm,revDerivUpdate]
 
 
 theorem revDerivProj.pi_rule
-  (f :  X → ι → E) (hf : ∀ i, HasAdjDiff K (f · i))
-  : (revDerivProj K fun (x : X) (i : ι) => f x i)
+  (f :  X → ι → Y) (hf : ∀ i, HasAdjDiff K (f · i))
+  : (@revDerivProj K _ _ _ _ Unit (fun _ => ι→Y) (instStrucLikeDefault) _ _ fun (x : X) (i : ι) => f x i)
     =
-    revDerivProj K fun x => f x := by rfl
+    fun x =>
+      let ydf := revDerivProjUpdate K f x
+      (fun i => ydf.1 i, 
+       fun _ df => Id.run do
+         let mut dx : X := 0
+         for i in fullRange ι do
+           dx := ydf.2 (i,()) (df i) dx
+         dx) := 
+by
+  sorry_proof
 
 
 theorem revDerivProjUpdate.pi_rule
-  (f :  X → ι → E) (hf : ∀ i, HasAdjDiff K (f · i))
-  : (revDerivProjUpdate K fun (x : X) (i : ι) => f x i)
+  (f :  X → ι → Y) (hf : ∀ i, HasAdjDiff K (f · i))
+  : (@revDerivProjUpdate K _ _ _ _ Unit (fun _ => ι→Y) (StructLike.instStructLikeDefault) _ _ fun (x : X) (i : ι) => f x i)
     =
-    revDerivProjUpdate K fun x => f x := by rfl
+    fun x =>
+      let ydf := revDerivProjUpdate K f x
+      (fun i => ydf.1 i, 
+       fun _ df dx => Id.run do
+         let mut dx : X := dx
+         for i in fullRange ι do
+           dx := ydf.2 (i,()) (df i) dx
+         dx) := 
+by
+  sorry_proof
 
 
 
 --------------------------------------------------------------------------------
-
 -- Register `revDerivProj` as function transformation --------------------------
 --------------------------------------------------------------------------------
 
@@ -301,8 +337,11 @@ def ftransExt : FTransExt where
 
   idRule  e X := do
     let .some K := e.getArg? 0 | return none
+    IO.println "hih"
+    let proof ← mkAppOptM ``id_rule #[K,none, X,none,none,none,none,none]
+    IO.println s!"proof of {← inferType proof}"
     tryTheorems
-      #[ { proof := ← mkAppM ``id_rule #[K, X], origin := .decl ``id_rule, rfl := false} ]
+      #[ { proof := ← mkAppOptM ``id_rule #[K,none, X,none,none,none,none,none], origin := .decl ``id_rule, rfl := false} ]
       discharger e
 
   constRule e X y := do
@@ -387,8 +426,11 @@ def ftransExt : FTransExt where
 
   idRule  e X := do
     let .some K := e.getArg? 0 | return none
+    IO.println "hih"
+    let proof ← mkAppOptM ``id_rule #[K,none, X,none,none,none,none,none,none,none]
+    IO.println s!"proof of {← inferType proof}"
     tryTheorems
-      #[ { proof := ← mkAppM ``id_rule #[K, X], origin := .decl ``id_rule, rfl := false} ]
+      #[ { proof := ← mkAppOptM ``id_rule #[K,none, X,none,none,none,none,none,none,none], origin := .decl ``id_rule, rfl := false} ]
       discharger e
 
   constRule e X y := do
@@ -434,44 +476,22 @@ end revDerivProjUpdate
 
 
 --------------------------------------------------------------------------------
-
-
-
 --------------------------------------------------------------------------------
+
 end SciLean
 open SciLean
 
 variable 
   {K : Type _} [IsROrC K]
-  {X Xi : Type} {XI : Xi → Type} [StructLike X Xi XI] [DecidableEq Xi]
-  {Y Yi : Type} {YI : Yi → Type} [StructLike Y Yi YI] [DecidableEq Yi]
-  {Z Zi : Type} {ZI : Zi → Type} [StructLike Z Zi ZI] [DecidableEq Zi]
-  [SemiInnerProductSpace K X] [∀ i, SemiInnerProductSpace K (XI i)]
-  [SemiInnerProductSpace K Y] [∀ i, SemiInnerProductSpace K (YI i)]
-  [SemiInnerProductSpace K Z] [∀ i, SemiInnerProductSpace K (ZI i)]
+  {X Xi : Type _} {XI : Xi → Type _} [StructLike X Xi XI] [EnumType Xi]
+  {Y Yi : Type _} {YI : Yi → Type _} [StructLike Y Yi YI] [EnumType Yi]
+  {Z Zi : Type _} {ZI : Zi → Type _} [StructLike Z Zi ZI] [EnumType Zi]
+  [SemiInnerProductSpace K X] [∀ i, SemiInnerProductSpace K (XI i)] [SemiInnerProductSpaceStruct K X Xi XI]
+  [SemiInnerProductSpace K Y] [∀ i, SemiInnerProductSpace K (YI i)] [SemiInnerProductSpaceStruct K Y Yi YI]
+  [SemiInnerProductSpace K Z] [∀ i, SemiInnerProductSpace K (ZI i)] [SemiInnerProductSpaceStruct K Z Zi ZI]
   {W : Type _} [SemiInnerProductSpace K W]
   {ι : Type _} [EnumType ι]
 
-@[simp]
-theorem StruckLike.make_zero
-  {X I : Type}  {XI : I → Type} [StructLike X I XI] 
-  [Zero X] [∀ i, Zero (XI i)]
-  : StructLike.make (E:=X) (fun _ => 0)
-    =
-    0 :=
-by
-  sorry
-
-@[simp]
-theorem revCDeriv_snd_zero
-  (f : X → Y) (x : X)
-  : (revCDeriv K f x).2 0 = 0 := sorry
-
-@[simp]
-theorem revDerivUpdate_snd_zero 
-  (f : X → Y) (x : X)
-  : (revDerivUpdate K f x).2 0 k dy = dy := sorry
-
 
 -- Prod.mk ---------------------------------------------------------------------
 --------------------------------------------------------------------------------
@@ -501,6 +521,7 @@ by
       subst h; rfl
     }
 
+
 @[ftrans]
 theorem Prod.mk.arg_fstsnd.revDerivProjUpdate_rule
   (g : X → Y) (f : X → Z)
@@ -519,13 +540,11 @@ by
   unfold revDerivProjUpdate
   funext x; ftrans; simp
   funext i de dx
-  induction i <;>
-  { simp[StructLike.make]
-    sorry_proof
-  }
+  induction i <;> simp
 
 
-------------------------
+-- Prod.fst --------------------------------------------------------------------
+--------------------------------------------------------------------------------
 
 @[ftrans]
 theorem Prod.fst.arg_self.revDerivProj_rule
@@ -557,35 +576,487 @@ theorem Prod.fst.arg_self.revDerivProjUpdate_rule
 by
   unfold revDerivProjUpdate
   funext x; ftrans; simp
-  funext e dxy dw
-  simp[StructLike.make]
-  -- apply congr_arg -- this fails for some reason :(
-  -- congr; funext i; congr; funext h; subst h; rfl
-  sorry_proof
-
 
 
+-- Prod.fst --------------------------------------------------------------------
+--------------------------------------------------------------------------------
 
-theorem Prod.fst.arg_self.revDeriv_rule 
+@[ftrans]
+theorem Prod.snd.arg_self.revDerivProj_rule
   (f : W → X×Y) (hf : HasAdjDiff K f)
-  : revCDeriv K (fun w => (f w).1)
+  : revDerivProj K (fun x => (f x).2)
     =
     fun w => 
-      let xydf' := revDerivProj K f w
-      (xydf'.1.1, fun dx => xydf'.2 (.inl ()) dx) :=
+      let xydf := revDerivProj K f w
+      (xydf.1.2,
+       fun i dxy => xydf.2 (.inr i) dxy) := 
 by
-  sorry_proof
+  unfold revDerivProj
+  funext x; ftrans; simp
+  funext e dxy
+  simp[StructLike.make]
+  apply congr_arg
+  congr; funext i; congr; funext h; subst h; rfl
 
 
-theorem Prod.fst.arg_self.revDerivProj_rule
-  {X I : Type _} {XI : I → Type _} 
-  [StructLike X I XI] [SemiInnerProductSpace K X] [∀ i, SemiInnerProductSpace K (XI i)]
+@[ftrans]
+theorem Prod.snd.arg_self.revDerivProjUpdate_rule
   (f : W → X×Y) (hf : HasAdjDiff K f)
-  : revDerivProj K (fun w => (f w).1)
+  : revDerivProjUpdate K (fun x => (f x).2)
     =
     fun w => 
-      let xydf' := revDerivProj K f w
-      (xydf'.1.1,
-       fun i dx => xydf'.2 (.inl i) dx) :=
+      let xydf := revDerivProjUpdate K f w
+      (xydf.1.2,
+       fun i dxy dw => xydf.2 (.inr i) dxy dw) := 
+by
+  unfold revDerivProjUpdate
+  funext x; ftrans; simp
+
+
+
+-- HAdd.hAdd -------------------------------------------------------------------
+--------------------------------------------------------------------------------
+
+@[ftrans]
+theorem HAdd.hAdd.arg_a0a1.revDerivProj_rule
+  (f g : X → Y) (hf : HasAdjDiff K f) (hg : HasAdjDiff K g)
+  : (revDerivProj K fun x => f x + g x)
+    =
+    fun x => 
+      let ydf := revDerivProj K f x
+      let ydg := revDerivProjUpdate K g x
+      (ydf.1 + ydg.1, 
+       fun i dy => (ydg.2 i dy (ydf.2 i dy))) := 
+by 
+  unfold revDerivProjUpdate; unfold revDerivProj
+  ftrans
+
+
+@[ftrans]
+theorem HAdd.hAdd.arg_a0a1.revDerivProjUpdate_rule
+  (f g : X → Y) (hf : HasAdjDiff K f) (hg : HasAdjDiff K g)
+  : (revDerivProjUpdate K fun x => f x + g x)
+    =
+    fun x => 
+      let ydf := revDerivProjUpdate K f x
+      let ydg := revDerivProjUpdate K g x
+      (ydf.1 + ydg.1, fun i dy dx => ydg.2 i dy (ydf.2 i dy dx)) := 
+by 
+  unfold revDerivProjUpdate
+  ftrans; simp[revDerivProjUpdate, add_assoc]
+
+
+-- HSub.hSub -------------------------------------------------------------------
+--------------------------------------------------------------------------------
+
+@[ftrans]
+theorem HSub.hSub.arg_a0a1.revDerivProj_rule
+  (f g : X → Y) (hf : HasAdjDiff K f) (hg : HasAdjDiff K g)
+  : (revDerivProj K fun x => f x - g x)
+    =
+    fun x => 
+      let ydf := revDerivProj K f x
+      let ydg := revDerivProjUpdate K g x
+      (ydf.1 - ydg.1, 
+       fun i dy => (ydg.2 i (-dy) (ydf.2 i dy))) := 
+by 
+  unfold revDerivProjUpdate; unfold revDerivProj
+  ftrans; simp; sorry_proof -- pulling the minus out is just tedious ...
+
+
+@[ftrans]
+theorem HSub.hSub.arg_a0a1.revDerivProjUpdate_rule
+  (f g : X → Y) (hf : HasAdjDiff K f) (hg : HasAdjDiff K g)
+  : (revDerivProjUpdate K fun x => f x - g x)
+    =
+    fun x => 
+      let ydf := revDerivProjUpdate K f x
+      let ydg := revDerivProjUpdate K g x
+      (ydf.1 - ydg.1, fun i dy dx => ydg.2 i (-dy) (ydf.2 i dy dx)) := 
+by 
+  unfold revDerivProjUpdate
+  ftrans; simp[revDerivProjUpdate, add_assoc]
+
+
+-- Neg.neg ---------------------------------------------------------------------
+--------------------------------------------------------------------------------
+
+@[ftrans]
+theorem Neg.neg.arg_a0.revDerivProj_rule
+  (f : X → Y)
+  : (revDerivProj K fun x => - f x)
+    =
+    fun x => 
+      let ydf := revDerivProj K f x
+      (-ydf.1, fun i dy => ydf.2 i (-dy)) :=
+by 
+  unfold revDerivProj; ftrans; simp; sorry_proof -- pulling the minus out is just tedious ...
+
+@[ftrans]
+theorem Neg.neg.arg_a0.revDerivProjUpdate_rule
+  (f : X → Y)
+  : (revDerivProjUpdate K fun x => - f x)
+    =
+    fun x => 
+      let ydf := revDerivProjUpdate K f x
+      (-ydf.1, fun i dy dx => ydf.2 i (-dy) dx) :=
+by 
+  unfold revDerivProjUpdate; ftrans
+
+
+-- HMul.hmul -------------------------------------------------------------------
+--------------------------------------------------------------------------------
+open ComplexConjugate
+
+@[ftrans]
+theorem HMul.hMul.arg_a0a1.revDerivProj_rule
+  (f g : X → K)
+  (hf : HasAdjDiff K f) (hg : HasAdjDiff K g)
+  : (revDerivProj K fun x => f x * g x)
+    =
+    fun x => 
+      let ydf := revDerivUpdate K f x
+      let zdg := revCDeriv K g x
+      (ydf.1 * zdg.1, fun _ dy => ydf.2 ((conj zdg.1)*dy) (zdg.2 (conj ydf.1* dy))) :=
+by 
+  unfold revDerivProj
+  ftrans; funext x; simp[revDerivUpdate,StructLike.make]; funext _ dy
+  sorry_proof -- just need to pull those multiplcations out
+
+
+@[ftrans]
+theorem HMul.hMul.arg_a0a1.revDerivProjUpdate_rule
+  (f g : X → K)
+  (hf : HasAdjDiff K f) (hg : HasAdjDiff K g)
+  : (revDerivProjUpdate K fun x => f x * g x)
+    =
+    fun x => 
+      let ydf := revDerivUpdate K f x
+      let zdg := revDerivUpdate K g x
+      (ydf.1 * zdg.1, fun _ dy dx => ydf.2 ((conj zdg.1)*dy) (zdg.2 (conj ydf.1* dy) dx)) :=
+by 
+  unfold revDerivProjUpdate
+  ftrans; simp[revDerivUpdate,add_assoc]
+  
+
+-- SMul.smul -------------------------------------------------------------------
+--------------------------------------------------------------------------------
+
+@[ftrans]
+theorem HSMul.hSMul.arg_a0a1.revDerivProj_rule
+  {Y Yi : Type _} {YI : Yi → Type _} [StructLike Y Yi YI] [EnumType Yi]
+  [SemiHilbert K Y] [∀ i, SemiHilbert K (YI i)] [SemiInnerProductSpaceStruct K Y Yi YI]
+  (f : X → K) (g : X → Y)
+  (hf : HasAdjDiff K f) (hg : HasAdjDiff K g)
+  : (revDerivProj K fun x => f x • g x)
+    =
+    fun x => 
+      let ydf := revDerivUpdate K f x
+      let zdg := revDerivProj K g x
+      (ydf.1 • zdg.1, fun i (dy : YI i) => ydf.2 (inner (StructLike.proj zdg.1 i) dy) (zdg.2 i (conj ydf.1•dy))) :=
+by 
+  unfold revDerivProj
+  ftrans; funext x; simp; funext i dy
+  simp[revDerivUpdate]
+  sorry_proof -- this requires some lemma about inner product with StruckLike types
+
+@[ftrans]
+theorem HSMul.hSMul.arg_a0a1.revDerivProjUpdate_rule
+  {Y Yi : Type} {YI : Yi → Type} [StructLike Y Yi YI] [EnumType Yi]
+  [SemiHilbert K Y] [∀ i, SemiHilbert K (YI i)] [SemiInnerProductSpaceStruct K Y Yi YI]
+  (f : X → K) (g : X → Y)
+  (hf : HasAdjDiff K f) (hg : HasAdjDiff K g)
+  : (revDerivProjUpdate K fun x => f x • g x)
+    =
+    fun x => 
+      let ydf := revDerivUpdate K f x
+      let zdg := revDerivProjUpdate K g x
+      (ydf.1 • zdg.1, fun i (dy : YI i) dx => ydf.2 (inner (StructLike.proj zdg.1 i) dy) (zdg.2 i (conj ydf.1•dy) dx)) :=
+by 
+  unfold revDerivProjUpdate
+  ftrans; simp[revDerivUpdate]; funext x; simp; funext i dy dx
+  simp[add_assoc]
+
+
+
+-- HDiv.hDiv -------------------------------------------------------------------
+--------------------------------------------------------------------------------
+
+
+@[ftrans]
+theorem HDiv.hDiv.arg_a0a1.revDerivProj_rule
+  (f g : X → K)
+  (hf : HasAdjDiff K f) (hg : HasAdjDiff K g) (hx : ∀ x, g x ≠ 0)
+  : (revDerivProj K fun x => f x / g x)
+    =
+    fun x => 
+      let ydf := revCDeriv K f x
+      let zdg := revDerivUpdate K g x
+      (ydf.1 / zdg.1, 
+       -- fun dy k dx => (1 / (conj zdg.1)^2) • (conj zdg.1 • ydf.2 dy - conj ydf.1 • zdg.2 dy)) :=
+       fun _ dy =>  
+         let factor := ((conj zdg.1)^2)⁻¹
+         let dy := factor * dy
+         zdg.2 (-conj ydf.1 * dy) (ydf.2 (conj zdg.1 * dy))) :=
+by 
+  sorry_proof
+
+@[ftrans]
+theorem HDiv.hDiv.arg_a0a1.revDerivProjUpdate_rule
+  (f g : X → K)
+  (hf : HasAdjDiff K f) (hg : HasAdjDiff K g) (hx : ∀ x, g x ≠ 0)
+  : (revDerivProjUpdate K fun x => f x / g x)
+    =
+    fun x => 
+      let ydf := revDerivUpdate K f x
+      let zdg := revDerivUpdate K g x
+      (ydf.1 / zdg.1, 
+       fun _ dy dx =>  
+         let factor := ((conj zdg.1)^2)⁻¹
+         let dy := factor * dy
+         zdg.2 (-conj ydf.1 * dy) (ydf.2 (conj zdg.1 * dy) dx)) :=
+by 
+  sorry_proof
+
+
+-- HPow.hPow -------------------------------------------------------------------
+-------------------------------------------------------------------------------- 
+
+@[ftrans]
+def HPow.hPow.arg_a0.revDerivProj_rule
+  (f : X → K) (n : Nat) (hf : HasAdjDiff K f) 
+  : revDerivProj K (fun x => f x ^ n)
+    =
+    fun x => 
+      let ydf := revCDeriv K f x
+      (ydf.1 ^ n, 
+       fun _ dy => ydf.2 (n * (conj ydf.1 ^ (n-1)) * dy)) :=
+by 
+  sorry_proof
+
+
+@[ftrans]
+def HPow.hPow.arg_a0.revDerivProjUpdate_rule
+  (f : X → K) (n : Nat) (hf : HasAdjDiff K f) 
+  : revDerivProjUpdate K (fun x => f x ^ n)
+    =
+    fun x => 
+      let ydf := revDerivUpdate K f x
+      (ydf.1 ^ n, 
+       fun _ dy dx => ydf.2 (n * (conj ydf.1 ^ (n-1)) * dy) dx) :=
+by 
+  unfold revDerivProjUpdate; 
+  ftrans; simp[revDerivUpdate]
+
+
+-- EnumType.sum ----------------------------------------------------------------
+-------------------------------------------------------------------------------- 
+
+@[ftrans]
+theorem SciLean.EnumType.sum.arg_f.revDerivProj_rule {ι : Type _} [EnumType ι]
+  (f : X → ι → Y) (hf : ∀ i, HasAdjDiff K (fun x => f x i))
+  : revDerivProj K (fun x => ∑ i, f x i)
+    =
+    fun x => 
+      let ydf := revDerivProjUpdate K f x
+      (∑ i, ydf.1 i, 
+       fun i dy => Id.run do
+         let mut dx : X := 0
+         for j in fullRange ι do
+           dx := ydf.2 (j,i) dy dx
+         dx) :=
 by
   sorry_proof
+
+
+@[ftrans]
+theorem SciLean.EnumType.sum.arg_f.revDerivProjUpdate_rule {ι : Type _} [EnumType ι]
+  (f : X → ι → Y) (hf : ∀ i, HasAdjDiff K (fun x => f x i))
+  : revDerivProjUpdate K (fun x => ∑ i, f x i)
+    =
+    fun x => 
+      let ydf := revDerivProjUpdate K f x
+      (∑ i, ydf.1 i, 
+       fun i dy dx => Id.run do
+         let mut dx : X := dx
+         for j in fullRange ι do
+           dx := ydf.2 (j,i) dy dx
+         dx) :=
+by
+  sorry_proof
+
+
+--------------------------------------------------------------------------------
+
+section InnerProductSpace
+
+variable 
+  {R : Type _} [RealScalar R]
+  -- {K : Type _} [Scalar R K]
+  {X : Type _} [SemiInnerProductSpace R X]
+  {X Xi : Type _} {XI : Xi → Type _} [StructLike X Xi XI] [EnumType Xi]
+  {Y Yi : Type _} {YI : Yi → Type _} [StructLike Y Yi YI] [EnumType Yi]
+  [SemiHilbert R Y] [∀ i, SemiHilbert R (YI i)] [SemiInnerProductSpaceStruct R Y Yi YI]
+  [SemiInnerProductSpace R X] [∀ i, SemiInnerProductSpace R (XI i)] [SemiInnerProductSpaceStruct R X Xi XI]
+
+  -- [SemiInnerProductSpace K Y] [∀ i, SemiInnerProductSpace K (YI i)] [SemiInnerProductSpaceStruct K Y Yi YI]
+  -- [SemiInnerProductSpace K Z] [∀ i, SemiInnerProductSpace K (ZI i)] [SemiInnerProductSpaceStruct K Z Zi ZI]
+  -- {W : Type _} [SemiInnerProductSpace K W]
+
+
+-- Inner -----------------------------------------------------------------------
+-------------------------------------------------------------------------------- 
+
+open ComplexConjugate
+
+@[ftrans]
+theorem Inner.inner.arg_a0a1.revDerivProj_rule
+  (f : X → Y) (g : X → Y)
+  (hf : HasAdjDiff R f) (hg : HasAdjDiff R g)
+  : (revDerivProj R fun x => ⟪f x, g x⟫[R])
+    =
+    fun x => 
+      let y₁df := revCDeriv R f x
+      let y₂dg := revDerivUpdate R g x
+      let dx₁ := y₁df.2 y₂dg.1
+      let dx₂ := y₂dg.2 y₁df.1
+      (⟪y₁df.1, y₂dg.1⟫[R],
+       fun i dr => 
+         y₂dg.2 (dr • y₁df.1) (y₁df.2 (conj dr • y₂dg.1))) := 
+by 
+  sorry_proof
+
+@[ftrans]
+theorem Inner.inner.arg_a0a1.revDerivProjUpdate_rule
+  (f : X → Y) (g : X → Y)
+  (hf : HasAdjDiff R f) (hg : HasAdjDiff R g)
+  : (revDerivProjUpdate R fun x => ⟪f x, g x⟫[R])
+    =
+    fun x => 
+      let y₁df := revDerivUpdate R f x
+      let y₂dg := revDerivUpdate R g x
+      let dx₁ := y₁df.2 y₂dg.1
+      let dx₂ := y₂dg.2 y₁df.1
+      (⟪y₁df.1, y₂dg.1⟫[R],
+       fun i dr dx => 
+         y₂dg.2 (dr • y₁df.1) (y₁df.2 (conj dr • y₂dg.1) dx) ) := 
+by       
+  unfold revDerivProjUpdate
+  ftrans; simp[add_assoc,revDerivUpdate]
+
+
+@[ftrans]
+theorem SciLean.Norm2.norm2.arg_a0.revDerivProj_rule
+  (f : X → Y) (hf : HasAdjDiff R f)
+  : (revDerivProj R fun x => ‖f x‖₂²[R])
+    =
+    fun x => 
+      let ydf := revCDeriv R f x
+      let ynorm2 := ‖ydf.1‖₂²[R]
+      (ynorm2,
+       fun _ dr => 
+          ydf.2 (((2:R)*dr)•ydf.1)) :=
+by 
+  sorry_proof
+
+@[ftrans]
+theorem SciLean.Norm2.norm2.arg_a0.revDerivProjUpdate_rule
+  (f : X → Y) (hf : HasAdjDiff R f)
+  : (revDerivProjUpdate R fun x => ‖f x‖₂²[R])
+    =
+    fun x => 
+      let ydf := revDerivUpdate R f x
+      let ynorm2 := ‖ydf.1‖₂²[R]
+      (ynorm2,
+       fun _ dr dx => 
+          ydf.2 (((2:R)*dr)•ydf.1) dx) :=
+by 
+  unfold revDerivProjUpdate
+  ftrans; simp[revDerivUpdate, add_assoc]
+
+
+@[ftrans]
+theorem SciLean.norm₂.arg_x.revDerivProj_rule_at
+  (f : X → Y) (x : X)
+  (hf : HasAdjDiffAt R f x) (hx : f x≠0)
+  : (revDerivProj R (fun x => ‖f x‖₂[R]) x)
+    =
+    let ydf := revCDeriv R f x
+    let ynorm := ‖ydf.1‖₂[R]
+    (ynorm,
+     fun _ dr => 
+       ydf.2 ((ynorm⁻¹ * dr)•ydf.1)):=
+by 
+  sorry_proof
+
+
+@[ftrans]
+theorem SciLean.norm₂.arg_x.revDerivProjUpdate_rule_at
+  (f : X → Y) (x : X)
+  (hf : HasAdjDiffAt R f x) (hx : f x≠0)
+  : (revDerivProjUpdate R (fun x => ‖f x‖₂[R]) x)
+    =
+    let ydf := revDerivUpdate R f x
+    let ynorm := ‖ydf.1‖₂[R]
+    (ynorm,
+     fun _ dr dx => 
+       ydf.2 ((ynorm⁻¹ * dr)•ydf.1) dx):=
+by 
+  unfold revDerivProjUpdate
+  ftrans; simp[revDerivUpdate, add_assoc]
+
+end InnerProductSpace
+
+
+
+#exit
+section Test
+
+variable {K : Type _} [RealScalar K]
+
+set_option trace.Meta.Tactic.simp.discharge true in
+#check 
+  (revDerivProj K fun x : K×K => x.1 + x.2)
+  rewrite_by ftrans only; simp[StructLike.modify,StructLike.make]
+
+
+set_option trace.Meta.Tactic.simp.discharge true in
+#check 
+  (revDerivProj K fun x : K×K => x.1*x.2 + x.2)
+  rewrite_by ftrans only; simp[StructLike.modify,StructLike.make]
+
+
+set_option trace.Meta.Tactic.simp.rewrite true in
+#check 
+  (revDerivProj K fun x : K×K => x.1*x.2)
+  rewrite_by
+    ftrans only 
+    simp only[StructLike.modify,StructLike.make,dite_eq_ite,eq_self,ite_true,dite_false]
+
+#exit
+
+set_option trace.Meta.Tactic.simp.rewrite true in
+#check 
+  (revDerivProj K fun x : K×K×K×K => x.1 + x.2.1 + x.2.2.1 + x.2.2.2)
+  rewrite_by 
+    ftrans only 
+    simp only[StructLike.modify,StructLike.make,dite_eq_ite,eq_self,ite_true,dite_false]
+
+
+set_option trace.Meta.Tactic.simp.discharge true in
+set_option trace.Meta.Tactic.fprop.discharge true in
+#check 
+  (revCDeriv K fun x : K×K×K×K => x.1^(2:ℕ) + x.2.1^2 + x.2.2.1^2 + x.2.2.2^2)
+  rewrite_by ftrans only; simp
+
+
+set_option trace.Meta.Tactic.simp.discharge true in
+set_option trace.Meta.Tactic.fprop.discharge true in
+#check 
+  (revCDeriv K fun x : K×K => x.2^2 + x.1^2)
+  rewrite_by ftrans only; simp
+
+
+
+
+
diff --git a/SciLean/Core/FunctionTransformations/RevDerivUpdate.lean b/SciLean/Core/FunctionTransformations/RevDerivUpdate.lean
index 7358cf72..44089e55 100644
--- a/SciLean/Core/FunctionTransformations/RevDerivUpdate.lean
+++ b/SciLean/Core/FunctionTransformations/RevDerivUpdate.lean
@@ -24,11 +24,23 @@ def revDerivUpdate
 --   : HasSemiAdjoint K (fun y => (revDerivUpdate K f x).2 y k 0) := by unfold revDerivUpdate; ftrans; fprop
 
 @[simp, ftrans_simp]
-theorem revDerivProj_fst (f : X → Y) (x : X)
+theorem revDerivUpdate_fst (f : X → Y) (x : X)
   : (revDerivUpdate K f x).1 = f x :=
 by
   rfl
 
+@[simp, ftrans_simp]
+theorem revDerivUpdate_snd_zero (f : X → Y) (x dx : X)
+  : (revDerivUpdate K f x).2 0 dx = dx := 
+by
+  simp[revDerivUpdate]
+
+@[simp, ftrans_simp]
+theorem revDerivUpdate_snd_zero' (f : X → Y) (x : X) (dy : Y)
+  : (revDerivUpdate K f x).2 dy 0 = (revCDeriv K f x).2 dy := 
+by
+  simp[revDerivUpdate]
+
 
 namespace revDerivUpdate
 
diff --git a/SciLean/Data/StructLike/Algebra.lean b/SciLean/Data/StructLike/Algebra.lean
index 0a8c1419..65ddddd1 100644
--- a/SciLean/Data/StructLike/Algebra.lean
+++ b/SciLean/Data/StructLike/Algebra.lean
@@ -30,6 +30,17 @@ class SemiInnerProductSpaceStruct (K X I XI) [StructLike X I XI] [IsROrC K] [Enu
   inner_proj : ∀ (x x' : X), ⟪x,x'⟫[K] = ∑ (i : I), ⟪proj x i, proj x' i⟫[K]
   testFun_proj : ∀ (x : X), TestFunction x ↔ (∀ i, TestFunction (proj x i))
 
+instance (priority:=low) {X} [Vec K X] : VecStruct K X Unit (fun _ => X) where
+  proj_add := by simp[StructLike.proj]
+  proj_smul := by simp[StructLike.proj]
+  proj_zero := by simp[StructLike.proj]
+  proj_continuous := sorry_proof
+  make_continuous := sorry_proof
+
+instance (priority:=low) {X} [SemiInnerProductSpace K X] : SemiInnerProductSpaceStruct K X Unit (fun _ => X) where
+  inner_proj := sorry_proof
+  testFun_proj := sorry_proof
+
 
 @[reducible]
 instance [∀ i, Vec K (EI i)] [∀ j, Vec K (FJ j)] (i : I ⊕ J) : Vec K (Prod.TypeFun EI FJ i) := 
@@ -37,7 +48,6 @@ instance [∀ i, Vec K (EI i)] [∀ j, Vec K (FJ j)] (i : I ⊕ J) : Vec K (Prod
   | .inl _ => by infer_instance
   | .inr _ => by infer_instance
 
-
 instance [Vec K E] [Vec K F] [∀ i, Vec K (EI i)] [∀ j, Vec K (FJ j)] 
   [VecStruct K E I EI] [VecStruct K F J FJ]
   : VecStruct K (E×F) (I⊕J) (Prod.TypeFun EI FJ) where
diff --git a/SciLean/Data/StructLike/Basic.lean b/SciLean/Data/StructLike/Basic.lean
index 3ea3e92c..707b2a29 100644
--- a/SciLean/Data/StructLike/Basic.lean
+++ b/SciLean/Data/StructLike/Basic.lean
@@ -38,7 +38,7 @@ by
 
 /-- Every type is `StructLike` with `Unit` as index set.
 -/
-instance (priority:=low) : StructLike α Unit (fun _ => α) where
+instance (priority:=low) instStructLikeDefault : StructLike α Unit (fun _ => α) where
   proj := fun x _ => x
   make := fun f => f ()
   modify := fun _ f x => f x