From 036691f93bfdca1254b3e3d8ef70af247ac383cd Mon Sep 17 00:00:00 2001
From: lecopivo <skrivantomas@seznam.cz>
Date: Wed, 19 Jul 2023 17:44:04 -0400
Subject: [PATCH] work on verified AD

---
 SciLean.lean                                  |   2 +
 SciLean/FTrans/FDeriv/Basic.lean              | 246 ++++++++++++------
 SciLean/FTrans/FDeriv/Test.lean               |  54 ++++
 .../ContinuousLinearMap/Basic.lean            | 229 +++++++++++++++-
 .../ContinuousLinearMap/Test.lean             |  48 ++++
 .../FunctionSpaces/Differentiable/Basic.lean  | 176 +++++++++++--
 .../FunctionSpaces/Differentiable/Test.lean   |  72 +++++
 SciLean/Functions/Interpolate.lean            |   1 +
 SciLean/Lean/Meta/Basic.lean                  |  21 ++
 SciLean/Tactic/FTrans/Basic.lean              |  94 ++-----
 SciLean/Tactic/FTrans/Init.lean               | 175 ++++++++++---
 11 files changed, 900 insertions(+), 218 deletions(-)
 create mode 100644 SciLean/FTrans/FDeriv/Test.lean
 create mode 100644 SciLean/FunctionSpaces/ContinuousLinearMap/Test.lean
 create mode 100644 SciLean/FunctionSpaces/Differentiable/Test.lean

diff --git a/SciLean.lean b/SciLean.lean
index 0bb82d34..987b079f 100644
--- a/SciLean.lean
+++ b/SciLean.lean
@@ -8,6 +8,8 @@ import SciLean.Data.DataArray
 import SciLean.Functions.OdeSolve
 import SciLean.Solver.Solver 
 
+import SciLean.FTrans.FDeriv.Basic
+
 /-!
 
 SciLean
diff --git a/SciLean/FTrans/FDeriv/Basic.lean b/SciLean/FTrans/FDeriv/Basic.lean
index de3eb5d7..e41ea16f 100644
--- a/SciLean/FTrans/FDeriv/Basic.lean
+++ b/SciLean/FTrans/FDeriv/Basic.lean
@@ -1,28 +1,31 @@
-import SciLean.Tactic.FTrans.Basic
 
 import Mathlib.Analysis.Calculus.FDeriv.Basic
 import Mathlib.Analysis.Calculus.FDeriv.Comp
 import Mathlib.Analysis.Calculus.FDeriv.Prod
 import Mathlib.Analysis.Calculus.FDeriv.Linear
+import Mathlib.Analysis.Calculus.FDeriv.Add
+import Mathlib.Analysis.Calculus.FDeriv.Mul
+
+import Mathlib.Analysis.Calculus.Deriv.Basic
+import Mathlib.Analysis.Calculus.Deriv.Inv 
 
 
-import SciLean.Tactic.LSimp.Elab
 import SciLean.FunctionSpaces.ContinuousLinearMap.Basic
 import SciLean.FunctionSpaces.Differentiable.Basic
+import SciLean.Tactic.FTrans.Basic
+
 
 namespace SciLean
 
 set_option linter.unusedVariables false
 
-variable {K : Type _} [NontriviallyNormedField K]
-
-variable {X : Type _} [NormedAddCommGroup X] [NormedSpace K X]
-variable {Y : Type _} [NormedAddCommGroup Y] [NormedSpace K Y]
-variable {Z : Type _} [NormedAddCommGroup Z] [NormedSpace K Z]
-
-variable {ι : Type _} [Fintype ι]
-
-variable {E : ι → Type _} [∀ i, NormedAddCommGroup (E i)] [∀ i, NormedSpace K (E i)]
+variable 
+  {K : Type _} [NontriviallyNormedField K]
+  {X : Type _} [NormedAddCommGroup X] [NormedSpace K X]
+  {Y : Type _} [NormedAddCommGroup Y] [NormedSpace K Y]
+  {Z : Type _} [NormedAddCommGroup Z] [NormedSpace K Z]
+  {ι : Type _} [Fintype ι]
+  {E : ι → Type _} [∀ i, NormedAddCommGroup (E i)] [∀ i, NormedSpace K (E i)]
 
 
 -- Basic lambda calculus rules -------------------------------------------------
@@ -47,8 +50,8 @@ theorem fderiv.let_rule_at
         let y := g x
         f x y) x
     =
+    let y  := g x
     fun dx =>L[K]
-      let y  := g x
       let dy := fderiv K g x dx
       let dz := fderiv K (fun xy : X×Y => f xy.1 xy.2) (x,y) (dx, dy)
       dz := 
@@ -68,11 +71,12 @@ theorem fderiv.let_rule
        let y := g x
        f x y)
     =
-    fun x => fun dx =>L[K]
+    fun x => 
       let y  := g x
-      let dy := fderiv K g x dx
-      let dz := fderiv K (fun xy : X×Y => f xy.1 xy.2) (x,y) (dx, dy)
-      dz := 
+      fun dx =>L[K]
+        let dy := fderiv K g x dx
+        let dz := fderiv K (fun xy : X×Y => f xy.1 xy.2) (x,y) (dx, dy)
+        dz := 
 by
   funext x
   apply fderiv.let_rule_at x _ (hg x) _ (hf (x,g x))
@@ -103,12 +107,12 @@ theorem fderiv.pi_rule
 
 open Lean Meta Qq
 
-
-def fderiv.discharger : Expr → SimpM (Option Expr) :=
+def fderiv.discharger : Expr → MetaM (Option Expr) :=
   FTrans.tacticToDischarge (Syntax.mkLit ``tacticDifferentiable "differentiable")
 
-open Lean Elab Term
-def fderiv.ftransInfo : FTrans.Info where
+open Lean Elab Term FTrans
+def fderiv.ftransExt : FTransExt where
+  ftransName := ``fderiv
   getFTransFun? e := 
     if e.isAppOf ``fderiv then
 
@@ -119,71 +123,46 @@ def fderiv.ftransInfo : FTrans.Info where
     else
       none
 
-  identityTheorem := ``fderiv.id_rule 
-  constantTheorem := ``fderiv.const_rule
-
   replaceFTransFun e f := 
     if e.isAppOf ``fderiv then
       e.modifyArg (fun _ => f) 8 
     else          
       e
 
-  applyLambdaLetRule e := do
-    match e.getArg? 8 with
-    | .some (.lam xName xType 
-              (.letE yName yType yVal body _) bi) => do
-
-      let ruleName := ``fderiv.let_rule
-
-      let thm : SimpTheorem := {
-        proof := mkConst ruleName
-        origin := .decl ruleName
-        rfl := false
-      }
-
-      if let some result ← Meta.Simp.tryTheorem? e thm fderiv.discharger then
-        return Simp.Step.visit result
-
-      return none
-    | _ => return none
-
-  applyLambdaLambdaRule e := do
-    match e.getArg? 8 with
-    | .some (.lam xName xType 
-              (.lam yName yType body _) _) => do
-
-      let ruleName := ``fderiv.pi_rule
-
-      let thm : SimpTheorem := {
-        proof := mkConst ruleName
-        origin := .decl ruleName
-        rfl := false
-      }
-
-      if let some result ← Meta.Simp.tryTheorem? e thm fderiv.discharger then
-        return Simp.Step.visit result
-
-      return none
-    | _ => return none
-
+  identityRule     := .some <| .thm ``fderiv.id_rule
+  constantRule     := .some <| .thm ``fderiv.const_rule
+  lambdaLetRule    := .some <| .thm ``fderiv.let_rule
+  lambdaLambdaRule := .some <| .thm ``fderiv.pi_rule
 
   discharger := fderiv.discharger
 
+
+-- register fderiv
 #eval show Lean.CoreM Unit from do
-  FTrans.FTransExt.insert ``fderiv fderiv.ftransInfo
+  modifyEnv (λ env => FTrans.ftransExt.addEntry env (``fderiv, fderiv.ftransExt))
 
 
+end SciLean
 
 --------------------------------------------------------------------------------
 -- Function Rules --------------------------------------------------------------
 --------------------------------------------------------------------------------
 
+variable 
+  {K : Type _} [NontriviallyNormedField K]
+  {X : Type _} [NormedAddCommGroup X] [NormedSpace K X]
+  {Y : Type _} [NormedAddCommGroup Y] [NormedSpace K Y]
+  {Z : Type _} [NormedAddCommGroup Z] [NormedSpace K Z]
+  {ι : Type _} [Fintype ι]
+  {E : ι → Type _} [∀ i, NormedAddCommGroup (E i)] [∀ i, NormedSpace K (E i)]
+
 
--- Prod.mk --------------------------------------------------------------------
+
+-- Prod.mk -----------------------------------v---------------------------------
 --------------------------------------------------------------------------------
 
 @[ftrans_rule]
-theorem _root_.Prod.mk.arg_fstsnd.fderiv_at_comp
+theorem Prod.mk.arg_fstsnd.fderiv_at_comp
   (x : X)
   (g : X → Y) (hg : DifferentiableAt K g x)
   (f : X → Z) (hf : DifferentiableAt K f x)
@@ -196,7 +175,7 @@ by
 
 
 @[ftrans_rule]
-theorem _root_.Prod.mk.arg_fstsnd.fderiv_comp
+theorem Prod.mk.arg_fstsnd.fderiv_comp
   (x : X)
   (g : X → Y) (hg : Differentiable K g)
   (f : X → Z) (hf : Differentiable K f)
@@ -213,7 +192,7 @@ by
 --------------------------------------------------------------------------------
 
 @[ftrans_rule]
-theorem _root_.Prod.fst.arg_self.fderiv_at_comp
+theorem Prod.fst.arg_self.fderiv_at_comp
   (x : X)
   (f : X → Y×Z) (hf : DifferentiableAt K f x)
   : fderiv K (fun x => (f x).1) x
@@ -223,7 +202,7 @@ theorem _root_.Prod.fst.arg_self.fderiv_at_comp
 
 
 @[ftrans_rule]
-theorem _root_.Prod.fst.arg_self.fderiv_comp
+theorem Prod.fst.arg_self.fderiv_comp
   (f : X → Y×Z) (hf : Differentiable K f)
   : fderiv K (fun x => (f x).1)
     =
@@ -232,7 +211,7 @@ theorem _root_.Prod.fst.arg_self.fderiv_comp
 
 
 @[ftrans_rule]
-theorem _root_.Prod.fst.arg_self.fderiv
+theorem Prod.fst.arg_self.fderiv
   : fderiv K (fun xy : X×Y => xy.1)
     =  
     fun _ => fun dxy =>L[K] dxy.1
@@ -244,7 +223,7 @@ theorem _root_.Prod.fst.arg_self.fderiv
 --------------------------------------------------------------------------------
 
 @[ftrans_rule]
-theorem _root_.Prod.snd.arg_self.fderiv_at_comp
+theorem Prod.snd.arg_self.fderiv_at_comp
   (x : X)
   (f : X → Y×Z) (hf : DifferentiableAt K f x)
   : fderiv K (fun x => (f x).2) x
@@ -254,15 +233,16 @@ theorem _root_.Prod.snd.arg_self.fderiv_at_comp
 
 
 @[ftrans_rule]
-theorem _root_.Prod.snd.arg_self.fderiv_comp
+theorem Prod.snd.arg_self.fderiv_comp
   (f : X → Y×Z) (hf : Differentiable K f)
   : fderiv K (fun x => (f x).2)
     =
     fun x => fun dx =>L[K] (fderiv K f x dx).2
 := sorry
 
+
 @[ftrans_rule]
-theorem _root_.Prod.snd.arg_self.fderiv
+theorem Prod.snd.arg_self.fderiv
   : fderiv K (fun xy : X×Y => xy.2)
     =  
     fun _ => fun dxy =>L[K] dxy.2
@@ -274,20 +254,136 @@ theorem _root_.Prod.snd.arg_self.fderiv
 --------------------------------------------------------------------------------
 
 @[ftrans_rule]
-theorem _root_.HAdd.hAdd.arg_a4a5.fderiv_at_comp
+theorem HAdd.hAdd.arg_a4a5.fderiv_at_comp
   (x : X) (f g : X → Y) (hf : DifferentiableAt K f x) (hg : DifferentiableAt K g x)
   : (fderiv K fun x => f x + g x) x
     =
     fun dx =>L[K]
       fderiv K f x dx + fderiv K g x dx
-  := sorry
+  := fderiv_add hf hg
 
 
 @[ftrans_rule]
-theorem _root_.HAdd.hAdd.arg_a4a5.fderiv_comp
+theorem HAdd.hAdd.arg_a4a5.fderiv_comp
   (f g : X → Y) (hf : Differentiable K f) (hg : Differentiable K g)
   : (fderiv K fun x => f x + g x)
     =
     fun x => fun dx =>L[K]
       fderiv K f x dx + fderiv K g x dx
-  := sorry
+  := by funext x; apply fderiv_add (hf x) (hg x)
+
+
+
+-- HSub.hSub -------------------------------------------------------------------
+--------------------------------------------------------------------------------
+
+@[ftrans_rule]
+theorem HSub.hSub.arg_a4a5.fderiv_at_comp
+  (x : X) (f g : X → Y) (hf : DifferentiableAt K f x) (hg : DifferentiableAt K g x)
+  : (fderiv K fun x => f x - g x) x
+    =
+    fun dx =>L[K]
+      fderiv K f x dx - fderiv K g x dx
+  := fderiv_sub hf hg
+
+
+@[ftrans_rule]
+theorem HSub.hSub.arg_a4a5.fderiv_comp
+  (f g : X → Y) (hf : Differentiable K f) (hg : Differentiable K g)
+  : (fderiv K fun x => f x - g x)
+    =
+    fun x => fun dx =>L[K]
+      fderiv K f x dx - fderiv K g x dx
+  := by funext x; apply fderiv_sub (hf x) (hg x)
+
+
+
+-- Neg.neg ---------------------------------------------------------------------
+--------------------------------------------------------------------------------
+
+@[ftrans_rule]
+theorem Neg.neg.arg_a2.fderiv_at_comp
+  (x : X) (f : X → Y)
+  : (fderiv K fun x => - f x) x
+    =
+    fun dx =>L[K]
+      - fderiv K f x dx
+  := fderiv_neg
+
+
+@[ftrans_rule]
+theorem Neg.neg.arg_a2.fderiv_comp
+  (f : X → Y)
+  : (fderiv K fun x => - f x)
+    =
+    fun x => fun dx =>L[K]
+      - fderiv K f x dx
+  := by funext x; apply fderiv_neg
+
+
+
+-- SMul.smul -------------------------------------------------------------------
+--------------------------------------------------------------------------------
+
+@[ftrans_rule]
+theorem SMul.smul.arg_a3a4.fderiv_at_comp
+  (x : X) (f : X → K) (g : X → Y) 
+  (hf : DifferentiableAt K f x) (hg : DifferentiableAt K g x)
+  : (fderiv K fun x => f x • g x) x
+    =
+    let k := f x
+    let y := g x
+    fun dx =>L[K]
+      k • (fderiv K g x dx) + (fderiv K f x dx) • y  
+  := fderiv_smul hf hg
+
+
+@[ftrans_rule]
+theorem SMul.smul.arg_a3a4.fderiv_comp
+  (f : X → K) (g : X → Y) 
+  (hf : Differentiable K f) (hg : Differentiable K g)
+  : (fderiv K fun x => f x • g x)
+    =
+    fun x => 
+      let k := f x
+      let y := g x
+      fun dx =>L[K]
+        k • (fderiv K g x dx) + (fderiv K f x dx) • y  
+  := by funext x; apply fderiv_smul (hf x) (hg x)
+
+
+
+-- HDiv.hDiv -------------------------------------------------------------------
+--------------------------------------------------------------------------------
+
+@[ftrans_rule]
+theorem HDiv.hDiv.arg_a4a5.fderiv_at_comp
+  {R : Type _} [NontriviallyNormedField R] [NormedAlgebra R K]
+  (x : R) (f : R → K) (g : R → K) 
+  (hf : DifferentiableAt R f x) (hg : DifferentiableAt R g x) (hx : g x ≠ 0)
+  : (fderiv R fun x => f x / g x) x
+    =
+    let k := f x
+    let k' := g x
+    fun dx =>L[R]
+      ((fderiv R f x dx) * k' - k * (fderiv R g x dx)) / k'^2 := 
+by
+  have h : ∀ (f : R → K) x, fderiv R f x 1 = deriv f x := by simp[deriv]
+  ext; simp[h]; apply deriv_div hf hg hx
+
+
+@[ftrans_rule]
+theorem HDiv.hDiv.arg_a4a5.fderiv_comp
+  {R : Type _} [NontriviallyNormedField R] [NormedAlgebra R K]
+  (f : R → K) (g : R → K) 
+  (hf : Differentiable R f) (hg : Differentiable R g) (hx : ∀ x, g x ≠ 0)
+  : (fderiv R fun x => f x / g x)
+    =
+    fun x => 
+      let k := f x
+      let k' := g x
+      fun dx =>L[R]
+        ((fderiv R f x dx) * k' - k * (fderiv R g x dx)) / k'^2 := 
+by
+  have h : ∀ (f : R → K) x, fderiv R f x 1 = deriv f x := by simp[deriv]
+  ext x; simp[h]; apply deriv_div (hf x) (hg x) (hx x)
diff --git a/SciLean/FTrans/FDeriv/Test.lean b/SciLean/FTrans/FDeriv/Test.lean
new file mode 100644
index 00000000..c735ad24
--- /dev/null
+++ b/SciLean/FTrans/FDeriv/Test.lean
@@ -0,0 +1,54 @@
+import SciLean.FTrans.FDeriv.Basic
+import SciLean.Profile
+
+open SciLean
+
+
+variable {K : Type _} [NontriviallyNormedField K]
+
+variable {X : Type _} [NormedAddCommGroup X] [NormedSpace K X]
+variable {Y : Type _} [NormedAddCommGroup Y] [NormedSpace K Y]
+variable {Z : Type _} [NormedAddCommGroup Z] [NormedSpace K Z]
+
+variable {ι : Type _} [Fintype ι]
+
+variable {E : ι → Type _} [∀ i, NormedAddCommGroup (E i)] [∀ i, NormedSpace K (E i)]
+
+#profile_this_file
+
+example 
+  : fderiv K (fun (x : K) => x + x)
+    =
+    0 := 
+by 
+  ext x; simp
+  ftrans only
+  sorry
+
+example 
+  : fderiv K (fun (x : K) => x + x + x)
+    =
+    0 := 
+by 
+  ext x; simp
+  ftrans only
+  sorry
+
+example 
+  : fderiv K (fun (x : K) => x + x + x + x)
+    =
+    0 := 
+by 
+  ext x; simp
+  ftrans only
+  sorry
+
+example 
+  : fderiv K (fun (x : K) => x + x + x + x + x)
+    =
+    0 := 
+by 
+  ext x; simp
+  ftrans only
+  sorry
+
diff --git a/SciLean/FunctionSpaces/ContinuousLinearMap/Basic.lean b/SciLean/FunctionSpaces/ContinuousLinearMap/Basic.lean
index 16c944d3..fe9c3ba1 100644
--- a/SciLean/FunctionSpaces/ContinuousLinearMap/Basic.lean
+++ b/SciLean/FunctionSpaces/ContinuousLinearMap/Basic.lean
@@ -1,4 +1,5 @@
 import Mathlib.Topology.Algebra.Module.Basic
+import Mathlib.Analysis.NormedSpace.Basic
 
 import SciLean.FunctionSpaces.ContinuousLinearMap.Init
 
@@ -26,7 +27,17 @@ macro "is_continuous_linear_map" : attr =>
 
 -- tactic
 macro "is_continuous_linear_map" : tactic =>
-  `(tactic| aesop (options := { terminal := true }) (rule_sets [$(Lean.mkIdent `IsContinuousLinearMap):ident]))
+  `(tactic| aesop (options := { terminal := true }) (simp_options := { enabled := false }) (rule_sets [$(Lean.mkIdent `IsContinuousLinearMap):ident, -default]))
+
+-- add `dsimp` as a normalization step
+open Lean.Meta Lean.Elab.Tactic in
+@[aesop norm (rule_sets [IsContinuousLinearMap])]
+def isContinuousLinearMapNormalizationTactic : TacticM Unit := do
+  let goal ← inferType (Lean.Expr.mvar (← getMainGoal))
+  evalTactic $ ← `(tactic| dsimp)
+  let goal' ← inferType (Lean.Expr.mvar (← getMainGoal))
+  if goal == goal' then
+    throwError "dsimp failed to progress"
 
 
 
@@ -120,10 +131,10 @@ theorem comp_rule
 
 
 @[aesop unsafe apply (rule_sets [IsContinuousLinearMap])]
-theorem scomb_rule 
+theorem let_rule 
   (g : X → Y) (hg : IsContinuousLinearMap R g)
   (f : X → Y → Z) (hf : IsContinuousLinearMap R (fun (xy : X×Y) => f xy.1 xy.2))
-  : IsContinuousLinearMap R fun x => f x (g x) 
+  : IsContinuousLinearMap R fun x => let y := g x; f x y
 := 
   by_morphism ((fun (xy : X×Y) =>L[R] f xy.1 xy.2).comp ((ContinuousLinearMap.id R X).prod (fun x =>L[R] g x))) 
   (by simp[ContinuousLinearMap.comp])
@@ -144,11 +155,27 @@ theorem morph_rule (f : X →L[R] Y) : IsContinuousLinearMap R fun x => f x :=
 
 
 
+end SciLean.IsContinuousLinearMap
+
+
+--------------------------------------------------------------------------------
+
+open SciLean IsContinuousLinearMap
+
+variable 
+  {R : Type _} [Semiring R]
+  {X : Type _} [TopologicalSpace X] [AddCommMonoid X] [Module R X]
+  {Y : Type _} [TopologicalSpace Y] [AddCommMonoid Y] [Module R Y]
+  {Z : Type _} [TopologicalSpace Z] [AddCommMonoid Z] [Module R Z]
+  {ι : Type _} [Fintype ι]
+  {E : ι → Type _} [∀ i, TopologicalSpace (E i)] [∀ i, AddCommMonoid (E i)] [∀ i, Module R (E i)]
+
+
 -- Id --------------------------------------------------------------------------
 --------------------------------------------------------------------------------
 
 @[is_continuous_linear_map]
-theorem _root_.id.arg_a.IsContinuousLinearMap
+theorem id.arg_a.IsContinuousLinearMap
   : IsContinuousLinearMap R (id : X → X)
 := 
   by_morphism (ContinuousLinearMap.id R X) (by simp)
@@ -159,7 +186,7 @@ theorem _root_.id.arg_a.IsContinuousLinearMap
 --------------------------------------------------------------------------------
 
 @[is_continuous_linear_map]
-theorem _root_.Prod.mk.arg_fstsnd.IsContinuousLinearMap_comp
+theorem Prod.mk.arg_fstsnd.IsContinuousLinearMap_comp
   (g : X → Y) (hg : IsContinuousLinearMap R g)
   (f : X → Z) (hf : IsContinuousLinearMap R f)
   : IsContinuousLinearMap R fun x => (g x, f x)
@@ -168,11 +195,12 @@ theorem _root_.Prod.mk.arg_fstsnd.IsContinuousLinearMap_comp
   (by simp)
 
 
+
 -- Prod.fst --------------------------------------------------------------------
 --------------------------------------------------------------------------------
 
 @[is_continuous_linear_map]
-theorem _root_.Prod.fst.arg_self.IsContinuousLinearMap
+theorem Prod.fst.arg_self.IsContinuousLinearMap
   : IsContinuousLinearMap R (@Prod.fst X Y)
 :=
   by_morphism (ContinuousLinearMap.fst R X Y) 
@@ -180,7 +208,7 @@ theorem _root_.Prod.fst.arg_self.IsContinuousLinearMap
 
 
 @[is_continuous_linear_map]
-theorem _root_.Prod.fst.arg_self.IsContinuousLinearMap_comp
+theorem Prod.fst.arg_self.IsContinuousLinearMap_comp
   (f : X → Y×Z) (hf : SciLean.IsContinuousLinearMap R f)
   : SciLean.IsContinuousLinearMap R fun (x : X) => (f x).fst
 := 
@@ -193,7 +221,7 @@ theorem _root_.Prod.fst.arg_self.IsContinuousLinearMap_comp
 --------------------------------------------------------------------------------
 
 @[is_continuous_linear_map]
-theorem _root_.Prod.snd.arg_self.IsContinuousLinearMap
+theorem Prod.snd.arg_self.IsContinuousLinearMap
   : IsContinuousLinearMap R fun (xy : X×Y) => xy.snd
 :=
   by_morphism (ContinuousLinearMap.snd R X Y) 
@@ -201,7 +229,7 @@ theorem _root_.Prod.snd.arg_self.IsContinuousLinearMap
 
 
 @[is_continuous_linear_map]
-theorem _root_.Prod.snd.arg_self.IsContinuousLinearMap_comp
+theorem Prod.snd.arg_self.IsContinuousLinearMap_comp
   (f : X → Y×Z) (hf : SciLean.IsContinuousLinearMap R f)
   : SciLean.IsContinuousLinearMap R fun (x : X) => (f x).snd
 := 
@@ -210,12 +238,191 @@ theorem _root_.Prod.snd.arg_self.IsContinuousLinearMap_comp
 
 
 
+-- Neg.neg ---------------------------------------------------------------------
+-------------------------------------------------------------------------------- 
+
+@[is_continuous_linear_map]
+theorem Neg.neg.arg_a2.IsContinuousLinearMap_comp 
+  {R : Type _} [Ring R]
+  {X : Type _} [TopologicalSpace X] [AddCommGroup X] [Module R X]
+  {Y : Type _} [TopologicalSpace Y] [AddCommGroup Y] [Module R Y] [TopologicalAddGroup Y]
+  (f : X → Y) (hf : IsContinuousLinearMap R f)
+  : IsContinuousLinearMap R fun x => - f x
+:= 
+  by_morphism (ContinuousLinearMap.neg.neg (fun x =>L[R] f x))
+  (by simp[ContinuousLinearMap.neg])
+
+
+
 -- HAdd.hAdd -------------------------------------------------------------------
 -------------------------------------------------------------------------------- 
 
 @[is_continuous_linear_map]
-theorem _root_.HAdd.hAdd.arg_a4a5.IsContinuousLinearMap_comp
+theorem HAdd.hAdd.arg_a4a5.IsContinuousLinearMap_comp [ContinuousAdd Y]
   (f g : X → Y) (hf : IsContinuousLinearMap R f) (hg : IsContinuousLinearMap R g)
   : IsContinuousLinearMap R fun x => f x + g x
 := 
-  sorry
+  by_morphism (ContinuousLinearMap.add.add (fun x =>L[R] f x) (fun x =>L[R] g x))
+  (by simp[ContinuousLinearMap.add])
+
+
+
+-- HSub.hSub -------------------------------------------------------------------
+-------------------------------------------------------------------------------- 
+
+@[is_continuous_linear_map]
+theorem HSub.hSub.arg_a4a5.IsContinuousLinearMap_comp 
+  {R : Type _} [Ring R]
+  {X : Type _} [TopologicalSpace X] [AddCommGroup X] [Module R X]
+  {Y : Type _} [TopologicalSpace Y] [AddCommGroup Y] [Module R Y] [TopologicalAddGroup Y]
+  (f g : X → Y) (hf : IsContinuousLinearMap R f) (hg : IsContinuousLinearMap R g)
+  : IsContinuousLinearMap R fun x => f x - g x
+:= 
+  by_morphism (ContinuousLinearMap.sub.sub (fun x =>L[R] f x) (fun x =>L[R] g x))
+  (by simp[ContinuousLinearMap.sub])
+
+
+
+-- HMul.hMul ---------------------------------------------------------------------
+-------------------------------------------------------------------------------- 
+
+def ContinuousLinearMap.mul_left 
+  {R : Type _} [CommSemiring R] 
+  {X : Type _} [TopologicalSpace X] [Semiring X] [Algebra R X] [TopologicalSemiring X] 
+  (x' : X) 
+  : X →L[R] X := 
+  ⟨⟨⟨fun x => x' * x, 
+    by apply mul_add⟩, 
+    by simp⟩, 
+    by continuity⟩
+
+
+def ContinuousLinearMap.mul_right 
+  {R : Type _} [CommSemiring R] 
+  {X : Type _} [TopologicalSpace X] [Semiring X] [Algebra R X] [TopologicalSemiring X] 
+  (x' : X) 
+  : X →L[R] X := 
+  ⟨⟨⟨fun x => x * x', 
+    fun a b => add_mul a b x'⟩, 
+    by simp⟩, 
+    by continuity⟩
+
+
+@[is_continuous_linear_map]
+theorem HMul.hMul.arg_a4.IsContinuousLinearMap_comp
+  {R : Type _} [CommSemiring R] 
+  {X : Type _} [TopologicalSpace X] [AddCommMonoid X] [Module R X]
+  {Y : Type _} [TopologicalSpace Y] [Semiring Y] [Algebra R Y] [TopologicalSemiring Y] 
+  (f : X → Y) (hf : IsContinuousLinearMap R f)
+  (y' : Y) 
+  : IsContinuousLinearMap R fun x => f x * y'
+:= 
+  by_morphism (ContinuousLinearMap.comp (ContinuousLinearMap.mul_right y') (fun x =>L[R] f x))
+  (by simp[ContinuousLinearMap.mul_right])
+
+
+@[is_continuous_linear_map]
+theorem HMul.hMul.arg_a5.IsContinuousLinearMap_comp
+  {R : Type _} [CommSemiring R] 
+  {X : Type _} [TopologicalSpace X] [AddCommMonoid X] [Module R X]
+  {Y : Type _} [TopologicalSpace Y] [Semiring Y] [Algebra R Y] [TopologicalSemiring Y] 
+  (f : X → Y) (hf : IsContinuousLinearMap R f)
+  (y' : Y) 
+  : IsContinuousLinearMap R fun x => y' * f x
+:= 
+  by_morphism (ContinuousLinearMap.comp (ContinuousLinearMap.mul_left y') (fun x =>L[R] f x))
+  (by simp[ContinuousLinearMap.mul_left])
+
+
+
+-- Smul.smul ---------------------------------------------------------------------
+-------------------------------------------------------------------------------- 
+
+/-- Creates `fun x =>L[R] r • g x` -/
+def ContinuousLinearMap.smulLeft 
+  {R : Type _} [CommSemiring R]
+  {X : Type _} [TopologicalSpace X] [AddCommMonoid X] [Module R X]
+  {Y : Type _} [TopologicalSpace Y] [AddCommMonoid Y] [Module R Y] [ContinuousConstSMul R Y]
+  (g : X →L[R] Y)
+  (r : R) 
+  : X →L[R] Y := 
+  let f : Y →L[R] Y := 
+    ⟨⟨⟨fun x => r • x, 
+      DistribMulAction.smul_add r⟩, 
+      smul_comm r⟩, 
+      ContinuousConstSMul.continuous_const_smul r⟩
+  f.comp g
+
+
+@[simp]
+def ContinuousLinearMap.smul_left 
+  {R : Type _} [CommSemiring R]
+  {X : Type _} [TopologicalSpace X] [AddCommMonoid X] [Module R X]
+  {Y : Type _} [TopologicalSpace Y] [AddCommMonoid Y] [Module R Y] [ContinuousConstSMul R Y]
+  (g : X →L[R] Y)
+  (r : R) (x : X)
+  : smulLeft g r x = r • g x := by rfl
+
+
+@[is_continuous_linear_map]
+theorem Smul.smul.arg_a3.IsContinuousLinearMap_comp 
+  [TopologicalSpace R] [ContinuousSMul R Y]
+  (f : X → R) (hf : IsContinuousLinearMap R f)
+  (y : Y) 
+  : IsContinuousLinearMap R fun x => f x • y
+:= 
+  by_morphism (ContinuousLinearMap.smulRight (fun x =>L[R] f x) y)
+  (by simp)
+
+
+@[is_continuous_linear_map]
+theorem Smul.smul.arg_a4.IsContinuousLinearMap_comp 
+  {R : Type _} [CommSemiring R]
+  {X : Type _} [TopologicalSpace X] [AddCommMonoid X] [Module R X]
+  {Y : Type _} [TopologicalSpace Y] [AddCommMonoid Y] [Module R Y] [ContinuousConstSMul R Y]
+  (c : R)
+  (f : X → Y) (hf : IsContinuousLinearMap R f)
+  : IsContinuousLinearMap R fun x => c • f x
+:= 
+  by_morphism (ContinuousLinearMap.smulLeft (fun x =>L[R] f x) c)
+  (by simp)
+
+
+
+-- HDiv.hDiv -------------------------------------------------------------------
+-------------------------------------------------------------------------------- 
+
+/-- Creates `fun x =>L[R] g x / y` -/
+def ContinuousLinearMap.divRight
+  {R : Type _} [NontriviallyNormedField R]
+  {K : Type _} [NontriviallyNormedField K] [NormedAlgebra R K]
+  {X : Type _} [TopologicalSpace X] [AddCommMonoid X] [Module R X]
+  (g : X →L[R] K) (y : K) 
+  : X →L[R] K := 
+  let f : K →L[R] K := 
+    ⟨⟨⟨fun x => x / y, 
+      by apply fun a b => add_div a b y⟩, 
+      by intro r x; simp; (repeat rw[div_eq_inv_mul]); apply mul_smul_comm⟩, 
+      by continuity⟩
+  f.comp g
+
+
+@[simp]
+def ContinuousLinearMap.div_right
+  {R : Type _} [NontriviallyNormedField R]
+  {K : Type _} [NontriviallyNormedField K] [NormedAlgebra R K]
+  {X : Type _} [TopologicalSpace X] [AddCommMonoid X] [Module R X]
+  (g : X →L[R] K) (y : K) (x : X)
+  : divRight g y x = g x / y := by rfl
+
+
+@[is_continuous_linear_map]
+theorem HDiv.hDul.arg_a4.IsContinuousLinearMap_comp
+  {R : Type _} [NontriviallyNormedField R]
+  {K : Type _} [NontriviallyNormedField K] [NormedAlgebra R K]
+  {X : Type _} [TopologicalSpace X] [AddCommMonoid X] [Module R X]
+  (f : X → K) (hf : IsContinuousLinearMap R f) (y : K) 
+  : IsContinuousLinearMap R fun x => f x / y
+:= 
+  by_morphism (ContinuousLinearMap.divRight (fun x =>L[R] f x) y)
+  (by simp)
diff --git a/SciLean/FunctionSpaces/ContinuousLinearMap/Test.lean b/SciLean/FunctionSpaces/ContinuousLinearMap/Test.lean
new file mode 100644
index 00000000..fee12633
--- /dev/null
+++ b/SciLean/FunctionSpaces/ContinuousLinearMap/Test.lean
@@ -0,0 +1,48 @@
+import SciLean.FunctionSpaces.ContinuousLinearMap.Basic
+
+open SciLean
+
+
+variable 
+  {R : Type _} [Semiring R]
+  {X : Type _} [TopologicalSpace X] [AddCommMonoid X] [Module R X]
+  {Y : Type _} [TopologicalSpace Y] [AddCommMonoid Y] [Module R Y]
+  {Z : Type _} [TopologicalSpace Z] [AddCommMonoid Z] [Module R Z]
+  {ι : Type _} [Fintype ι]
+  {E : ι → Type _} [∀ i, TopologicalSpace (E i)] [∀ i, AddCommMonoid (E i)] [∀ i, Module R (E i)]
+
+
+example 
+  (g : X → Y) (hg : IsContinuousLinearMap R g)
+  (f : Y → Z) (hf : IsContinuousLinearMap R f)
+  : IsContinuousLinearMap R fun x => f (g x) := by is_continuous_linear_map
+
+example 
+  (g : X → Y) (hg : IsContinuousLinearMap R g)
+  (f : X → Z) (hf : IsContinuousLinearMap R f)
+  : IsContinuousLinearMap R fun x => (f x, g x) := by is_continuous_linear_map
+
+example 
+  (g : X → Y) (hg : IsContinuousLinearMap R g)
+  (f : X → Y → Z) (hf : IsContinuousLinearMap R (fun xy : X×Y => f xy.1 xy.2))
+  : IsContinuousLinearMap R fun x => f x (g x) := by is_continuous_linear_map
+
+example 
+  (g : X → Y) (hg : IsContinuousLinearMap R g)
+  (f : X → Y → Z) (hf : IsContinuousLinearMap R (fun xy : X×Y => f xy.1 xy.2))
+  : IsContinuousLinearMap R fun x => let y := g x; let y' := g x; let y'' := g x; let y'' := g x; let y'' := g x; f x y := by is_continuous_linear_map
+
+
+example 
+  (F : (X→X) → (X →L[R] X))
+  (g : X → X)
+  : IsContinuousLinearMap R fun x => F g (F g x) := by is_continuous_linear_map
+
+
+example 
+  (F : (X→X) → (X →L[R] X))
+  (g : X → X)
+  : IsContinuousLinearMap R fun x => 
+      let y := F g x 
+      let z := F g y
+      z := by is_continuous_linear_map
diff --git a/SciLean/FunctionSpaces/Differentiable/Basic.lean b/SciLean/FunctionSpaces/Differentiable/Basic.lean
index def75032..0d7978e4 100644
--- a/SciLean/FunctionSpaces/Differentiable/Basic.lean
+++ b/SciLean/FunctionSpaces/Differentiable/Basic.lean
@@ -3,6 +3,8 @@ import Mathlib.Analysis.Calculus.FDeriv.Comp
 import Mathlib.Analysis.Calculus.FDeriv.Prod
 import Mathlib.Analysis.Calculus.FDeriv.Linear
 import Mathlib.Analysis.Calculus.FDeriv.Add
+import Mathlib.Analysis.Calculus.FDeriv.Mul
+import Mathlib.Analysis.Calculus.Deriv.Inv
 
 
 import SciLean.FunctionSpaces.Differentiable.Init
@@ -10,7 +12,8 @@ import SciLean.FunctionSpaces.Differentiable.Init
 namespace SciLean
 
 
-variable (R : Type _) [NontriviallyNormedField R]
+variable 
+  (R : Type _) [NontriviallyNormedField R]
   {X : Type _} [NormedAddCommGroup X] [NormedSpace R X]
   {Y : Type _} [NormedAddCommGroup Y] [NormedSpace R Y]
   {Z : Type _} [NormedAddCommGroup Z] [NormedSpace R Z]
@@ -32,7 +35,18 @@ macro "differentiable" : attr =>
 
 -- tactic
 macro "differentiable" : tactic =>
-  `(tactic| aesop (options := { terminal := true }) (rule_sets [$(Lean.mkIdent `Differentiable):ident]))
+  `(tactic| aesop (options := { terminal := true }) (simp_options := { enabled := false }) (rule_sets [$(Lean.mkIdent `Differentiable):ident, -default]))
+
+-- add `dsimp` as a normalization step
+open Lean.Meta Lean.Elab.Tactic in
+@[aesop norm (rule_sets [Differentiable])]
+def differentiableNormalizationTactic : TacticM Unit := do
+  let goal ← inferType (Lean.Expr.mvar (← getMainGoal))
+  evalTactic $ ← `(tactic| dsimp)
+  let goal' ← inferType (Lean.Expr.mvar (← getMainGoal))
+  if goal == goal' then
+    throwError "dsimp failed to progress"
+
 
 
 -- Basic rules -----------------------------------------------------------------
@@ -52,25 +66,25 @@ variable
 @[differentiable]
 theorem id_rule_at (x : X)
   : DifferentiableAt R (fun x : X => x) x
-:= by simp
+  := by simp
 
 
 @[differentiable]
 theorem id_rule
   : Differentiable R (fun x : X => x)
-:= by simp
+  := by simp
   
 
 @[differentiable]
 theorem const_rule_at (x : X) (y : Y)
   : DifferentiableAt R (fun _ : Y => x) y
-:= by simp
+  := by simp
 
 
 @[differentiable]
 theorem const_rule (x : X)
   : Differentiable R (fun _ : Y => x)
-:= by simp
+  := by simp
 
 
 @[aesop unsafe apply (rule_sets [Differentiable])]
@@ -79,7 +93,7 @@ theorem comp_rule_at
   (g : X → Y) (hg : DifferentiableAt R g x)
   (f : Y → Z) (hf : DifferentiableAt R f (g x))
   : DifferentiableAt R (fun x => f (g x)) x
-:= DifferentiableAt.comp x hf hg
+  := DifferentiableAt.comp x hf hg
 
 
 @[aesop safe apply (rule_sets [Differentiable])]
@@ -87,7 +101,7 @@ theorem comp_rule
   (g : X → Y) (hg : Differentiable R g)
   (f : Y → Z) (hf : Differentiable R f)
   : Differentiable R (fun x => f (g x))
-:= Differentiable.comp hf hg
+  := Differentiable.comp hf hg
 
 
 @[aesop unsafe apply (rule_sets [Differentiable])]
@@ -112,8 +126,8 @@ by
 theorem let_rule
   (g : X → Y) (hg : Differentiable R g)
   (f : X → Y → Z) (hf : Differentiable R (fun (xy : X×Y) => f xy.1 xy.2))
-  : Differentiable R (fun x => let y := g x; f x y) := 
-by apply fun x => let_rule_at x g (hg x) f (hf (x, g x))
+  : Differentiable R (fun x => let y := g x; f x y) 
+  := by apply fun x => let_rule_at x g (hg x) f (hf (x, g x))
 
 
 @[differentiable]
@@ -121,7 +135,7 @@ theorem pi_rule_at
   (x : X)
   (f : (i : ι) → X → E i) (hf : ∀ i, DifferentiableAt R (f i) x)
   : DifferentiableAt R (fun x i => f i x) x
-  := by sorry
+  := by apply differentiableAt_pi.2 hf
 
 
 @[differentiable]
@@ -131,16 +145,34 @@ theorem pi_rule
   := fun x => pi_rule_at x f (fun i => hf i x)
 
 
+end SciLean.Differentiable
+
+
+--------------------------------------------------------------------------------
+-- Function Rules --------------------------------------------------------------
+--------------------------------------------------------------------------------
+
+open SciLean Differentiable 
+
+variable 
+  {R : Type _} [NontriviallyNormedField R]
+  {X : Type _} [NormedAddCommGroup X] [NormedSpace R X]
+  {Y : Type _} [NormedAddCommGroup Y] [NormedSpace R Y]
+  {Z : Type _} [NormedAddCommGroup Z] [NormedSpace R Z]
+  {ι : Type _} [Fintype ι]
+  {E : ι → Type _} [∀ i, NormedAddCommGroup (E i)] [∀ i, NormedSpace R (E i)]
+
+
 -- Id --------------------------------------------------------------------------
 --------------------------------------------------------------------------------
 
 @[differentiable]
-theorem _root_.id.arg_a.DifferentiableAt (x : X)
+theorem id.arg_a.DifferentiableAt (x : X)
   : DifferentiableAt R (id : X → X) x := by simp
 
 
 @[differentiable]
-theorem _root_.id.arg_a.Differentiable
+theorem id.arg_a.Differentiable
   : Differentiable R (id : X → X) := by simp
 
 
@@ -151,7 +183,7 @@ theorem _root_.id.arg_a.Differentiable
 --------------------------------------------------------------------------------
 
 @[differentiable]
-theorem _root_.Prod.mk.arg_fstsnd.DifferentiableAt_comp
+theorem Prod.mk.arg_fstsnd.DifferentiableAt_comp
   (x : X)
   (g : X → Y) (hg : DifferentiableAt R g x)
   (f : X → Z) (hf : DifferentiableAt R f x)
@@ -160,7 +192,7 @@ theorem _root_.Prod.mk.arg_fstsnd.DifferentiableAt_comp
 
 
 @[differentiable]
-theorem _root_.Prod.mk.arg_fstsnd.Differentiable_comp
+theorem Prod.mk.arg_fstsnd.Differentiable_comp
   (g : X → Y) (hg : Differentiable R g)
   (f : X → Z) (hf : Differentiable R f)
   : Differentiable R fun x => (g x, f x)
@@ -172,7 +204,7 @@ theorem _root_.Prod.mk.arg_fstsnd.Differentiable_comp
 --------------------------------------------------------------------------------
 
 @[differentiable]
-theorem _root_.Prod.fst.arg_self.DifferentiableAt_comp 
+theorem Prod.fst.arg_self.DifferentiableAt_comp 
   (x : X)
   (f : X → Y×Z) (hf : DifferentiableAt R f x)
   : DifferentiableAt R (fun x => (f x).1) x
@@ -180,7 +212,7 @@ theorem _root_.Prod.fst.arg_self.DifferentiableAt_comp
 
 
 @[differentiable]
-theorem _root_.Prod.fst.arg_self.Differentiable_comp 
+theorem Prod.fst.arg_self.Differentiable_comp 
   (f : X → Y×Z) (hf : Differentiable R f)
   : Differentiable R (fun x => (f x).1)
   := Differentiable.fst hf
@@ -191,7 +223,7 @@ theorem _root_.Prod.fst.arg_self.Differentiable_comp
 --------------------------------------------------------------------------------
 
 @[differentiable]
-theorem _root_.Prod.snd.arg_self.DifferentiableAt_comp 
+theorem Prod.snd.arg_self.DifferentiableAt_comp 
   (x : X)
   (f : X → Y×Z) (hf : DifferentiableAt R f x)
   : DifferentiableAt R (fun x => (f x).2) x
@@ -199,25 +231,125 @@ theorem _root_.Prod.snd.arg_self.DifferentiableAt_comp
 
 
 @[differentiable]
-theorem _root_.Prod.snd.arg_self.Differentiable_comp 
+theorem Prod.snd.arg_self.Differentiable_comp 
   (f : X → Y×Z) (hf : Differentiable R f)
   : Differentiable R (fun x => (f x).2)
   := Differentiable.snd hf
 
 
 
+-- Neg.neg ---------------------------------------------------------------------
+--------------------------------------------------------------------------------
+
+@[differentiable]
+theorem Neg.neg.arg_a2.DifferentiableAt_comp
+  (x : X) (f : X → Y) (hf : DifferentiableAt R f x)
+  : DifferentiableAt R (fun x => - f x) x
+  := DifferentiableAt.neg hf
+ 
+
+@[differentiable]
+theorem Neg.neg.arg_a2.Differentiable_comp
+  (f : X → Y) (hf : Differentiable R f) 
+  : Differentiable R fun x => - f x 
+  := fun x => Neg.neg.arg_a2.DifferentiableAt_comp x f (hf x)
+
+
+
 -- HAdd.hAdd -------------------------------------------------------------------
 --------------------------------------------------------------------------------
 
 @[differentiable]
-theorem _root_.HAdd.hAdd.arg_a4a5.DifferentiableAt_comp
+theorem HAdd.hAdd.arg_a4a5.DifferentiableAt_comp
   (x : X) (f g : X → Y) (hf : DifferentiableAt R f x) (hg : DifferentiableAt R g x)
   : DifferentiableAt R (fun x => f x + g x) x
   := DifferentiableAt.add hf hg
  
 
 @[differentiable]
-theorem _root_.HAdd.hAdd.arg_a4a5.Differentiable_comp
+theorem HAdd.hAdd.arg_a4a5.Differentiable_comp
   (f g : X → Y) (hf : Differentiable R f) (hg : Differentiable R g)
   : Differentiable R fun x => f x + g x
-  := fun x => _root_.HAdd.hAdd.arg_a4a5.DifferentiableAt_comp x f g (hf x) (hg x)
+  := fun x => HAdd.hAdd.arg_a4a5.DifferentiableAt_comp x f g (hf x) (hg x)
+
+
+
+-- HSub.hSub -------------------------------------------------------------------
+--------------------------------------------------------------------------------
+
+@[differentiable]
+theorem HSub.hSub.arg_a4a5.DifferentiableAt_comp
+  (x : X) (f g : X → Y) (hf : DifferentiableAt R f x) (hg : DifferentiableAt R g x)
+  : DifferentiableAt R (fun x => f x - g x) x
+  := DifferentiableAt.sub hf hg
+ 
+
+@[differentiable]
+theorem HSub.hSub.arg_a4a5.Differentiable_comp
+  (f g : X → Y) (hf : Differentiable R f) (hg : Differentiable R g)
+  : Differentiable R fun x => f x - g x
+  := fun x => HSub.hSub.arg_a4a5.DifferentiableAt_comp x f g (hf x) (hg x)
+
+
+
+-- HMul.hMul ---------------------------------------------------------------------
+-------------------------------------------------------------------------------- 
+
+@[differentiable]
+def HMul.hMul.arg_a4a5.DifferentiableAt_comp
+  {Y : Type _} [TopologicalSpace Y] [NormedRing Y] [NormedAlgebra R Y] 
+  (x : X) (f g : X → Y) (hf : DifferentiableAt R f x) (hg : DifferentiableAt R g x)
+  : DifferentiableAt R (fun x => f x * g x) x 
+  := DifferentiableAt.mul hf hg
+
+
+@[differentiable]
+def HMul.hMul.arg_a4a5.Differentiable_comp
+  {Y : Type _} [TopologicalSpace Y] [NormedRing Y] [NormedAlgebra R Y] 
+  (f g : X → Y) (hf : Differentiable R f) (hg : Differentiable R g)
+  : Differentiable R (fun x => f x * g x)
+  := Differentiable.mul hf hg
+
+
+
+-- SMul.sMul ---------------------------------------------------------------------
+-------------------------------------------------------------------------------- 
+
+@[differentiable]
+def SMul.sMul.arg_a4a5.DifferentiableAt_comp
+  {Y : Type _} [TopologicalSpace Y] [NormedRing Y] [NormedAlgebra R Y] 
+  (x : X) (f : X → R) (g : X → Y) (hf : DifferentiableAt R f x) (hg : DifferentiableAt R g x)
+  : DifferentiableAt R (fun x => f x • g x) x 
+  := DifferentiableAt.smul hf hg
+
+
+@[differentiable]
+def SMul.sMul.arg_a4a5.Differentiable_comp
+  {Y : Type _} [TopologicalSpace Y] [NormedRing Y] [NormedAlgebra R Y] 
+  (f : X → R) (g : X → Y) (hf : Differentiable R f) (hg : Differentiable R g)
+  : Differentiable R (fun x => f x • g x)
+  := Differentiable.smul hf hg
+
+
+
+-- HDiv.hDiv ---------------------------------------------------------------------
+-------------------------------------------------------------------------------- 
+
+@[differentiable]
+def HDiv.hDiv.arg_a4a5.DifferentiableAt_comp
+  {R : Type _} [NontriviallyNormedField R]
+  {K : Type _} [NontriviallyNormedField K] [NormedAlgebra R K]
+  (x : R) (f : R → K) (g : R → K) 
+  (hf : DifferentiableAt R f x) (hg : DifferentiableAt R g x) (hx : g x ≠ 0)
+  : DifferentiableAt R (fun x => f x / g x) x 
+  := DifferentiableAt.div hf hg hx
+
+
+@[differentiable]
+def HDiv.hDiv.arg_a4a5.Differentiable_comp
+  {R : Type _} [NontriviallyNormedField R]
+  {K : Type _} [NontriviallyNormedField K] [NormedAlgebra R K]
+  (f : R → K) (g : R → K) 
+  (hf : Differentiable R f) (hg : Differentiable R g) (hx : ∀ x, g x ≠ 0)
+  : Differentiable R (fun x => f x / g x)
+  := Differentiable.div hf hg hx
diff --git a/SciLean/FunctionSpaces/Differentiable/Test.lean b/SciLean/FunctionSpaces/Differentiable/Test.lean
new file mode 100644
index 00000000..3b2abfbc
--- /dev/null
+++ b/SciLean/FunctionSpaces/Differentiable/Test.lean
@@ -0,0 +1,72 @@
+import SciLean.FunctionSpaces.Differentiable.Basic
+
+
+open SciLean
+
+
+
+variable 
+  {R : Type _} [NontriviallyNormedField R]
+  {X : Type _} [NormedAddCommGroup X] [NormedSpace R X]
+  {Y : Type _} [NormedAddCommGroup Y] [NormedSpace R Y]
+  {Z : Type _} [NormedAddCommGroup Z] [NormedSpace R Z]
+  {ι : Type _} [Fintype ι]
+  {E : ι → Type _} [∀ i, NormedAddCommGroup (E i)] [∀ i, NormedSpace R (E i)]
+
+
+-- TODO: fix this!!!
+example
+  (f : X → Y×Z) (hf : Differentiable R f)
+  : Differentiable R (fun x => (f x).1)
+  := by (try differentiable); sorry
+
+-- TODO: fix this!!!
+example : 
+  Differentiable R (@Prod.fst X Y)
+:= by (try differentiable); sorry
+
+-- TODO: fix this!!!
+example
+  (f : X → Y×Z) (hf : Differentiable R f)
+  : Differentiable R (fun x => (f x).2)
+  := by (try differentiable); sorry
+
+-- TODO: fix this!!!
+example : 
+  Differentiable R (@Prod.snd X Y)
+:= by (try differentiable); sorry
+
+
+-- TODO: fix this!!!
+example
+  (x' : X)
+  : Differentiable R fun x : X => x' + x
+  := by (try differentiable); sorry
+
+
+
+example
+  {R : Type _} [NontriviallyNormedField R]
+  {K : Type _} [NontriviallyNormedField K] [NormedAlgebra R K]
+  (x : R) (f : R → K) (g : R → K) 
+  (hf : DifferentiableAt R f x) (hg : DifferentiableAt R g x) (hx : g x ≠ 0)
+  : DifferentiableAt R (fun x => f x / g x) x 
+  := by differentiable
+
+
+example
+  {R : Type _} [NontriviallyNormedField R]
+  {K : Type _} [NontriviallyNormedField K] [NormedAlgebra R K]
+  (x : R) (k : K) (g : R → K) 
+   (hg : DifferentiableAt R g x) (hx : g x ≠ 0)
+  : DifferentiableAt R (fun x => k / g x) x 
+  := by differentiable
+
+
+example
+  {R : Type _} [NontriviallyNormedField R]
+  {K : Type _} [NontriviallyNormedField K] [NormedAlgebra R K]
+  (x : R) (f : R → K) (k : K)
+  (hf : DifferentiableAt R f x) (hx : k ≠ 0)
+  : DifferentiableAt R (fun x => f x / k) x 
+  := by differentiable
diff --git a/SciLean/Functions/Interpolate.lean b/SciLean/Functions/Interpolate.lean
index 2bff78b3..8be615d4 100644
--- a/SciLean/Functions/Interpolate.lean
+++ b/SciLean/Functions/Interpolate.lean
@@ -15,6 +15,7 @@ def linearInterpolate1D {X} [Vec X] (f : Int → X) (x : ℝ) : X :=
   let f₁ := f (ix+1)
   f₀ + w • (f₁-f₀)
 
+#exit
 function_properties SciLean.linearInterpolate1D {X : Type} [Vec X] (f : Int → X) (x : ℝ)
 argument f 
   IsSmooth,
diff --git a/SciLean/Lean/Meta/Basic.lean b/SciLean/Lean/Meta/Basic.lean
index 5fb2c243..5316b6cb 100644
--- a/SciLean/Lean/Meta/Basic.lean
+++ b/SciLean/Lean/Meta/Basic.lean
@@ -17,6 +17,27 @@ def getConstArity (constName : Name) : m Nat := do
   let info ← getConstInfo constName
   return info.type.forallArity
 
+/-- Returns name of the head function of an expression
+
+Example:
+  `getFunHeadConst? q(fun x => x + x) = HAdd.hAdd`
+  `getFunHeadConst? q(fun x y => x + y) = HAdd.hAdd`
+  `getFunHeadConst? q(HAdd.hAdd 1) = HAdd.hAdd`
+  `getFunHeadConst? q(fun xy : X×Y => xy.2) = Prod.snd`
+  `getFunHeadConst? q(fun f x => f x) = none`
+-/
+def getFunHeadConst? (e : Expr) : MetaM (Option Name) :=
+  match e with
+  | .const name _ => return name
+  | .app f _ => return f.getAppFn.constName?
+  | .lam _ _ b _ => return b.getAppFn.constName?
+  | .proj structName idx _ => do
+     let .some info := getStructureInfo? (← getEnv) structName
+       | return none
+     return info.getProjFn? idx
+  | _ => return none
+
+
 /-- Changes structure projection back to function application. Left unchanged if not a projection.
 
 For example `proj ``Prod 0 xy` is changed to `mkApp ``Prod.fst #[xy]`.
diff --git a/SciLean/Tactic/FTrans/Basic.lean b/SciLean/Tactic/FTrans/Basic.lean
index d9365fff..e96f6d86 100644
--- a/SciLean/Tactic/FTrans/Basic.lean
+++ b/SciLean/Tactic/FTrans/Basic.lean
@@ -13,7 +13,7 @@ namespace SciLean.FTrans
 
 
 open Elab Term in
-def tacticToDischarge (tacticCode : Syntax) : Expr → SimpM (Option Expr) := fun e => do
+def tacticToDischarge (tacticCode : Syntax) : Expr → MetaM (Option Expr) := fun e => do
     let mvar ← mkFreshExprSyntheticOpaqueMVar e `simp.discharger
     let runTac? : TermElabM (Option Expr) :=
       try
@@ -42,27 +42,11 @@ def tacticToDischarge (tacticCode : Syntax) : Expr → SimpM (Option Expr) := fu
 -/
 def applyTheorems (e : Expr) (discharge? : Expr → SimpM (Option Expr)) : SimpM (Option Simp.Step) := do
 
-  -- using simplifier
-  -- let .some ext ← getSimpExtension? "ftrans_core" | return none
-  -- let thms ← ext.getTheorems
-
-  -- if let some r ← Simp.rewrite? e thms.pre thms.erased discharge? (tag := "pre") (rflOnly := false) then
-  --   return Simp.Step.visit r
-  -- return Simp.Step.visit { expr := e }
-
   let .some (ftransName, _, f) ← getFTrans? e
     | return none
 
-  let .some funName ←
-     match f with
-     | .app f _ => pure f.getAppFn.constName?
-     | .lam _ _ b _ => pure b.getAppFn.constName?
-     | .proj structName idx _ => do
-       let .some info := getStructureInfo? (← getEnv) structName
-         | pure none
-       pure (info.getProjFn? idx)
-     | _ => pure none
-   | pure none
+  let .some funName ← getFunHeadConst? f
+    | return none
 
   let candidates ← FTrans.getFTransRules funName ftransName
 
@@ -70,68 +54,33 @@ def applyTheorems (e : Expr) (discharge? : Expr → SimpM (Option Expr)) : SimpM
     if let some result ← Meta.Simp.tryTheorem? e thm discharge? then
       return Simp.Step.visit result
   return Simp.Step.visit { expr := e }
-
-
-def Info.applyIdentityRule (info : FTrans.Info) (e : Expr) : SimpM (Option Simp.Step) := do
-
-  let .some ruleName := info.identityTheorem
-    | return Simp.Step.visit { expr := e }
-
-  let thm : SimpTheorem := {
-    proof := mkConst ruleName
-    origin := .decl ruleName
-    rfl := false
-  }
-  
-  if let some result ← Meta.Simp.tryTheorem? e thm info.discharger then
-    return Simp.Step.visit result
-  return Simp.Step.visit { expr := e }
-
-
-def Info.applyConstantRule (info : FTrans.Info) (e : Expr) : SimpM (Option Simp.Step) := do
-
-  let .some ruleName := info.constantTheorem
-    | return Simp.Step.visit { expr := e }
-
-  let thm : SimpTheorem := {
-    proof := mkConst ruleName
-    origin := .decl ruleName
-    rfl := false
-  }
-  
-  if let some result ← Meta.Simp.tryTheorem? e thm info.discharger then
-    return Simp.Step.visit result
-  return Simp.Step.visit { expr := e }
   
 
 /-- Try to apply function transformation to `e`. Returns `none` if expression is not a function transformation applied to a function.
   -/
 def main (e : Expr) (discharge? : Expr → SimpM (Option Expr)) : SimpM (Option Simp.Step) := do
 
-  let .some (ftransName, info, f) ← getFTrans? e
+  let .some (ftransName, ext, f) ← getFTrans? e
     | return none
 
   trace[Meta.Tactic.ftrans.step] "{ftransName}\n{← ppExpr e}"
 
   match f with
-  | .lam _ _ (.letE ..) _ => info.applyLambdaLetRule e
-  | .lam _ _ (.lam  ..) _ => info.applyLambdaLambdaRule e
-  -- | .lam _ t _ _  => 
-  --   if let .some e' ← applyStructureRule
-    -- check if `t` is a structure and apply specialized rule for structure projections
-  | .lam _ _ b _ => do
-    if b == .bvar 0 then
-      info.applyIdentityRule e
-    else if !(b.hasLooseBVar 0) then
-      info.applyConstantRule e
-    else
-      applyTheorems e info.discharger
   | .letE .. => letTelescope f λ xs b => do
     -- swap all let bindings and the function transformation
-    let e' ← mkLetFVars xs (info.replaceFTransFun e b)
-    return .some (.visit (.mk e' none 0))
+    let e' ← mkLetFVars xs (ext.replaceFTransFun e b)
+    return .some (.visit { expr := e' })
+
+  | .lam _ _ (.bvar  0) _ => ext.applyIdentityRule e
+  | .lam _ _ (.letE ..) _ => ext.applyLambdaLetRule e
+  | .lam _ _ (.lam  ..) _ => ext.applyLambdaLambdaRule e
+  | .lam _ _ b _ => do
+    if !(b.hasLooseBVar 0) then
+      ext.applyConstantRule e
+    else
+      applyTheorems e (ext.discharger ·)
   | _ => do
-    applyTheorems e info.discharger
+    applyTheorems e (ext.discharger ·)
 
 
 def tryFTrans? (e : Expr) (discharge? : Expr → SimpM (Option Expr)) (post := false) : SimpM (Option Simp.Step) := do
@@ -157,12 +106,15 @@ mutual
         Simp.andThen (← Simp.postDefault e discharge) (fun e' => tryFTrans? e' discharge (post := true))
       discharge? := discharge
     } else {
-      pre  := fun e ↦ Simp.andThen (.visit { expr := e }) (fun e' => tryFTrans? e' discharge)
-      post := fun e ↦ Simp.andThen (.visit { expr := e }) (fun e' => tryFTrans? e' discharge (post := true))
+      pre  := fun e ↦ do 
+        Simp.andThen (.visit { expr := e }) (fun e' => tryFTrans? e' discharge)
+      post := fun e ↦ do
+        Simp.andThen (.visit { expr := e }) (fun e' => tryFTrans? e' discharge (post := true))
       discharge? := discharge
     }
 
-  partial def deriveSimp (e : Expr) : MetaM Simp.Result :=
+  partial def deriveSimp (e : Expr) : MetaM Simp.Result := do
+    withTraceNode `ftrans (fun _ => return s!"ftrans of {← ppExpr e}") do
     (·.1) <$> Tactic.LSimp.main e ctx (methods := methods)
 end
 
@@ -183,7 +135,7 @@ def fTransAt (g : MVarId) (ctx : Simp.Context) (fvarIdsToSimp : Array FVarId)
     MetaM (Option (Array FVarId × MVarId)) := g.withContext do
   g.checkNotAssigned `norm_num
   let mut g := g
-  let mut toAssert := #[]
+  let mut toAssert := #[] 
   let mut replaced := #[]
   for fvarId in fvarIdsToSimp do
     let localDecl ← fvarId.getDecl
diff --git a/SciLean/Tactic/FTrans/Init.lean b/SciLean/Tactic/FTrans/Init.lean
index 8b0266ea..274effd6 100644
--- a/SciLean/Tactic/FTrans/Init.lean
+++ b/SciLean/Tactic/FTrans/Init.lean
@@ -1,11 +1,15 @@
+import Qq
 import Lean.Meta.Tactic.Simp.Types
 
 import Std.Data.RBMap.Alter
 
+import Mathlib.Data.FunLike.Basic
+
 import SciLean.Prelude
 import SciLean.Lean.MergeMapDeclarationExtension
+import SciLean.Lean.Meta.Basic
  
-open Lean Meta.Simp
+open Lean Meta.Simp Qq
 
 namespace SciLean.FTrans
 
@@ -14,7 +18,7 @@ namespace SciLean.FTrans
 -------------
 initialize registerTraceClass `Meta.Tactic.ftrans
 initialize registerTraceClass `Meta.Tactic.ftrans.step
--- initialize registerTraceClass `Meta.Tactic.ftrans.missing_rule
+initialize registerTraceClass `Meta.Tactic.ftrans.missing_rule
 -- initialize registerTraceClass `Meta.Tactic.ftrans.normalize_let
 initialize registerTraceClass `Meta.Tactic.ftrans.rewrite
 initialize registerTraceClass `Meta.Tactic.ftrans.discharge
@@ -28,58 +32,156 @@ register_simp_attr ftrans_simp
 
 macro "ftrans" : attr => `(attr| ftrans_simp ↓)
 
-/-- 
-Function Transformation Info
---
 
-Stores information and custom functionalities for a function transformation.
+open Meta Simp
+
+
+-- TODO: Move RewriteRule to a new file and add a custom version `tryTheorem?` with proper tracing
+
+/-- Rewrite rule can be either provided as a theorem or as a meta program
 -/
-structure Info where
-  getFTransFun? (expr : Expr) : Option Expr
-  replaceFTransFun (expr : Expr) (newFun : Expr) : Expr
-  applyLambdaLetRule    (expr : Expr) : SimpM (Option Step)
-  applyLambdaLambdaRule (expr : Expr) : SimpM (Option Step)
-  identityTheorem : Option Name
-  constantTheorem  : Option Name
-  -- The CoreM monad is likely completely unecessary
-  -- I just do not know how to convert `(tactic| by simp) into Syntax without
-  -- having some kind of monad
-  discharger : Expr → SimpM (Option Expr)
+inductive RewriteRule where
+  | thm  (name : Name) 
+  | eval (f : Expr → MetaM (Option Result))
+deriving Inhabited
 
+
+def RewriteRule.apply (r : RewriteRule) (discharger : Expr → SimpM (Option Expr)) (e : Expr) : SimpM (Option Result) := 
+  match r with
+  | eval f => f e
+  | thm name => do
+
+    let thm : SimpTheorem := {
+      proof := mkConst name
+      origin := .decl name
+      rfl := false
+    }
+
+    let .some result ← Meta.Simp.tryTheorem? e thm discharger
+      | return none
+    return result
+
+
+structure FTransExt where
+  /-- Function transformation name -/
+  ftransName : Name
+  /-- Get function being transformed from function transformation expression -/
+  getFTransFun?    (expr : Expr) : Option Expr
+  /-- Replace function being transformed in function transformation expression -/
+  replaceFTransFun (expr : Expr) (newFun : Expr) : Expr
+  /-- Custom rule for transforming `fun x => x -/
+  identityRule     : Option RewriteRule
+  /-- Custom rule for transforming `fun x => y -/
+  constantRule    : Option RewriteRule
+  /-- Custom rule for transforming `fun x => let y := g x; f x y -/
+  lambdaLetRule    : Option RewriteRule
+  /-- Custom rule for transforming `fun x y => f x y -/
+  lambdaLambdaRule : Option RewriteRule
+  /-- Custom discharger for this function transformation -/
+  discharger       : Expr → MetaM (Option Expr)
+  /-- Name of this extension, keep the default value! -/
+  name : Name := by exact decl_name%
 deriving Inhabited
 
-private def Info.merge! (ftrans : Name) (_ _ : Info) : Info :=
-panic! 
-s!"Two conflicting definitions for function transformation `{ftrans}` found!
 
-  Keep only one and remove the other."
+def FTransExt.applyLambdaLetRule (ext : FTransExt) (e : Expr) : SimpM Step := do
+  let .some r := ext.lambdaLetRule 
+    | trace[Meta.Tactic.ftrans.missing_rule] "Missing lambda-let rule a rule for `{ext.ftransName}`"
+      return .visit { expr := e }
 
-initialize FTransExt : MergeMapDeclarationExtension Info 
-  ← mkMergeMapDeclarationExtension ⟨Info.merge!, sorry_proof⟩
+  if let .some r ← r.apply (ext.discharger ·) e then
+    return .visit r
+  else
+    trace[Meta.Tactic.ftrans.discharge] "Failed applying lambda-let rule to `{← ppExpr e}"
+    return .visit { expr := e }
 
+def FTransExt.applyLambdaLambdaRule (ext : FTransExt) (e : Expr) : SimpM Step := do
+  let .some r := ext.lambdaLambdaRule 
+    | trace[Meta.Tactic.ftrans.missing_rule] "Missing lambda-lambda rule a rule for `{ext.ftransName}`"
+      return .visit { expr := e }
+
+  if let .some r ← r.apply (ext.discharger ·) e then
+    return .visit r
+  else
+    trace[Meta.Tactic.ftrans.discharge] "Failed applying lambda-lambda rule to `{← ppExpr e}"
+    return .visit { expr := e }
+
+def FTransExt.applyIdentityRule (ext : FTransExt) (e : Expr) : SimpM Step := do
+  let .some r := ext.identityRule 
+    | trace[Meta.Tactic.ftrans.missing_rule] "Missing identity rule a rule for `{ext.ftransName}`"
+      return .visit { expr := e }
+
+  if let .some r ← r.apply (ext.discharger ·) e then
+    return .visit r
+  else
+    trace[Meta.Tactic.ftrans.discharge] "Failed applying identity rule to `{← ppExpr e}"
+    return .visit { expr := e }
+
+def FTransExt.applyConstantRule (ext : FTransExt) (e : Expr) : SimpM Step := do
+  let .some r := ext.constantRule 
+    | trace[Meta.Tactic.ftrans.missing_rule] "Missing constant rule a rule for `{ext.ftransName}`"
+      return .visit { expr := e }
+
+  if let .some r ← r.apply (ext.discharger ·) e then
+    return .visit r
+  else
+    trace[Meta.Tactic.ftrans.discharge] "Failed applying constant rule to `{← ppExpr e}"
+    return .visit { expr := e }
+
+
+def mkFTransExt (n : Name) : ImportM FTransExt := do
+  let { env, opts, .. } ← read
+  IO.ofExcept <| unsafe env.evalConstCheck FTransExt opts ``FTransExt n
+
+
+initialize ftransExt : PersistentEnvExtension (Name × Name) (Name × FTransExt) (Std.RBMap Name FTransExt Name.quickCmp) ←
+  registerPersistentEnvExtension {
+    mkInitial := pure {}
+    addImportedFn := fun s => do
+
+      let mut r : Std.RBMap Name FTransExt Name.quickCmp := {}
+
+      for s' in s do
+        for (ftransName, extName) in s' do
+          let ext ← mkFTransExt extName
+          r := r.insert ftransName ext
+
+      pure r
+    addEntryFn := fun s (n, ext) => s.insert n ext
+    exportEntriesFn := fun s => s.valuesArray.map (fun ext => (ext.ftransName, ext.name))
+  }
 
 /-- 
   Returns function transformation name and function being tranformed if `e` is function tranformation expression.
  -/
-def getFTrans? (e : Expr) : CoreM (Option (Name × Info × Expr)) := do
-  let .some ftransName := e.getAppFn.constName?
+def getFTrans? (e : Expr) : CoreM (Option (Name × FTransExt × Expr)) := do
+  let .some ftransName := 
+      match e.getAppFn.constName? with
+      | none => none
+      | .some name => 
+        if name != ``FunLike.coe then
+          name
+        else if let .some ftrans := e.getArg? 4 then
+          ftrans.getAppFn.constName? 
+        else
+          none
     | return none
 
-  let .some info ← FTransExt.find? ftransName
+  let .some ext := (ftransExt.getState (← getEnv)).find? ftransName
     | return none
 
-  let .some f := info.getFTransFun? e
+  let .some f := ext.getFTransFun? e
     | return none
 
-  return (ftransName, info, f)
+  return (ftransName, ext, f)
 
 /-- 
   Returns function transformation info if `e` is function tranformation expression.
  -/
-def getFTransInfo? (e : Expr) : CoreM (Option Info) := do
-  let .some (_, info, _) ← getFTrans? e
+def getFTransExt? (e : Expr) : CoreM (Option FTransExt) := do
+  let .some (_, ext, _) ← getFTrans? e
     | return none
-  return info
+  return ext
 
 /-- 
   Returns function transformation info if `e` is function btranformation expression.
@@ -90,7 +192,6 @@ def getFTransFun? (e : Expr) : CoreM (Option Expr) := do
   return f
 
 
-
 --------------------------------------------------------------------------------
 --------------------------------------------------------------------------------
 --------------------------------------------------------------------------------
@@ -141,10 +242,10 @@ initialize funTransRuleAttr : TagAttribute ←
       MetaM.run' do
         forallTelescope rule λ _ eq => do
 
-          let .some (_,lhs,rhs) := eq.app3? ``Eq
+          let .some (_,lhs,_) := eq.app3? ``Eq
             | throwError s!"`{← ppExpr eq}` is not a rewrite rule!"
 
-          let .some (transName, transInfo, f) ← getFTrans? lhs
+          let .some (transName, _, f) ← getFTrans? lhs
             | throwError s!
 "`{← ppExpr eq}` is not a rewrite rule of known function transformaion!
 To register function transformation call:
@@ -154,11 +255,7 @@ To register function transformation call:
 ```
 where <name> is name of the function transformation and <info> is corresponding `FTrans.Info`. 
 "
-          let .some funName := 
-              match f with 
-              | .app f _ => f.getAppFn.constName?
-              | .lam _ _ b _ => b.getAppFn.constName?
-              | _ => none
+          let .some funName ← getFunHeadConst? f
             | throwError "Function being transformed is in invalid form!"
 
           FTransRulesExt.insert funName (FTransRules.empty.insert transName ruleName)