diff --git a/SciLean.lean b/SciLean.lean
index 892facf3..5c6b5394 100644
--- a/SciLean.lean
+++ b/SciLean.lean
@@ -10,6 +10,9 @@ import SciLean.Data.Fin
 
 import SciLean.Modules.DifferentialEquations
 
+import SciLean.Util.Profile
+
+
 /-!
 
 SciLean
diff --git a/SciLean/Core/Distribution/Basic.lean b/SciLean/Core/Distribution/Basic.lean
index 2d864a15..7f0a2279 100644
--- a/SciLean/Core/Distribution/Basic.lean
+++ b/SciLean/Core/Distribution/Basic.lean
@@ -217,10 +217,10 @@ theorem Distribution.smul_extAction (r : R) (T : 𝒟'(X,U)) (φ : X → V) (L :
 theorem Distribution.neg_extAction (T : 𝒟'(X,U)) (φ : X → V) (L : U ⊸ V ⊸ W) :
     (- T).extAction φ L = - T.extAction φ L := by sorry_proof
 
-open BigOperators in
-@[action_push]
-theorem Distribution.fintype_sum_extAction {I} [Fintype I] (T : I → 𝒟'(X,U)) (φ : X → V) (L : U ⊸ V ⊸ W) :
-    (∑ i, T i).extAction φ L = ∑ i, (T i).extAction φ L := by sorry_proof
+-- open BigOperators in
+-- @[action_push]
+-- theorem Distribution.fintype_sum_extAction {I} [Fintype I] (T : I → 𝒟'(X,U)) (φ : X → V) (L : U ⊸ V ⊸ W) :
+--     (∑ i, T i).extAction φ L = ∑ i, (T i).extAction φ L := by sorry_proof
 
 @[action_push]
 theorem Distribution.indextype_sum_extAction {I} [IndexType I] (T : I → 𝒟'(X,U)) (φ : X → V) (L : U ⊸ V ⊸ W) :
@@ -328,15 +328,15 @@ theorem neg_restrict (T : 𝒟'(X,Y)) (A : Set X) :
 theorem neg_restrict' (T : 𝒟'(X,Y)) (A : Set X) :
     - (T.restrict A) = (- T).restrict A := sorry_proof
 
-open BigOperators in
-@[restrict_push]
-theorem finset_sum_restrict {I} [Fintype I] (T : I → 𝒟'(X,Y)) (A : Set X) :
-    (∑ i, T i).restrict A = ∑ i, (T i).restrict A := sorry_proof
+-- open BigOperators in
+-- @[restrict_push]
+-- theorem finset_sum_restrict {I} [Fintype I] (T : I → 𝒟'(X,Y)) (A : Set X) :
+--     (∑ i, T i).restrict A = ∑ i, (T i).restrict A := sorry_proof
 
-open BigOperators in
-@[restrict_pull]
-theorem finset_sum_restrict' {I} [Fintype I] (T : I → 𝒟'(X,Y)) (A : Set X) :
-    ∑ i, (T i).restrict A = (∑ i, T i).restrict A := sorry_proof
+-- open BigOperators in
+-- @[restrict_pull]
+-- theorem finset_sum_restrict' {I} [Fintype I] (T : I → 𝒟'(X,Y)) (A : Set X) :
+--     ∑ i, (T i).restrict A = (∑ i, T i).restrict A := sorry_proof
 
 @[restrict_push]
 theorem indextype_sum_restrict {I} [IndexType I] (T : I → 𝒟' X) (A : Set X) :
diff --git a/SciLean/Core/FloatAsReal.lean b/SciLean/Core/FloatAsReal.lean
index 62c4176b..743dd0ee 100644
--- a/SciLean/Core/FloatAsReal.lean
+++ b/SciLean/Core/FloatAsReal.lean
@@ -45,7 +45,8 @@ instance : Field Float where
   inv_zero := sorry_proof
   qsmul q x := (q.num * x) / q.den
   qsmul_def := sorry_proof
-
+  nnqsmul q x := (q.num * x) / q.den
+  nnqsmul_def := sorry_proof
 
 instance : DecidableEq Float := fun x y =>
   if x ≤ y && y ≤ x
@@ -79,6 +80,8 @@ instance : LinearOrderedField Float where
   div_eq_mul_inv := sorry_proof
   qsmul q x := (q.num * x) / q.den
   qsmul_def := sorry_proof
+  nnqsmul q x := (q.num * x) / q.den
+  nnqsmul_def := sorry_proof
 
 
 instance : SeminormedRing Float where
@@ -106,6 +109,7 @@ instance : DenselyNormedField Float where
 instance : StarRing Float where
   star_add := sorry_proof
 
+
 instance : Algebra ℝ Float where
   smul := fun r x => realToFloat r * x
   toFun := realToFloat
@@ -245,5 +249,5 @@ instance : MeasureTheory.MeasureSpace Float where
     mono := sorry_proof
     iUnion_nat := sorry_proof
     m_iUnion := sorry_proof
-    trimmed := sorry_proof
+    trim_le := sorry_proof
 }
diff --git a/SciLean/Core/FunctionPropositions/HasSemiAdjoint.lean b/SciLean/Core/FunctionPropositions/HasSemiAdjoint.lean
index 0d473507..8e63988b 100644
--- a/SciLean/Core/FunctionPropositions/HasSemiAdjoint.lean
+++ b/SciLean/Core/FunctionPropositions/HasSemiAdjoint.lean
@@ -5,8 +5,8 @@ import SciLean.Core.FunctionPropositions.IsSmoothLinearMap
 import SciLean.Core.Simp
 import SciLean.Core.Meta.GenerateLinearMapSimp
 
-import Mathlib.Tactic.FunTrans.Attr
-import Mathlib.Tactic.FunTrans.Elab
+import SciLean.Tactic.FunTrans.Attr
+import SciLean.Tactic.FunTrans.Elab
 
 set_option linter.unusedVariables false
 
diff --git a/SciLean/Core/FunctionPropositions/IsLinearMap.lean b/SciLean/Core/FunctionPropositions/IsLinearMap.lean
index 93dfc042..545e2a58 100644
--- a/SciLean/Core/FunctionPropositions/IsLinearMap.lean
+++ b/SciLean/Core/FunctionPropositions/IsLinearMap.lean
@@ -6,6 +6,7 @@ import SciLean.Core.Objects.FinVec
 import SciLean.Core.Meta.GenerateLinearMapSimp
 
 set_option linter.unusedVariables false
+set_option linter.hashCommand false
 
 --------------------------------------------------------------------------------
 open LeanColls
diff --git a/SciLean/Core/FunctionPropositions/IsSmoothLinearMap.lean b/SciLean/Core/FunctionPropositions/IsSmoothLinearMap.lean
index 5f3a8e54..8b4799f9 100644
--- a/SciLean/Core/FunctionPropositions/IsSmoothLinearMap.lean
+++ b/SciLean/Core/FunctionPropositions/IsSmoothLinearMap.lean
@@ -35,7 +35,7 @@ theorem id_rule : IsSmoothLinearMap K (fun x : X => x) := by constructor <;> fun
 variable (Y)
 @[fun_prop]
 theorem const_zero_rule : IsSmoothLinearMap K (fun _ : X => (0 : Y)) := by
-  constructor <;> first | fun_prop | apply IsLinearMap.isLinearMap_const_zero
+  constructor <;> first | fun_prop
 variable {Y}
 
 variable {X}
diff --git a/SciLean/Core/FunctionSpaces/SmoothLinearMap.lean b/SciLean/Core/FunctionSpaces/SmoothLinearMap.lean
index 29993cad..fbe7b9e6 100644
--- a/SciLean/Core/FunctionSpaces/SmoothLinearMap.lean
+++ b/SciLean/Core/FunctionSpaces/SmoothLinearMap.lean
@@ -130,8 +130,8 @@ instance : Vec K (X ⊸[K] Y) := Vec.mkSorryProofs
 
 open BigOperators in
 @[simp, ftrans_simp]
-theorem SmoothLinearMap.fintype_sum_apply {I} [Fintype I] (f : I → X⊸[K] Y) (x : X) :
-    (∑ i, f i) x = ∑ i, f i x  := by sorry_proof
+theorem SmoothLinearMap.fintype_sum_apply {I} (A : Finset I) (f : I → X⊸[K] Y) (x : X) :
+    (Finset.sum A f) x = Finset.sum A (f · x)  := by sorry_proof
 
 @[simp, ftrans_simp]
 theorem SmoothLinearMap.indextype_sum_apply {I} [IndexType I] (f : I → X⊸[K] Y) (x : X) :
diff --git a/SciLean/Core/FunctionTransformations/Broadcast.lean b/SciLean/Core/FunctionTransformations/Broadcast.lean
index 3544d75e..50c68db9 100644
--- a/SciLean/Core/FunctionTransformations/Broadcast.lean
+++ b/SciLean/Core/FunctionTransformations/Broadcast.lean
@@ -1,7 +1,7 @@
 import SciLean.Core.Objects.BroadcastType
 
-import Mathlib.Tactic.FunTrans.Attr
-import Mathlib.Tactic.FunTrans.Elab
+import SciLean.Tactic.FunTrans.Attr
+import SciLean.Tactic.FunTrans.Elab
 
 namespace SciLean
 
diff --git a/SciLean/Core/FunctionTransformations/CDeriv.lean b/SciLean/Core/FunctionTransformations/CDeriv.lean
index 3d687828..4e5a193c 100644
--- a/SciLean/Core/FunctionTransformations/CDeriv.lean
+++ b/SciLean/Core/FunctionTransformations/CDeriv.lean
@@ -3,8 +3,8 @@ import SciLean.Core.FunctionPropositions.IsSmoothLinearMap
 
 import SciLean.Core.Meta.GenerateLinearMapSimp
 
-import Mathlib.Tactic.FunTrans.Attr
-import Mathlib.Tactic.FunTrans.Elab
+import SciLean.Tactic.FunTrans.Attr
+import SciLean.Tactic.FunTrans.Elab
 
 set_option linter.unusedVariables false
 
diff --git a/SciLean/Core/FunctionTransformations/Complexify.lean b/SciLean/Core/FunctionTransformations/Complexify.lean
index c7af9738..dc2f5bd7 100644
--- a/SciLean/Core/FunctionTransformations/Complexify.lean
+++ b/SciLean/Core/FunctionTransformations/Complexify.lean
@@ -1,7 +1,7 @@
 import SciLean.Core.Objects.FinVec
 
-import Mathlib.Tactic.FunTrans.Attr
-import Mathlib.Tactic.FunTrans.Elab
+import SciLean.Tactic.FunTrans.Attr
+import SciLean.Tactic.FunTrans.Elab
 
 namespace SciLean
 
diff --git a/SciLean/Core/FunctionTransformations/FDeriv.lean b/SciLean/Core/FunctionTransformations/FDeriv.lean
index f9a63b36..f26e07a8 100644
--- a/SciLean/Core/FunctionTransformations/FDeriv.lean
+++ b/SciLean/Core/FunctionTransformations/FDeriv.lean
@@ -8,8 +8,8 @@ import Mathlib.Analysis.Calculus.FDeriv.Mul
 import Mathlib.Analysis.Calculus.Deriv.Basic
 import Mathlib.Analysis.Calculus.Deriv.Inv
 
-import Mathlib.Tactic.FunTrans.Attr
-import Mathlib.Tactic.FunTrans.Elab
+import SciLean.Tactic.FunTrans.Attr
+import SciLean.Tactic.FunTrans.Elab
 
 import SciLean.Core.Meta.ToAnyPoint
 import SciLean.Core.FunctionPropositions.IsContinuousLinearMap
diff --git a/SciLean/Core/FunctionTransformations/FwdFDeriv.lean b/SciLean/Core/FunctionTransformations/FwdFDeriv.lean
index 76305fc1..51ab872f 100644
--- a/SciLean/Core/FunctionTransformations/FwdFDeriv.lean
+++ b/SciLean/Core/FunctionTransformations/FwdFDeriv.lean
@@ -236,13 +236,13 @@ def HPow.hPow.arg_a0.fwdFDeriv_rule_at (n : Nat) (x : X)
 
 open BigOperators in
 @[fun_trans, to_any_point]
-theorem FinType.sum.arg_f.fwdFDeriv_rule_at (x : X)
+theorem FinType.sum.arg_f.fwdFDeriv_rule_at (x : X) (A : Finset ι)
     (f : X → ι → Y) (hf : ∀ i, DifferentiableAt K (f · i) x) :
-    fwdFDeriv K (fun x => ∑ i, f x i) x
+    fwdFDeriv K (fun x => Finset.sum A (f x)) x
     =
     fun dx =>
       let ydy := fun i => fwdFDeriv K (f · i) x dx
-      ∑ i, ydy i := by
+      Finset.sum A ydy := by
   unfold fwdFDeriv; fun_trans
   sorry_proof
 
diff --git a/SciLean/Core/FunctionTransformations/InvFun.lean b/SciLean/Core/FunctionTransformations/InvFun.lean
index b78e9ab9..419fffe9 100644
--- a/SciLean/Core/FunctionTransformations/InvFun.lean
+++ b/SciLean/Core/FunctionTransformations/InvFun.lean
@@ -1,7 +1,7 @@
 import SciLean.Core.FunctionPropositions.Bijective
 
-import Mathlib.Tactic.FunTrans.Attr
-import Mathlib.Tactic.FunTrans.Elab
+import SciLean.Tactic.FunTrans.Attr
+import SciLean.Tactic.FunTrans.Elab
 
 set_option linter.unusedVariables false
 
diff --git a/SciLean/Core/FunctionTransformations/Preimage.lean b/SciLean/Core/FunctionTransformations/Preimage.lean
index c3dde0ae..02fc6a5f 100644
--- a/SciLean/Core/FunctionTransformations/Preimage.lean
+++ b/SciLean/Core/FunctionTransformations/Preimage.lean
@@ -1,8 +1,8 @@
 import Mathlib.Data.Set.Defs
 import Mathlib.Data.Set.Image
 
-import Mathlib.Tactic.FunTrans.Attr
-import Mathlib.Tactic.FunTrans.Elab
+import SciLean.Tactic.FunTrans.Attr
+import SciLean.Tactic.FunTrans.Elab
 
 import SciLean.Core.Objects.Scalar
 import SciLean.Util.SorryProof
diff --git a/SciLean/Core/FunctionTransformations/SemiAdjoint.lean b/SciLean/Core/FunctionTransformations/SemiAdjoint.lean
index c8a54434..60c31121 100644
--- a/SciLean/Core/FunctionTransformations/SemiAdjoint.lean
+++ b/SciLean/Core/FunctionTransformations/SemiAdjoint.lean
@@ -231,11 +231,11 @@ by
 
 open BigOperators in
 @[fun_trans]
-theorem Finset.sum.arg_f.semiAdjoint_rule {ι : Type _} [Fintype ι]
+theorem Finset.sum.arg_f.semiAdjoint_rule {ι : Type _} (A : Finset ι)
   (f : X → ι → Y) (hf : ∀ i, HasSemiAdjoint K (f · i))
-  : semiAdjoint K (fun x => ∑ i, f x i)
+  : semiAdjoint K (fun x => Finset.sum A (fun i => f x i))
     =
-    (fun y => ∑ i, semiAdjoint K (f · i) y) :=
+    (fun y => Finset.sum A (fun i => semiAdjoint K (f · i) y)) :=
 by
   sorry_proof
 
diff --git a/SciLean/Core/FunctionTransformations/ToMatrix.lean b/SciLean/Core/FunctionTransformations/ToMatrix.lean
index 71eedec8..1cd3d47b 100644
--- a/SciLean/Core/FunctionTransformations/ToMatrix.lean
+++ b/SciLean/Core/FunctionTransformations/ToMatrix.lean
@@ -1,8 +1,8 @@
 import SciLean.Core.Objects.FinVec
 import SciLean.Core.FunctionPropositions.IsLinearMap
 
-import Mathlib.Tactic.FunTrans.Attr
-import Mathlib.Tactic.FunTrans.Elab
+import SciLean.Tactic.FunTrans.Attr
+import SciLean.Tactic.FunTrans.Elab
 
 open SciLean LeanColls
 
diff --git a/SciLean/Core/Integral/Common.lean b/SciLean/Core/Integral/Common.lean
index b671b8cc..f0a7db5c 100644
--- a/SciLean/Core/Integral/Common.lean
+++ b/SciLean/Core/Integral/Common.lean
@@ -77,7 +77,7 @@ theorem surfaceIntegral_parametrization (f : X → U) (d) (φ ψ : X → R)
     =
     let sub := fun i x => p i x (g i x)
     let J := fun i x => jacobian R (sub i) x
-    ∑ i : I, ∫' x in dom i, J i x • f (sub i x) := sorry_proof
+    Finset.sum Finset.univ (fun i => ∫' x in dom i, J i x • f (sub i x)) := sorry_proof
 
 
 open BigOperators in
@@ -89,7 +89,7 @@ theorem surfaceIntegral_inter_parametrization (f : X → U) (d) (φ ψ : X → R
     [Fintype I] [∀ i, SemiHilbert R (X₁ i)] [∀ i, MeasureSpace (X₁ i)] :
     ∫' x in {x | φ x = ψ x} ∩ A, f x ∂((surfaceMeasure d))
     =
-    ∑ i : I,
+    Finset.sum Finset.univ fun i =>
       let sub := fun x => p i x (g i x)
       let J := fun x => jacobian R sub x
       ∫' x in sub ⁻¹' A ∩ dom i, J x • f (sub x) := sorry_proof
diff --git a/SciLean/Core/Integral/Substitution.lean b/SciLean/Core/Integral/Substitution.lean
index 927f688e..3f016409 100644
--- a/SciLean/Core/Integral/Substitution.lean
+++ b/SciLean/Core/Integral/Substitution.lean
@@ -27,4 +27,4 @@ theorem integral_parametric_inverse (φ ψ : X → W) (f : X → Y) (hdim : d =
   [Fintype I] [∀ i, SemiHilbert R (X₁ i)] [∀ i, MeasureSpace (X₁ i)] :
   ∫' x in {x' | φ x' = ψ x'}, f x ∂(surfaceMeasure d)
   =
-  ∑ i, ∫' x₁ in dom i, jacobian R (fun x => p i x (ζ i x)) x₁ • f (p i x₁ (ζ i x₁)) := sorry_proof
+  Finset.sum Finset.univ (fun i => ∫' x₁ in dom i, jacobian R (fun x => p i x (ζ i x)) x₁ • f (p i x₁ (ζ i x₁))) := sorry_proof
diff --git a/SciLean/Core/Meta/GenerateLinearMapSimp.lean b/SciLean/Core/Meta/GenerateLinearMapSimp.lean
index cf5ef901..f8da5cab 100644
--- a/SciLean/Core/Meta/GenerateLinearMapSimp.lean
+++ b/SciLean/Core/Meta/GenerateLinearMapSimp.lean
@@ -9,6 +9,7 @@ import SciLean.Tactic.AnalyzeConstLambda
 open LeanColls
 namespace SciLean
 
+set_option linter.unusedVariables false
 
 section HelperTheorems
 
@@ -34,7 +35,7 @@ theorem _root_.IsLinearMap.add_pull (x x' : X)
 theorem _root_.IsLinearMap.sum_push
   {f : X → Y} (hf : IsLinearMap K f)
   (ι : Type) [IndexType.{_,u} ι] [IndexType.{_,v} ι] (x : ι → X)
-  : (∑ i, f (x i)) = f (∑ i, x i) := by sorry_proof
+  : (∑ i : ι, f (x i)) = f (∑ i, x i) := by sorry_proof
 
 -- todo: this is not sufficiently universe polymorphic
 --       and somethimes forces to write non-universe polymorphic code
@@ -146,7 +147,7 @@ def generateLinearMapSimp
 
   let thrmVal : TheoremVal :=
   {
-    name  := data.constName |>.append data.declSuffix |>.append thrmName
+    name  := data.constName |>.append (.mkSimple data.declSuffix) |>.append thrmName
     type  := statement
     value := proof
     levelParams := (collectLevelParams {} statement).params.toList
diff --git a/SciLean/Core/Meta/ParametrizeFVars.lean b/SciLean/Core/Meta/ParametrizeFVars.lean
index 04e23fc5..a6ee1c33 100644
--- a/SciLean/Core/Meta/ParametrizeFVars.lean
+++ b/SciLean/Core/Meta/ParametrizeFVars.lean
@@ -1,7 +1,7 @@
 import Lean
 import Qq
 
-import Std.Tactic.GuardMsgs
+import Batteries.Tactic.GuardMsgs
 import SciLean.Lean.Meta.Basic
 
 open Lean Meta Qq
diff --git a/SciLean/Core/Monads/FwdDerivMonad.lean b/SciLean/Core/Monads/FwdDerivMonad.lean
index 575edfa6..dbb35ca9 100644
--- a/SciLean/Core/Monads/FwdDerivMonad.lean
+++ b/SciLean/Core/Monads/FwdDerivMonad.lean
@@ -189,7 +189,9 @@ by
              fun x => pure (g' x) >>= f') by simp]
     rw[fwdDerivM_bind f' (fun x => pure (g' x)) hf (CDifferentiableM_pure g' hg')]
     simp[fwdDerivM_pure (K:=K) g' hg']
-    fun_trans; simp
+    -- fun_trans
+    -- simp
+  sorry_proof
 
 end fwdDerivM
 
@@ -274,7 +276,7 @@ by
 
   have hg : CDifferentiableM K (fun x => do let y ← a0 x; pure (x,y)) :=
     by apply FwdDerivMonad.CDifferentiableM_pair a0 ha0
-  have hf : CDifferentiableM K f := by fun_prop
+  have hf : CDifferentiableM K f := by simp[f]; fun_prop
 
   apply FwdDerivMonad.CDifferentiableM_bind _ _ hf hg
 
@@ -301,7 +303,7 @@ by
 
   have hg : CDifferentiableM K (fun x => do let y ← a0 x; pure (x,y)) :=
     by apply FwdDerivMonad.CDifferentiableM_pair a0 ha0
-  have hf : CDifferentiableM K f := by fun_prop
+  have hf : CDifferentiableM K f := by simp [f]; fun_prop
 
   rw [FwdDerivMonad.fwdDerivM_bind _ _ hf hg]
   simp [FwdDerivMonad.fwdDerivM_pair a0 ha0]
diff --git a/SciLean/Core/Monads/RevDerivMonad.lean b/SciLean/Core/Monads/RevDerivMonad.lean
index c7feeaae..97022739 100644
--- a/SciLean/Core/Monads/RevDerivMonad.lean
+++ b/SciLean/Core/Monads/RevDerivMonad.lean
@@ -110,6 +110,7 @@ by
            fun x => pure (g' x) >>= f') by simp]
   apply HasAdjDiffM_bind _ _ hf
   apply HasAdjDiffM_pure g'
+  simp[g']
   fun_prop
 
 
@@ -169,6 +170,7 @@ by
     rw[revDerivM_bind f (fun x => pure (g x))
          hf (HasAdjDiffM_pure _ hg)]
     simp[revDerivM_pure g hg]
+  rfl
 
 @[fun_trans]
 theorem let_rule
@@ -195,7 +197,8 @@ by
              fun x => pure (g' x) >>= f') by simp]
     rw[revDerivM_bind f' (fun x => pure (g' x)) hf (HasAdjDiffM_pure g' hg')]
     simp[revDerivM_pure (K:=K) g' hg']
-    fun_trans; simp
+    -- fun_trans; simp
+  sorry_proof
 
 end revDerivM
 
@@ -284,7 +287,7 @@ by
 
   have hg : HasAdjDiffM K (fun x => do let y ← a0 x; pure (x,y)) :=
     by apply RevDerivMonad.HasAdjDiffM_pair a0 ha0
-  have hf : HasAdjDiffM K f := by fun_prop
+  have hf : HasAdjDiffM K f := by simp[f]; fun_prop
 
   apply RevDerivMonad.HasAdjDiffM_bind _ _ hf hg
 
@@ -316,7 +319,7 @@ by
 
   have hg : HasAdjDiffM K (fun x => do let y ← a0 x; pure (x,y)) :=
     by apply RevDerivMonad.HasAdjDiffM_pair a0 ha0
-  have hf : HasAdjDiffM K f := by fun_prop
+  have hf : HasAdjDiffM K f := by simp[f]; fun_prop
 
   rw [RevDerivMonad.revDerivM_bind _ _ hf hg]
   simp [RevDerivMonad.revDerivM_pair a0 ha0]
diff --git a/SciLean/Core/Objects/IsomorphicType.lean b/SciLean/Core/Objects/IsomorphicType.lean
index eeaa71fe..99e7866c 100644
--- a/SciLean/Core/Objects/IsomorphicType.lean
+++ b/SciLean/Core/Objects/IsomorphicType.lean
@@ -1,7 +1,7 @@
 import Mathlib.Logic.Equiv.Basic
 
-import Mathlib.Tactic.FunTrans.Attr
-import Mathlib.Tactic.FunTrans.Elab
+import SciLean.Tactic.FunTrans.Attr
+import SciLean.Tactic.FunTrans.Elab
 
 import SciLean.Tactic.FTrans.Simp
 
diff --git a/SciLean/Core/Objects/Vec.lean b/SciLean/Core/Objects/Vec.lean
index 4e9cf3e6..6b6955ab 100644
--- a/SciLean/Core/Objects/Vec.lean
+++ b/SciLean/Core/Objects/Vec.lean
@@ -6,6 +6,7 @@ import SciLean.Util.SorryProof
 
 namespace SciLean
 
+set_option linter.unusedVariables false
 
 -- TODO: move this section
 namespace Curve
diff --git a/SciLean/Core/old/Meta/FunctionProperty/EnvExtension.lean b/SciLean/Core/old/Meta/FunctionProperty/EnvExtension.lean
index 9abd5ce5..7af0aa01 100644
--- a/SciLean/Core/old/Meta/FunctionProperty/EnvExtension.lean
+++ b/SciLean/Core/old/Meta/FunctionProperty/EnvExtension.lean
@@ -1,4 +1,4 @@
-import Std.Data.RBMap.Alter
+import Batteries.Data.RBMap.Alter
 
 import SciLean.Lean.MergeMapDeclarationExtension
 import SciLean.Lean.Meta.Basic
diff --git a/SciLean/Core/old/Meta/FunctionProperty/LocalContext.lean b/SciLean/Core/old/Meta/FunctionProperty/LocalContext.lean
index 5f32b7cd..090a4c86 100644
--- a/SciLean/Core/old/Meta/FunctionProperty/LocalContext.lean
+++ b/SciLean/Core/old/Meta/FunctionProperty/LocalContext.lean
@@ -1,5 +1,5 @@
-import Std.Data.RBMap.Alter
-import Std.Data.HashMap
+import Batteries.Data.RBMap.Alter
+import Batteries.Data.HashMap
 
 import SciLean.Lean.Meta.Basic
 import SciLean.Data.ArraySet
diff --git a/SciLean/Core/old/Tactic/FunctionTransformation/Core.lean b/SciLean/Core/old/Tactic/FunctionTransformation/Core.lean
index 629fee67..484e9bdb 100644
--- a/SciLean/Core/old/Tactic/FunctionTransformation/Core.lean
+++ b/SciLean/Core/old/Tactic/FunctionTransformation/Core.lean
@@ -1,4 +1,4 @@
-import Std.Lean.Parser
+import Batteries.Lean.Parser
 import Mathlib.Tactic.NormNum.Core
 
 import SciLean.Lean.Meta.Basic
diff --git a/SciLean/Core/old/Tactic/FunctionTransformation/Init.lean b/SciLean/Core/old/Tactic/FunctionTransformation/Init.lean
index d8dbe813..6955ce8a 100644
--- a/SciLean/Core/old/Tactic/FunctionTransformation/Init.lean
+++ b/SciLean/Core/old/Tactic/FunctionTransformation/Init.lean
@@ -1,7 +1,7 @@
 import Lean
 import Qq
 
-import Std.Data.RBMap.Alter
+import Batteries.Data.RBMap.Alter
 import SciLean.Lean.Array
 import SciLean.Lean.MergeMapDeclarationExtension
 
diff --git a/SciLean/Data/ArraySet.lean b/SciLean/Data/ArraySet.lean
index 9448ce5f..ce2e3b7f 100644
--- a/SciLean/Data/ArraySet.lean
+++ b/SciLean/Data/ArraySet.lean
@@ -1,5 +1,5 @@
-import Std.Data.Array.Merge
-import Std.Data.List.Basic
+import Batteries.Data.Array.Merge
+import Batteries.Data.List.Basic
 
 import SciLean.Lean.Array
 import SciLean.Util.SorryProof
@@ -13,7 +13,7 @@ namespace SciLean
   -/
 structure ArraySet (α : Type _) [ord : Ord α] where
   data : Array α
-  isSet : data.sortAndDeduplicate = data
+  isSet : data.sortDedup = data
 deriving Hashable
 
 namespace ArraySet
@@ -32,7 +32,7 @@ namespace ArraySet
   instance [ToString α] : ToString (ArraySet α) := ⟨λ as => toString as.data⟩
 
   def _root_.Array.toArraySet (as : Array α) : ArraySet α where
-    data := as.sortAndDeduplicate
+    data := as.sortDedup
     isSet := sorry_proof
 
   def mem (as : ArraySet α) (a : α) [DecidableEq α] : Bool := Id.run do
@@ -57,7 +57,7 @@ namespace ArraySet
   instance (a b : ArraySet α) : Decidable (a ⊆ b) := Id.run do
     let mut j := 0
     for h : i in [0:b.size] do
-      if h' : (a.size - j) > (b.size - i) then
+      if _h' : (a.size - j) > (b.size - i) then
         return isFalse sorry_proof
       if h' : j < a.size then
         have _ := h.2
diff --git a/SciLean/Data/ArrayType/Algebra.lean b/SciLean/Data/ArrayType/Algebra.lean
index 38e5042e..bbf67cce 100644
--- a/SciLean/Data/ArrayType/Algebra.lean
+++ b/SciLean/Data/ArrayType/Algebra.lean
@@ -238,5 +238,5 @@ instance [ArrayType Cont Idx Elem] [MeasureSpace Elem] : MeasureSpace Cont where
     mono := sorry_proof
     iUnion_nat := sorry_proof
     m_iUnion := sorry_proof
-    trimmed := sorry_proof
+    trim_le := sorry_proof
 }
diff --git a/SciLean/Data/ArrayType/Notation.lean b/SciLean/Data/ArrayType/Notation.lean
index a1b851a4..a7c40fd9 100644
--- a/SciLean/Data/ArrayType/Notation.lean
+++ b/SciLean/Data/ArrayType/Notation.lean
@@ -1,6 +1,6 @@
 import SciLean.Data.ArrayType.Basic
 import SciLean.Data.ListN
-import Std.Lean.Expr
+import Batteries.Lean.Expr
 import Qq
 
 
diff --git a/SciLean/Data/ArrayType/Properties.lean b/SciLean/Data/ArrayType/Properties.lean
index 549ae662..f8f49f17 100644
--- a/SciLean/Data/ArrayType/Properties.lean
+++ b/SciLean/Data/ArrayType/Properties.lean
@@ -97,6 +97,7 @@ by
   unfold revDeriv;
   conv =>
     lhs; fun_trans; fun_trans; simp
+  rfl
 
 @[fun_trans]
 theorem GetElem.getElem.arg_cont.revCDerivUpdate_rule
@@ -112,6 +113,7 @@ by
   unfold revDerivUpdate;
   conv =>
     lhs; fun_trans; fun_trans; simp
+  rfl
 
 @[fun_trans]
 theorem GetElem.getElem.arg_cont.revCDerivProj_rule
@@ -218,6 +220,7 @@ theorem LeanColls.Indexed.set.arg_contelem.revCDeriv_rule
   unfold revDeriv;
   conv =>
     lhs; fun_trans; fun_trans; simp
+  rfl
 
 @[fun_trans]
 theorem LeanColls.Indexed.set.arg_contelem.revCDerivUpdate_rule
@@ -391,6 +394,7 @@ theorem LeanColls.Indexed.ofFn.arg_cont.revCDerivUpdate_rule
 by
   unfold revDerivUpdate;
   conv => lhs; fun_trans; simp
+  rfl
 
 @[fun_trans]
 theorem LeanColls.Indexed.ofFn.arg_cont.revCDerivProj_rule
@@ -416,6 +420,7 @@ theorem LeanColls.Indexed.ofFn.arg_cont.revCDerivProjUpdate_rule
        fdf.2) := by
   unfold revDerivProjUpdate;
   conv => lhs; fun_trans; simp
+  rfl
 
 end OnSemiInnerProductSpace
 
diff --git a/SciLean/Data/IndexType.lean b/SciLean/Data/IndexType.lean
index c54f9a40..c538c780 100644
--- a/SciLean/Data/IndexType.lean
+++ b/SciLean/Data/IndexType.lean
@@ -32,11 +32,7 @@ instance (a b : Int) : LawfulIndexType (Icc a b) where
   leftInv := by
     intro x
     simp only [IndexType.toFin, IndexType.fromFin]
-    unhygienic
-      with_reducible
-        aesop_destruct_products
-    simp_all only [Subtype.mk.injEq]
-    simp_all only [mem_Icc, sub_nonneg, Int.toNat_of_nonneg, add_sub_cancel]
+    sorry_proof
   rightInv := by
     intro x
     simp only [IndexType.toFin, IndexType.fromFin, add_sub_cancel_left, Int.toNat_ofNat, Fin.eta]
@@ -140,7 +136,7 @@ def argMax {I} [IndexType.{_,0} I] [Inhabited I]
   Fold.fold (β:=α) (C:=IndexType.Univ ι) (τ:=ι) (IndexType.univ ι) (fun (s : α) (i : ι) => s + f i) (0 : α)
 
 open Lean.TSyntax.Compat in
-macro " ∑ " xs:Lean.explicitBinders ", " b:term:66 : term => Lean.expandExplicitBinders ``sum xs b
+macro (priority:=high) " ∑ " xs:Lean.explicitBinders ", " b:term:66 : term => Lean.expandExplicitBinders ``sum xs b
 
 @[app_unexpander sum] def unexpandSum : Lean.PrettyPrinter.Unexpander
   | `($(_) fun $x:ident => $b) =>
diff --git a/SciLean/Lean/Array.lean b/SciLean/Lean/Array.lean
index a0d6cf78..e8365d02 100644
--- a/SciLean/Lean/Array.lean
+++ b/SciLean/Lean/Array.lean
@@ -1,4 +1,3 @@
-import Std.Logic
 import SciLean.Util.SorryProof
 
 namespace Array
@@ -66,7 +65,7 @@ def joinl [Inhabited β] (xs : Array α) (map : α → β) (op : β → β → 
   xs.joinlM map op
 
 def joinrM [Monad m] [Inhabited β] (xs : Array α) (map : α → m β) (op : β → β → m β) : m β := do
-  if h : 0 < xs.size then
+  if _h : 0 < xs.size then
     let n := xs.size - 1
     have : n < xs.size := sorry_proof
     xs[0:n].foldrM (init:=(← map xs[n])) λ x acc => do op (← map x) acc
diff --git a/SciLean/Lean/Expr.lean b/SciLean/Lean/Expr.lean
index 6a38f10e..f8f3e2c2 100644
--- a/SciLean/Lean/Expr.lean
+++ b/SciLean/Lean/Expr.lean
@@ -1,8 +1,8 @@
 import Lean
 import Qq
-import Std.Lean.Expr
+import Batteries.Lean.Expr
 import Mathlib.Lean.Expr
-import Mathlib.Tactic.FunProp.ToStd
+import Mathlib.Tactic.FunProp.ToBatteries
 
 namespace Lean.Expr
 
diff --git a/SciLean/Lean/MergeMapDeclarationExtension.lean b/SciLean/Lean/MergeMapDeclarationExtension.lean
index 36882f31..350352d5 100644
--- a/SciLean/Lean/MergeMapDeclarationExtension.lean
+++ b/SciLean/Lean/MergeMapDeclarationExtension.lean
@@ -1,5 +1,5 @@
-
-import Std.Data.RBMap.Alter
+import Batteries.Data.RBMap.Alter
+import Lean
 import SciLean.Lean.Array
 
 open Lean
@@ -18,7 +18,7 @@ Similar to `MapDeclarationExtension` but it allows you have insert declarations
 However, you have to provide how to merge the values and to guarantee consistency i.e. merging should be associative and commutative.
 -/
 def MergeMapDeclarationExtension (α)
-  := PersistentEnvExtension (Name × α) (Name × α) (Std.RBMap Name α Name.quickCmp)
+  := PersistentEnvExtension (Name × α) (Name × α) (Batteries.RBMap Name α Name.quickCmp)
 
 open MergeMapDeclarationExtension in
 def mkMergeMapDeclarationExtension [Inhabited α] (merge : Merge α) (name : Name := by exact decl_name%)
diff --git a/SciLean/Lean/Meta/Basic.lean b/SciLean/Lean/Meta/Basic.lean
index f94b6159..6df7c3ed 100644
--- a/SciLean/Lean/Meta/Basic.lean
+++ b/SciLean/Lean/Meta/Basic.lean
@@ -1,5 +1,5 @@
 import Lean
-import Std.Lean.Expr
+import Batteries.Lean.Expr
 
 import SciLean.Lean.Expr
 import SciLean.Lean.Array
@@ -196,7 +196,7 @@ def mkUncurryFun (n : Nat) (f : Expr) (mk := ``Prod.mk) (fst := ``Prod.fst) (snd
   forallTelescope (← inferType f) λ xs _ => do
     let xs := xs[0:n]
 
-    let xProdName : String ← xs.foldlM (init:="") λ n x =>
+    let xProdName := Name.mkSimple <| ← xs.foldlM (init:="") λ n x =>
       do return (n ++ toString (← x.fvarId!.getUserName).eraseMacroScopes)
     let xProdType ← inferType (← mkProdElem xs mk)
 
diff --git a/SciLean/Mathlib/Set.lean b/SciLean/Mathlib/Set.lean
index 0706984f..893bf119 100644
--- a/SciLean/Mathlib/Set.lean
+++ b/SciLean/Mathlib/Set.lean
@@ -4,11 +4,9 @@ import SciLean.Tactic.FTrans.Simp
 
 
 /-- Take a slice of a set in the first component. -/
-@[pp_dot]
 def Set.fst (A : Set (α×β)) (b : β) : Set α := {x | (x,b) ∈ A}
 
 /-- Take a slice of a set in the second component. -/
-@[pp_dot]
 def Set.snd (A : Set (α×β)) (a : α) : Set β := {y | (a,y) ∈ A}
 
 
diff --git a/SciLean/Meta/DerivingOp.lean b/SciLean/Meta/DerivingOp.lean
index 5548a665..1e8b7a70 100644
--- a/SciLean/Meta/DerivingOp.lean
+++ b/SciLean/Meta/DerivingOp.lean
@@ -19,13 +19,13 @@ def mkBinaryOpInstance (className opName : Name) (declName : Name) : TermElabM U
         let mut fields := #[]
         for i in [0:info.fieldNames.size] do
           fields := fields.push (← Meta.mkAppM opName #[x.proj info.structName i, y.proj info.structName i])
-        (Meta.mkLambdaFVars #[x,y] (← Meta.mkAppM (info.structName.append "mk") fields))
+        (Meta.mkLambdaFVars #[x,y] (← Meta.mkAppM (info.structName.append `mk) fields))
 
-      Meta.mkLambdaFVars xs (← Meta.mkAppM (className.append "mk") #[binOp])
+      Meta.mkLambdaFVars xs (← Meta.mkAppM (className.append `mk) #[binOp])
 
     let instType ← Meta.inferType instValue
 
-    let instName : Name := declName.append "instances" |>.append className
+    let instName : Name := declName.append `instances |>.append className
     let instDecl : Declaration := .defnDecl
       {levelParams := [],
        hints := .regular 0,
@@ -35,7 +35,7 @@ def mkBinaryOpInstance (className opName : Name) (declName : Name) : TermElabM U
        name := instName,
        }
     addAndCompile instDecl
-    Attribute.add instName "instance" default
+    Attribute.add instName `instance default
   | none =>
     pure default
 
@@ -60,13 +60,13 @@ def mkUnaryOpInstance (className opName : Name) (declName : Name) : TermElabM Un
         let mut fields := #[]
         for i in [0:info.fieldNames.size] do
           fields := fields.push (← Meta.mkAppM opName #[x.proj info.structName i])
-        (Meta.mkLambdaFVars #[x] (← Meta.mkAppM (info.structName.append "mk") fields))
+        (Meta.mkLambdaFVars #[x] (← Meta.mkAppM (info.structName.append `mk) fields))
 
-      Meta.mkLambdaFVars xs (← Meta.mkAppM (className.append "mk") #[op])
+      Meta.mkLambdaFVars xs (← Meta.mkAppM (className.append `mk) #[op])
 
     let instType ← Meta.inferType instValue
 
-    let instName : Name := declName.append "instances" |>.append className
+    let instName : Name := declName.append `instances |>.append className
     let instDecl : Declaration := .defnDecl
       {levelParams := [],
        hints := .regular 0,
@@ -76,7 +76,7 @@ def mkUnaryOpInstance (className opName : Name) (declName : Name) : TermElabM Un
        name := instName,
        }
     addAndCompile instDecl
-    Attribute.add instName "instance" default
+    Attribute.add instName `instance default
   | none =>
     pure default
 
@@ -100,13 +100,13 @@ def mkNullaryOpInstance (className opName : Name) (declName : Name) : TermElabM
         let mut fields := #[]
         for i in [0:info.fieldNames.size] do
           fields := fields.push (← Meta.mkAppOptM opName #[← Meta.inferType (x.proj info.structName i),none])
-        Meta.mkAppM (info.structName.append "mk") fields
+        Meta.mkAppM (info.structName.append `mk) fields
 
-      Meta.mkLambdaFVars xs (← Meta.mkAppM (className.append "mk") #[op])
+      Meta.mkLambdaFVars xs (← Meta.mkAppM (className.append `mk) #[op])
 
     let instType ← Meta.inferType instValue
 
-    let instName : Name := declName.append "instances" |>.append className
+    let instName : Name := declName.append `instances |>.append className
     let instDecl : Declaration := .defnDecl
       {levelParams := [],
        hints := .regular 0,
@@ -116,7 +116,7 @@ def mkNullaryOpInstance (className opName : Name) (declName : Name) : TermElabM
        name := instName,
        }
     addAndCompile instDecl
-    Attribute.add instName "instance" default
+    Attribute.add instName `instance default
   | none =>
     pure default
 
@@ -142,13 +142,13 @@ def mkSMulOpInstance (declName : Name) : TermElabM Unit := do
         let mut fields := #[]
         for i in [0:info.fieldNames.size] do
           fields := fields.push (← Meta.mkAppM ``SMul.smul #[s, x.proj info.structName i])
-        (Meta.mkLambdaFVars #[s,x] (← Meta.mkAppM (info.structName.append "mk") fields))
+        (Meta.mkLambdaFVars #[s,x] (← Meta.mkAppM (info.structName.append `mk) fields))
 
       Meta.mkLambdaFVars xs (← Meta.mkAppM ``SMul.mk #[binOp])
 
     let instType ← Meta.inferType instValue
 
-    let instName : Name := declName.append "instances" |>.append "SMul"
+    let instName : Name := declName.append `instances |>.append `SMul
     let instDecl : Declaration := .defnDecl
       {levelParams := [],
        hints := .regular 0,
@@ -157,7 +157,7 @@ def mkSMulOpInstance (declName : Name) : TermElabM Unit := do
        value := instValue,
        name := instName}
     addAndCompile instDecl
-    Attribute.add instName "instance" default
+    Attribute.add instName `instance default
   | none =>
     pure default
 
diff --git a/SciLean/Modules/PhysicalUnits/PhysicalUnits.lean b/SciLean/Modules/PhysicalUnits/PhysicalUnits.lean
index c69e26a3..81730da9 100644
--- a/SciLean/Modules/PhysicalUnits/PhysicalUnits.lean
+++ b/SciLean/Modules/PhysicalUnits/PhysicalUnits.lean
@@ -1,5 +1,5 @@
 import Lean
-import Std
+import Batteries
 import Qq
 import Mathlib.Data.Real.Basic
 import Mathlib.Tactic.NormNum
diff --git a/SciLean/Modules/Prob/Erased.lean b/SciLean/Modules/Prob/Erased.lean
index bfac8c35..3afd896a 100644
--- a/SciLean/Modules/Prob/Erased.lean
+++ b/SciLean/Modules/Prob/Erased.lean
@@ -1,4 +1,4 @@
-import Std
+import Batteries
 
 structure Erased (α : Type) : Type where
   spec : α → Prop
diff --git a/SciLean/Tactic/ConvInduction.lean b/SciLean/Tactic/ConvInduction.lean
index 4be716a2..3d1ee211 100644
--- a/SciLean/Tactic/ConvInduction.lean
+++ b/SciLean/Tactic/ConvInduction.lean
@@ -51,7 +51,6 @@ syntax (name:=conv_induction) "induction" ident (ident)? (ident)? (ident)? conv
 
 syntax (name:=conv_induction_list) "induction_list" ident (ident)? (ident)? (ident)? (ident)? conv conv : conv
 
-#check List.recOn
 @[tactic conv_induction_list] def convInductionList : Tactic
 | `(conv| induction_list $n $[$head]? $[$tail]? $[$prev]? $[$eq]? $baseConv $succConv) => do
   let mvarId ← getMainGoal
diff --git a/SciLean/Tactic/FTrans/Basic.lean b/SciLean/Tactic/FTrans/Basic.lean
index f7ab2309..a51b5fdf 100644
--- a/SciLean/Tactic/FTrans/Basic.lean
+++ b/SciLean/Tactic/FTrans/Basic.lean
@@ -1,4 +1,4 @@
-import Std.Lean.Parser
+import Batteries.Lean.Parser
 import Mathlib.Tactic.NormNum.Core
 
 import SciLean.Lean.Meta.Basic
diff --git a/SciLean/Tactic/FTrans/Init.lean b/SciLean/Tactic/FTrans/Init.lean
index 1d7c3a65..c14ddfd5 100644
--- a/SciLean/Tactic/FTrans/Init.lean
+++ b/SciLean/Tactic/FTrans/Init.lean
@@ -1,7 +1,7 @@
 import Qq
 import Lean.Meta.Tactic.Simp.Types
 
-import Std.Data.RBMap.Alter
+import Batteries.Data.RBMap.Alter
 
 import Mathlib.Data.FunLike.Basic
 
@@ -128,12 +128,12 @@ def mkFTransExt (n : Name) : ImportM FTransExt := do
   IO.ofExcept <| unsafe env.evalConstCheck FTransExt opts ``FTransExt n
 
 
-initialize ftransExt : PersistentEnvExtension (Name × Name) (Name × FTransExt) (Std.RBMap Name FTransExt Name.quickCmp) ←
+initialize ftransExt : PersistentEnvExtension (Name × Name) (Name × FTransExt) (Batteries.RBMap Name FTransExt Name.quickCmp) ←
   registerPersistentEnvExtension {
     mkInitial := pure {}
     addImportedFn := fun s => do
 
-      let mut r : Std.RBMap Name FTransExt Name.quickCmp := {}
+      let mut r : Batteries.RBMap Name FTransExt Name.quickCmp := {}
 
       for s' in s do
         for (ftransName, extName) in s' do
@@ -230,7 +230,7 @@ local instance : Ord Name := ⟨Name.quickCmp⟩
 /--
 This holds a collection of function transformation rules for a fixed constant
 -/
-def FTransRules := Std.RBMap Name (Std.RBSet FTransRule FTransRule.cmp) compare
+def FTransRules := Batteries.RBMap Name (Batteries.RBSet FTransRule FTransRule.cmp) compare
 
 namespace FTransRules
 
@@ -243,9 +243,9 @@ namespace FTransRules
     fp.alter ftransName (λ p? =>
       match p? with
       | some p => some (p.insert rule)
-      | none => some (Std.RBSet.empty.insert rule))
+      | none => some (Batteries.RBSet.empty.insert rule))
 
-  def empty : FTransRules := Std.RBMap.empty
+  def empty : FTransRules := Batteries.RBMap.empty
 
 end FTransRules
 
@@ -293,8 +293,8 @@ where <name> is name of the function transformation and <info> is corresponding
 
           let suggestedRuleName :=
             data.constName
-              |>.append data.declSuffix
-              |>.append (transName.getString.append "_rule")
+              |>.append (.mkSimple data.declSuffix)
+              |>.append (.mkSimple (transName.lastComponentAsString.append "_rule"))
 
           if (← getBoolOption `linter.ftransDeclName) &&
              ¬(suggestedRuleName.toString.isPrefixOf ruleName.toString) then
diff --git a/SciLean/Tactic/FunTrans/Attr.lean b/SciLean/Tactic/FunTrans/Attr.lean
new file mode 100644
index 00000000..23d66d08
--- /dev/null
+++ b/SciLean/Tactic/FunTrans/Attr.lean
@@ -0,0 +1,42 @@
+/-
+Copyright (c) 2024 Tomas Skrivan. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Tomas Skrivan
+-/
+import Lean
+
+import SciLean.Tactic.FunTrans.Decl
+import SciLean.Tactic.FunTrans.Theorems
+
+/-!
+## `funTrans` attribute
+-/
+
+
+namespace Mathlib
+open Lean Meta
+
+namespace Meta.FunTrans
+
+
+private def funTransHelpString : String :=
+"`funTrans` tactic to compute function transformations like `fderiv` or `adjoint`"
+
+/-- Initialization of `funTrans` attribute -/
+initialize funTransAttr : Unit ←
+  registerBuiltinAttribute {
+    name  := `fun_trans
+    descr := funTransHelpString
+    applicationTime := AttributeApplicationTime.afterCompilation
+    add   := fun declName _stx attrKind =>
+       discard <| MetaM.run do
+       let info ← getConstInfo declName
+
+       forallTelescope info.type fun _ b => do
+         if b.isEq then
+           addTheorem declName attrKind
+         else
+           addFunTransDecl declName
+    erase := fun _declName =>
+      throwError "can't remove `funTrans` attribute (not implemented yet)"
+  }
diff --git a/SciLean/Tactic/FunTrans/Core.lean b/SciLean/Tactic/FunTrans/Core.lean
new file mode 100644
index 00000000..73092393
--- /dev/null
+++ b/SciLean/Tactic/FunTrans/Core.lean
@@ -0,0 +1,605 @@
+/-
+Copyright (c) 2024 Tomas Skrivan. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Tomas Skrivan
+-/
+import Lean
+import Qq
+import Batteries.Tactic.Exact
+
+import SciLean.Tactic.FunTrans.Theorems
+import SciLean.Tactic.FunTrans.Types
+import Mathlib.Tactic.FunProp.Core
+import Mathlib.Tactic.FunProp.Types
+
+/-!
+## `funTrans` core tactic algorithm
+-/
+
+namespace Mathlib
+open Lean Meta Qq
+
+namespace Meta.FunTrans
+
+def runFunProp (e : Expr) : SimpM (Option Expr) := do
+  let cache := (← get).cache
+  modify (fun s => { s with cache := {}}) -- hopefully this prevent duplicating the cache
+  let config : FunProp.Config := (← funTransConfig.get).funPropConfig
+  let state  : FunProp.State := { cache := cache }
+  let (result?, state) ← FunProp.funProp e |>.run config state
+  modify (fun simpState => { simpState with cache := state.cache })
+
+  match result? with
+  | .some r => return r.proof
+  | .none => return .none
+
+
+private def ppOrigin' (origin : FunProp.Origin) : MetaM String := do
+  match origin with
+  | .fvar id => return s!"{← ppExpr (.fvar id)} : {← ppExpr (← inferType (.fvar id))}"
+  | _ => pure (toString origin.name)
+
+
+-- TODO: remove this once updated to newer version of mathlib
+/-- Is `e` a `fun_prop` goal? For example `∀ y z, Continuous fun x => f x y z` -/
+private def FunProp.isFunPropGoal (e : Expr) : MetaM Bool := do
+  forallTelescope e fun _ b =>
+  return (← FunProp.getFunProp? b).isSome
+
+
+def synthesizeArgs (thmId : FunProp.Origin) (xs : Array Expr) : SimpM Bool := do
+  let mut postponed : Array Expr := #[]
+  for x in xs do
+    let type ← inferType x
+    if (← instantiateMVars x).isMVar then
+      -- A hypothesis can be both a type class instance as well as a proposition,
+      -- in that case we try both TC synthesis and the discharger
+      -- (because we don't know whether the argument was originally explicit or instance-implicit).
+      if (← isClass? type).isSome then
+        if (← synthesizeInstance x type) then
+          continue
+
+      if (← isProp type) then
+        if ← FunProp.isFunPropGoal type then
+          if let .some r ← runFunProp type then
+            x.mvarId!.assignIfDefeq r
+            continue
+        else
+          let disch := (← funTransConfig.get).funPropConfig.disch
+          if let .some r ← disch type then
+            x.mvarId!.assignIfDefeq r
+            continue
+
+      if ¬(← isProp type) then
+        postponed := postponed.push x
+        continue
+      else
+        trace[Meta.Tactic.fun_trans]
+          "{← ppOrigin' thmId}, failed to discharge hypotheses{indentExpr type}"
+        return false
+
+  for x in postponed do
+    if (← instantiateMVars x).isMVar then
+      trace[Meta.Tactic.fun_trans]
+        "{← ppOrigin' thmId}, failed to infer `({← ppExpr x} : {← ppExpr (← inferType x)})`"
+      return false
+
+  return true
+where
+  synthesizeInstance (x type : Expr) : SimpM Bool := do
+    match (← trySynthInstance type) with
+    | LOption.some val =>
+      if (← withReducibleAndInstances <| isDefEq x val) then
+        return true
+      else
+        trace[Meta.Tactic.fun_trans.discharge] "{← ppOrigin' thmId}, failed to assign instance{indentExpr type}\nsythesized value{indentExpr val}\nis not definitionally equal to{indentExpr x}"
+        return false
+    | _ =>
+      trace[Meta.Tactic.fun_trans.discharge] "{← ppOrigin' thmId}, failed to synthesize instance{indentExpr type}"
+      return false
+
+
+
+def tryTheoremCore (lhs : Expr) (xs : Array Expr) (val : Expr) (type : Expr) (e : Expr) (thmId : FunProp.Origin) : SimpM (Option Simp.Result) := do
+  withTraceNode `Meta.Tactic.fun_trans
+    (fun r => return s!"[{ExceptToEmoji.toEmoji r}] applying: {← ppOrigin' thmId}") do
+
+  unless (← isDefEq lhs (← instantiateMVars e)) do
+    trace[Meta.Tactic.fun_trans.unify] "failed to unify {← ppOrigin' thmId}\n{lhs}\nwith\n{e}"
+    return none
+
+  if ¬(← synthesizeArgs thmId xs) then
+    return none
+
+  let proof ← instantiateMVars (mkAppN val xs)
+  let rhs := (← instantiateMVars type).appArg!
+  if e == rhs then
+    return none
+  trace[Meta.Tactic.fun_trans] "{← ppOrigin' thmId}, \n{e}\n==>\n{rhs}"
+  return .some { expr := rhs, proof? := proof }
+
+
+def tryTheoremWithHint (e : Expr) (thmOrigin : FunProp.Origin) (hint : Array (Nat × Expr)) : SimpM (Option Simp.Result) := do
+
+  let proof ← thmOrigin.getValue
+  let type ← instantiateMVars (← inferType proof)
+  let (xs, _, type) ← forallMetaTelescope type
+  let .some (_,lhs,_) := type.eq?
+    | throwError "fun_trans bug: applying theorem {← ppExpr type} that is not an equality"
+
+  try
+    for (id,v) in hint do
+      xs[id]!.mvarId!.assignIfDefeq v
+  catch _ =>
+    trace[Meta.Tactic.fun_trans.discharge]  "failed to use `{← FunProp.ppOrigin thmOrigin}` on `{e}`"
+    return .none
+
+  let extraArgsNum := e.getAppNumArgs - lhs.getAppNumArgs
+  let e' := e.stripArgsN extraArgsNum
+  let extraArgs := e.getAppArgsN extraArgsNum
+  let .some r ← tryTheoremCore lhs xs proof type e' thmOrigin | return .none
+  return (← r.addExtraArgs extraArgs)
+
+
+def tryTheorem? (e : Expr) (thmOrigin : FunProp.Origin) : SimpM (Option Simp.Result) :=
+  tryTheoremWithHint e thmOrigin #[]
+
+
+def applyIdRule (funTransDecl : FunTransDecl) (e X : Expr) : SimpM (Option Simp.Result) := do
+  trace[Meta.Tactic.fun_trans.step] "id case"
+
+  let .some thms ← getLambdaTheorems funTransDecl.funTransName .id e.getAppNumArgs
+    | trace[Meta.Tactic.fun_trans] "missing identity rule to transform `{← ppExpr e}`"
+      return none
+
+  for thm in thms do
+    let .id id_X := thm.thmArgs | continue
+
+    if let .some r ← tryTheoremWithHint e (.decl thm.thmName) #[(id_X,X)] then
+      return r
+
+  return none
+
+def applyConstRule (funTransDecl : FunTransDecl) (e : Expr) : SimpM (Option Simp.Result) := do
+  let .some thms ← getLambdaTheorems funTransDecl.funTransName .const e.getAppNumArgs
+    | trace[Meta.Tactic.fun_trans] "missing const rule to transform `{← ppExpr e}`"
+      return none
+
+  for thm in thms do
+    let .const := thm.thmArgs | continue
+
+    if let .some r ← tryTheoremWithHint e (.decl thm.thmName) #[] then
+      return r
+
+  return none
+
+
+
+def applyCompRule (funTransDecl : FunTransDecl) (e f g : Expr) : SimpM (Option Simp.Result) := do
+  let .some thms ← getLambdaTheorems funTransDecl.funTransName .comp e.getAppNumArgs
+    | trace[Meta.Tactic.fun_trans] "missing comp rule to transform `{← ppExpr e}`"
+      return none
+
+  for thm in thms do
+    let .comp id_f id_g := thm.thmArgs | continue
+    trace[Meta.Tactic.fun_trans] "trying comp theorem {thm.thmName}"
+    if let .some r ← tryTheoremWithHint e (.decl thm.thmName) #[(id_f,f),(id_g,g)] then
+      return r
+
+  return none
+
+def applyLetRule (funTransDecl : FunTransDecl) (e f g : Expr) : SimpM (Option Simp.Result) := do
+  let .some thms ← getLambdaTheorems funTransDecl.funTransName .letE e.getAppNumArgs
+    | trace[Meta.Tactic.fun_trans] "missing let rule to transform `{← ppExpr e}`"
+      return none
+
+  for thm in thms do
+    let .letE id_f id_g := thm.thmArgs | continue
+
+    if let .some r ← tryTheoremWithHint e (.decl thm.thmName) #[(id_f,f),(id_g,g)] then
+      return r
+
+  return none
+
+def applyApplyRule (funTransDecl : FunTransDecl) (e x XY : Expr) : SimpM (Option Simp.Result) := do
+  let ext := lambdaTheoremsExt.getState (← getEnv)
+  let .forallE n X Y _ := XY | return none
+
+  -- non dependent case
+  if ¬(Y.hasLooseBVars) then
+    if let .some thms := ext.theorems.find? (funTransDecl.funTransName, .proj) then
+      for thm in thms do
+        let .proj id_x id_Y := thm.thmArgs | return none
+        if let .some r ← tryTheoremWithHint e (.decl thm.thmName) #[(id_x,x),(id_Y,Y)] then
+          return r
+
+  -- dependent case
+  -- can also handle non-dependent cases if non-dependent theorem is not available
+  let Y := Expr.lam n X Y default
+
+  let .some thms := ext.theorems.find? (funTransDecl.funTransName, .projDep)
+    | trace[Meta.Tactic.fun_trans]
+        "missing projection rule to transform `{← ppExpr e}`"
+      return none
+  for thm in thms do
+    let .projDep id_x id_Y := thm.thmArgs | return none
+
+    if let .some r ← tryTheoremWithHint e (.decl thm.thmName) #[(id_x,x),(id_Y,Y)] then
+      return r
+
+  return none
+
+def applyApplyDepRule (funTransDecl : FunTransDecl) (e x Y : Expr) : SimpM (Option Simp.Result) := do
+  let .some thms ← getLambdaTheorems funTransDecl.funTransName .projDep e.getAppNumArgs
+    | trace[Meta.Tactic.fun_trans] "missing projDep rule to transform `{← ppExpr e}`"
+      return none
+
+  for thm in thms do
+    let .projDep id_x id_Y := thm.thmArgs | continue
+
+    if let .some r ← tryTheoremWithHint e (.decl thm.thmName) #[(id_x,x),(id_Y,Y)] then
+      return r
+
+  return none
+
+def applyPiRule (funTransDecl : FunTransDecl) (e f : Expr) : SimpM (Option Simp.Result) := do
+  let .some thms ← getLambdaTheorems funTransDecl.funTransName .pi e.getAppNumArgs
+    | trace[Meta.Tactic.fun_trans] "missing pi rule to transform `{← ppExpr e}`"
+      return none
+
+  for thm in thms do
+    let .pi id_f := thm.thmArgs | continue
+
+    if let .some r ← tryTheoremWithHint e (.decl thm.thmName) #[(id_f,f)] then
+      return r
+
+  return none
+
+
+
+def applyMorTheorems (funTransDecl : FunTransDecl) (e : Expr) (fData : FunProp.FunctionData) : SimpM (Option Simp.Result) := do
+
+  match ← fData.isMorApplication with
+  | .none => return none
+  | .underApplied =>
+    applyPiRule funTransDecl e (← fData.toExpr)
+  | .overApplied =>
+    let .some (f,g) ← fData.peeloffArgDecomposition | return none
+    applyCompRule funTransDecl e f g
+  | .exact =>
+    let ext := (morTheoremsExt.getState (← getEnv))
+
+    let candidates ← ext.theorems.getMatchWithScoreWithExtra e false { iota := false, zeta := false }
+    let candidates := candidates.map (·.1) |>.flatten
+
+    trace[Meta.Tactic.fun_trans]
+      "candidate morphism theorems: {← candidates.mapM fun c => ppOrigin (.decl c.thmName)}"
+
+    for c in candidates do
+      if let .some r ← tryTheoremWithHint e (.decl c.thmName) #[] then
+        return r
+
+    return none
+
+def applyFVarTheorems (e : Expr) : SimpM (Option Simp.Result) := do
+
+  let ext := (fvarTheoremsExt.getState (← getEnv))
+
+  let candidates ← ext.theorems.getMatchWithScoreWithExtra e false { iota := false, zeta := false }
+  let candidates := candidates.map (·.1) |>.flatten
+
+  trace[Meta.Tactic.fun_trans]
+    "candidate fvar theorems: {← candidates.mapM fun c => ppOrigin (.decl c.thmName)}"
+
+  for c in candidates do
+    if let .some r ← tryTheoremWithHint e (.decl c.thmName) #[] then
+      return .some r
+
+  return none
+
+def getLocalTheorems (funTransDecl : FunTransDecl) (funOrigin : FunProp.Origin)
+    (mainArgs : Array Nat) (appliedArgs : Nat) : MetaM (Array FunctionTheorem) := do
+
+  let mut thms : Array FunctionTheorem := #[]
+  let lctx ← getLCtx
+  for var in lctx do
+    if (var.kind = Lean.LocalDeclKind.auxDecl) then
+      continue
+    let type ← instantiateMVars var.type
+    let thm? : Option FunctionTheorem ←
+      forallTelescope type fun _ b => do
+      let b ← whnfR b
+      let .some (_,lhs,_) := b.eq? | return none
+      let .some (decl,f) ← getFunTrans? lhs | return none
+      unless decl.funTransName = funTransDecl.funTransName do return none
+
+      let .data fData ← FunProp.getFunctionData? f FunProp.defaultUnfoldPred | return none
+      unless (fData.getFnOrigin == funOrigin) do return none
+
+      unless FunProp.isOrderedSubsetOf mainArgs fData.mainArgs do return none
+
+      let dec? ← fData.nontrivialDecomposition
+
+      let thm : FunctionTheorem := {
+        funTransName := funTransDecl.funTransName
+        transAppliedArgs := lhs.getAppNumArgs
+        thmOrigin := .fvar var.fvarId
+        funOrigin := funOrigin
+        mainArgs := fData.mainArgs
+        appliedArgs := fData.args.size
+        priority := eval_prio default
+        form := if dec?.isSome then .comp else .uncurried
+      }
+
+      return .some thm
+
+    if let .some thm := thm? then
+      thms := thms.push thm
+
+  thms := thms
+    |>.qsort (fun t s =>
+      let dt := (Int.ofNat t.appliedArgs - Int.ofNat appliedArgs).natAbs
+      let ds := (Int.ofNat s.appliedArgs - Int.ofNat appliedArgs).natAbs
+      match compare dt ds with
+      | .lt => true
+      | .gt => false
+      | .eq => t.mainArgs.size < s.mainArgs.size)
+
+  return thms
+
+
+def tryTheorems (funTransDecl : FunTransDecl) (e : Expr) (fData : FunProp.FunctionData)
+    (thms : Array FunctionTheorem) : SimpM (Option Simp.Result) := do
+  -- none - decomposition not tried
+  -- some none - decomposition failed
+  -- some some (f, g) - succesfull decomposition
+  let mut dec? : Option (Option (Expr × Expr)) := none
+
+  for thm in thms do
+
+    trace[Meta.Tactic.fun_trans.step] s!"trying theorem {← ppOrigin' thm.thmOrigin}"
+
+    match compare thm.appliedArgs fData.args.size with
+    | .lt =>
+      trace[Meta.Tactic.fun_trans] s!"removing argument to later use {← ppOrigin' thm.thmOrigin}"
+      trace[Meta.Tactic.fun_trans] s!"NOT IMPLEMENTED"
+      -- if let .some r ← removeArgRule funTransDecl e fData funTrans then
+      --   return r
+      return none
+    | .gt =>
+      trace[Meta.Tactic.fun_trans] s!"adding argument to later use {← ppOrigin' thm.thmOrigin}"
+      if let .some r ← applyPiRule funTransDecl e (← fData.toExpr) then
+        return r
+      continue
+    | .eq =>
+      if thm.form == .comp then
+        if let .some r ← tryTheorem? e thm.thmOrigin then
+          return r
+      else
+
+        if thm.mainArgs.size == fData.mainArgs.size then
+          if dec?.isNone then
+            dec? := .some (← fData.nontrivialDecomposition)
+          match dec? with
+          | .some .none =>
+            if let .some r ← tryTheorem? e thm.thmOrigin then
+              return r
+          | .some (.some (f,g)) =>
+            trace[Meta.Tactic.fun_trans.step]
+              s!"decomposing to later use {←ppOrigin' thm.thmOrigin}"
+            if let .some r ← applyCompRule funTransDecl e f g then
+              return r
+          | _ => continue
+        else
+          trace[Meta.Tactic.fun_trans.step]
+            s!"decomposing in args {thm.mainArgs} to later use {←ppOrigin' thm.thmOrigin}"
+          let .some (f,g) ← fData.decompositionOverArgs thm.mainArgs
+            | continue
+          trace[Meta.Tactic.fun_trans.step]
+            s!"decomposition: {← ppExpr f} ∘ {← ppExpr g}"
+          if let .some r ← applyCompRule funTransDecl e f g then
+            return r
+  return none
+
+
+def letCase (funTransDecl : FunTransDecl) (e f : Expr) : SimpM (Option Simp.Result) := do
+  trace[Meta.Tactic.fun_trans.step] "let case"
+
+  let .lam xName xType (.letE yName yType yVal yBody _) xBi := f | return none
+
+  match (yBody.hasLooseBVar 0), (yBody.hasLooseBVar 1) with
+  | true, true =>
+
+    let f := Expr.lam xName xType (.lam yName yType yBody .default) xBi
+    let g := Expr.lam xName xType yVal .default
+
+    applyLetRule funTransDecl e f g
+  | true, false =>
+    let f := Expr.lam yName yType yBody default
+    let g := Expr.lam xName xType yVal default
+
+    applyCompRule funTransDecl e f g
+
+  | false, _ =>
+    let f := Expr.lam xName xType (yBody.lowerLooseBVars 1 1) xBi
+    let e' := e.setArg (funTransDecl.funArgId) f
+
+    return .some ({expr := e'})
+
+
+
+def bvarAppCase (funTransDecl : FunTransDecl) (e : Expr) (fData : FunProp.FunctionData) : SimpM (Option Simp.Result) := do
+  trace[Meta.Tactic.fun_trans.step] "bvar app case"
+
+  if (← fData.isMorApplication) != .none then
+    applyMorTheorems funTransDecl e fData
+  else
+    if let .some (f, g) ← fData.nontrivialDecomposition then
+      applyCompRule funTransDecl e f g
+    else
+      applyApplyRule funTransDecl e fData.args[0]!.expr (← fData.domainType)
+
+  -- if let .some (f,g) ← fData.nontrivialDecomposition then
+  --   return ← applyCompRule funTransDecl e f g
+  -- else
+  --   if fData.args.size = 1 then
+  --     let x := fData.args[0]!
+  --     if x.coe.isSome then
+  --       trace[Meta.Tactic.fun_trans.step] "morphism apply case"
+  --       if let .some r ← applyMorTheorems funTransDecl e fData then
+  --         return r
+  --       return none
+  --     else
+  --       let x := x.expr
+  --       let .forallE xName X Y bi ← withLCtx fData.lctx fData.insts do inferType fData.fn
+  --         | return none
+
+  --       if Y.hasLooseBVars then
+  --         let Y := Expr.lam xName X Y bi
+  --         return ← applyApplyDepRule funTransDecl e x Y
+  --       else
+  --         return ← applyApplyRule funTransDecl e x Y
+  --   else
+  --     -- can we get here?
+  --     throwError "fun_trans bug: bvar app unhandled case"
+
+
+def fvarAppCase (funTransDecl : FunTransDecl) (e : Expr) (fData : FunProp.FunctionData) : SimpM (Option Simp.Result) := do
+  trace[Meta.Tactic.fun_trans.step] "fvar app case"
+  if let .some (f,g) ← fData.nontrivialDecomposition then
+    if let .some r ← applyMorTheorems funTransDecl e fData then
+      return r
+
+    return ← applyCompRule funTransDecl e f g
+  else
+
+    let .fvar fvarId := fData.fn | throwError "fun_trans bug: incorrectly calling fvarAppCase!"
+
+    let thms ← getLocalTheorems funTransDecl (.fvar fvarId) fData.mainArgs e.getAppNumArgs
+    trace[Meta.Tactic.fun_trans] "candidate local theorems for {← ppExpr (.fvar fvarId)}: {thms.map fun thm => thm.thmOrigin.name}"
+    if let .some r ← tryTheorems funTransDecl e fData thms then
+      return r
+
+    if let .some r ← applyMorTheorems funTransDecl e fData then
+      return r
+
+    if let .some r ← applyFVarTheorems e then
+      return r
+
+    return none
+
+/-- Prevend applying morphism theorems to `fun fx => ⇑(Prod.fst fx) (Prod.snd fx)` -/
+def morphismGuard (fData : FunProp.FunctionData) : MetaM Bool := do
+
+  trace[Meta.Tactic.fun_trans] "running guard on {← ppExpr (←fData.toExpr)}"
+  trace[Meta.Tactic.fun_trans] "morphism guard 0 {fData.args.size}"
+  unless fData.args.size == 4 do return true
+  trace[Meta.Tactic.fun_trans] "morphism guard 1 {fData.args[3]!.coe.isSome}"
+  unless fData.args[3]!.coe.isSome do return true
+  trace[Meta.Tactic.fun_trans] "morphism guard 2 {(← fData.getFnConstName?)}"
+  unless (← fData.getFnConstName?) == .some ``Prod.fst do return true
+  trace[Meta.Tactic.fun_trans] "morphism guard 3 {← ppExpr fData.args[2]!.expr}"
+  unless fData.args[2]!.expr == fData.mainVar do return true
+  trace[Meta.Tactic.fun_trans] "morphism guard 4"
+  unless fData.args[3]!.expr.isAppOfArity ``Prod.snd 3 do return true
+  trace[Meta.Tactic.fun_trans] "morphism guard 5 {← ppExpr fData.args[3]!.expr.appArg!}"
+  unless fData.args[3]!.expr.appArg! == fData.mainVar do return true
+  trace[Meta.Tactic.fun_trans] "morphism guard 6"
+
+  return false
+
+
+def constAppCase (funTransDecl : FunTransDecl) (e : Expr) (fData : FunProp.FunctionData) : SimpM (Option Simp.Result) := do
+  trace[Meta.Tactic.fun_trans.step] "const app case on {← ppExpr e}"
+
+  let .some funName ← fData.getFnConstName?
+    | throwError "fun_trans bug: incorrectly calling constAppCase!"
+
+  let thms ←
+    getTheoremsForFunction funName funTransDecl.funTransName e.getAppNumArgs fData.mainArgs
+  trace[Meta.Tactic.fun_trans]
+    "candidate theorems for {funName}: {thms.map fun thm => thm.thmOrigin.name}"
+  if let .some r ← tryTheorems funTransDecl e fData thms then
+    return r
+
+  let thms ← getLocalTheorems funTransDecl (.decl funName) fData.mainArgs e.getAppNumArgs
+  trace[Meta.Tactic.fun_trans]
+    "candidate local theorems for {funName}: {thms.map fun thm => thm.thmOrigin.name}"
+  if let .some r ← tryTheorems funTransDecl e fData thms then
+    return r
+
+  -- if ← morphismGuard fData then
+  if let .some r ← applyMorTheorems funTransDecl e fData then
+    return r
+
+  if let .some (f,g) ← fData.nontrivialDecomposition then
+    -- if ← morphismGuard fData then
+      if let .some r ← applyCompRule funTransDecl e f g then
+        return r
+  else
+    if let .some r ← applyFVarTheorems e then
+      return r
+
+  return none
+
+local instance {ε} : ExceptToEmoji ε (Simp.Step) :=
+  ⟨fun s =>
+    match s with
+    | .ok (.continue .none) => crossEmoji
+    | .ok _ => checkEmoji
+    | .error _ => bombEmoji⟩
+
+/-- Main `funProp` function. Returns proof of `e`. -/
+partial def funTrans (e : Expr) : SimpM Simp.Step := do
+
+  let e ← instantiateMVars e
+
+  let .some (funTransDecl, f) ← getFunTrans? e | return .continue
+
+  if e.approxDepth > 200 then
+    throwError "fun_trans, expression is too deep({e.approxDepth})\n{← ppExpr e}"
+
+  withTraceNode `Meta.Tactic.fun_trans
+    (fun r => return s!"[{ExceptToEmoji.toEmoji r}] {← ppExpr e}") do
+
+  -- bubble leading lets infront of function transformationx
+  if f.isLet then
+    return ← FunProp.letTelescope f fun xs b => do
+      trace[Meta.Tactic.fun_trans.step] "moving let bindings out"
+      let e' := e.setArg funTransDecl.funArgId b
+      return .visit { expr := ← mkLambdaFVars xs e' }
+
+  let toStep (e : SimpM (Option Simp.Result)) : SimpM Simp.Step := do
+    if let .some r ← e then
+      return .visit r
+    else
+      return .continue
+
+  match ← FunProp.getFunctionData? f FunProp.defaultUnfoldPred {zeta:=false} with
+  | .letE f =>
+    trace[Meta.Tactic.fun_trans.step] "let case on {← ppExpr f}"
+    let e := e.setArg funTransDecl.funArgId f -- update e with reduced f
+    toStep <| letCase funTransDecl e f
+  | .lam f =>
+    trace[Meta.Tactic.fun_trans.step] "lam case on {← ppExpr f}"
+    let e := e.setArg funTransDecl.funArgId f -- update e with reduced f
+    toStep <| applyPiRule funTransDecl e f
+  | .data fData =>
+    let e := e.setArg funTransDecl.funArgId (← fData.toExpr) -- update e with reduced f
+
+    if fData.isIdentityFun then
+      toStep <| applyIdRule funTransDecl e (← fData.domainType)
+    else if fData.isConstantFun then
+      toStep <| applyConstRule funTransDecl e
+    else
+      match fData.fn with
+      | .fvar id =>
+        if id == fData.mainVar.fvarId!
+        then toStep <| bvarAppCase funTransDecl e fData
+        else toStep <| fvarAppCase funTransDecl e fData
+      | .mvar .. => funTrans (← instantiateMVars e)
+      | .const ..
+      | .proj .. => toStep <| constAppCase funTransDecl e fData
+      | _ =>
+        trace[Meta.Tactic.fun_trans.step] "unknown case, ctor: {fData.fn.ctorName}\n{e}"
+        return .continue
diff --git a/SciLean/Tactic/FunTrans/Decl.lean b/SciLean/Tactic/FunTrans/Decl.lean
new file mode 100644
index 00000000..531d9316
--- /dev/null
+++ b/SciLean/Tactic/FunTrans/Decl.lean
@@ -0,0 +1,129 @@
+/-
+Copyright (c) 2024 Tomas Skrivan. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Tomas Skrivan
+-/
+import Qq
+
+/-!
+## `funTrans` environment extension that stores all registered function properties
+-/
+
+
+namespace Mathlib
+open Lean Meta
+
+namespace Meta.FunTrans
+
+
+
+initialize registerTraceClass `Meta.Tactic.fun_trans.attr
+initialize registerTraceClass `Meta.Tactic.fun_trans
+
+initialize registerTraceClass `Meta.Tactic.fun_trans.step
+initialize registerTraceClass `Meta.Tactic.fun_trans.unify
+initialize registerTraceClass `Meta.Tactic.fun_trans.discharge
+initialize registerTraceClass `Meta.Tactic.fun_trans.rewrite
+initialize registerTraceClass `Meta.Tactic.fun_trans.unfold
+initialize registerTraceClass `Meta.Tactic.fun_trans.cache
+
+
+
+/-- Basic information about function transformation -/
+structure FunTransDecl where
+  /-- function transformation name -/
+  funTransName : Name
+  /-- path for discriminatory tree -/
+  path : Array DiscrTree.Key
+  /-- argument index of a function this function transformation talks about.
+  For example, this would be 8 for `@fderiv 𝕜 _ E _ _ F _ _ f` -/
+  funArgId : Nat
+  deriving Inhabited, BEq
+
+/-- -/
+structure FunTransDecls where
+  /-- discriminatory tree for function transformations -/
+  decls : DiscrTree FunTransDecl := {}
+  deriving Inhabited
+
+/-- -/
+abbrev FunTransDeclsExt := SimpleScopedEnvExtension FunTransDecl FunTransDecls
+
+/-- -/
+initialize funTransDeclsExt : FunTransDeclsExt ←
+  registerSimpleScopedEnvExtension {
+    name := by exact decl_name%
+    initial := {}
+    addEntry := fun d e =>
+      {d with decls := d.decls.insertCore e.path e}
+  }
+
+/-- -/
+def addFunTransDecl (declName : Name) : MetaM Unit := do
+
+  let info ← getConstInfo declName
+
+  let (xs,_,_) ← forallMetaTelescope info.type
+
+  -- find the argument position of the function `f` in `P f`
+  let mut .some funArgId ← xs.reverse.findIdxM? fun x => do
+    if (← inferType x).isForall then
+      return true
+    else
+      return false
+    | throwError "invalid fun_trans declaration, can't find argument of type `α → β`"
+  funArgId := xs.size - funArgId - 1
+
+  let lvls := info.levelParams.map (fun l => Level.param l)
+  let e := mkAppN (.const declName lvls) xs[0:funArgId+1]
+  let path ← DiscrTree.mkPath e {}
+
+  let decl : FunTransDecl := {
+    funTransName := declName
+    path := path
+    funArgId := funArgId
+  }
+
+  modifyEnv fun env => funTransDeclsExt.addEntry env decl
+
+  trace[Meta.Tactic.fun_trans.attr]
+    "added new function property `{declName}`\nlook up pattern is `{path}`"
+
+
+/-- -/
+def getFunTrans? (e : Expr) : MetaM (Option (FunTransDecl × Expr)) := do
+  unless e.isApp do return .none
+
+  let ext := funTransDeclsExt.getState (← getEnv)
+
+  let decls ← ext.decls.getMatchWithExtra e
+    {zeta:=false,zetaDelta:=false,proj:=.no,iota:=false,beta:=false}
+
+  if decls.size = 0 then
+    return none
+
+  if decls.size > 1 then
+    throwError "\
+fun_trans bug: expression {← ppExpr e} matches multiple function transformations
+{decls.map (fun d => d.1.funTransName)}"
+
+  let decl := decls[0]!.fst
+  let f := e.getArg! decl.funArgId
+
+  return (decl,f)
+
+/-- -/
+def isFunTrans (e : Expr) : MetaM Bool := do return (← getFunTrans? e).isSome
+
+/-- Returns function property transformation from `e = T f`. -/
+def getFunTransDecl? (e : Expr) : MetaM (Option FunTransDecl) := do
+  match ← getFunTrans? e with
+  | .some (decl,_) => return decl
+  | .none => return none
+
+
+/-- Returns function `f` from `e = T f` and `T` is function transformation. -/
+def getFunTransFun? (e : Expr) : MetaM (Option Expr) := do
+  match ← getFunTrans? e with
+  | .some (_,f) => return f
+  | .none => return none
diff --git a/SciLean/Tactic/FunTrans/Elab.lean b/SciLean/Tactic/FunTrans/Elab.lean
new file mode 100644
index 00000000..866b0f09
--- /dev/null
+++ b/SciLean/Tactic/FunTrans/Elab.lean
@@ -0,0 +1,85 @@
+/-
+Copyright (c) 2024 Tomas Skrivan. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Tomas Skrivan
+-/
+import Lean
+import Mathlib.Tactic.FunProp.Core
+import SciLean.Tactic.FunTrans.Core
+
+/-!
+## `funProp` tactic syntax
+-/
+
+namespace Mathlib
+open Lean Meta Elab Tactic
+
+namespace Meta.FunTrans
+
+open Lean.Parser.Tactic
+
+
+syntax (name := funTransTacStx) "fun_trans" (config)? (discharger)? (&" only")?
+  (" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*,?) "]")? (location)? : tactic
+
+syntax (name := funTransConvStx) "fun_trans" (config)? (discharger)? (&" only")?
+  (" [" withoutPosition((simpStar <|> simpErase <|> simpLemma),*) "]")? : conv
+
+
+simproc_decl fun_trans_simproc (_) := funTrans
+
+private def emptyDischarge : Expr → MetaM (Option Expr) :=
+  fun e =>
+    withTraceNode `Meta.Tactic.fun_trans
+      (fun r => do pure s!"[{ExceptToEmoji.toEmoji r}] discharging: {← ppExpr e}") do
+      pure none
+
+private def stxToDischarge (stx : Option (TSyntax ``discharger)) : Expr → MetaM (Option Expr) := fun e => do
+  match stx with
+  | none => (emptyDischarge e)
+  | some d =>
+    match d with
+    | `(discharger| (discharger:=$tac)) => FunProp.tacticToDischarge (← `(tactic| ($tac))) e
+    | _ => emptyDischarge e
+
+
+@[tactic funTransTacStx]
+def funTransTac : Tactic := fun stx => do
+  match stx with
+  | `(tactic| fun_trans $[$cfg]? $[$disch]? $[only]? $[[$a,*]]? $[$loc]?) => do
+
+    -- set fun_trans config
+    funTransConfig.modify
+      fun c => { c with funPropConfig := { c.funPropConfig with disch := stxToDischarge disch}}
+
+    let a := a.getD (Syntax.TSepArray.mk #[])
+    if stx[3].isNone then
+      evalTactic (← `(tactic| simp $[$cfg]? $[$disch]? [↓fun_trans_simproc,$a,*]  $[$loc]?))
+    else
+      evalTactic (← `(tactic| simp $[$cfg]? $[$disch]? only [↓fun_trans_simproc,$a,*]  $[$loc]?))
+
+    -- reset fun_trans config
+    funTransConfig.modify fun _ => {}
+
+  | _ => throwUnsupportedSyntax
+
+
+@[tactic funTransConvStx]
+def funTransConv : Tactic := fun stx => do
+  match stx with
+  | `(conv| fun_trans $[$cfg]? $[$disch]? $[only]? $[[$a,*]]?) => do
+
+    -- set fun_trans config
+    funTransConfig.modify
+      fun c => { c with funPropConfig := { c.funPropConfig with disch := stxToDischarge disch}}
+
+    let a := a.getD (Syntax.TSepArray.mk #[])
+    if stx[3].isNone then
+      evalTactic (← `(conv| simp $[$cfg]? $[$disch]? [↓fun_trans_simproc,$a,*]))
+    else
+      evalTactic (← `(conv| simp $[$cfg]? $[$disch]? only [↓fun_trans_simproc,$a,*]))
+
+    -- reset fun_trans config
+    funTransConfig.modify fun _ => {}
+
+  | _ => throwUnsupportedSyntax
diff --git a/SciLean/Tactic/FunTrans/Theorems.lean b/SciLean/Tactic/FunTrans/Theorems.lean
new file mode 100644
index 00000000..828c2190
--- /dev/null
+++ b/SciLean/Tactic/FunTrans/Theorems.lean
@@ -0,0 +1,353 @@
+/-
+Copyright (c) 2024 Tomas Skrivan. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Tomas Skrivan
+-/
+import Batteries.Data.RBMap.Alter
+
+import SciLean.Tactic.FunTrans.Decl
+import Mathlib.Tactic.FunProp.Theorems
+
+/-!
+## `fun_trans` enviroment extensions storing thorems for `fun_trans`
+-/
+
+namespace Mathlib
+open Lean Meta
+
+namespace Meta.FunTrans
+
+/--  -/
+structure LambdaTheorem where
+  /-- Name of function transformation -/
+  funTransName : Name
+  /-- Name of lambda theorem -/
+  thmName : Name
+  /-- total number of arguments applied to the function transformation  -/
+  transAppliedArgs : Nat
+  /-- Type and important argument of the theorem. -/
+  thmArgs : FunProp.LambdaTheoremArgs
+  deriving Inhabited, BEq
+
+/-- -/
+structure LambdaTheorems where
+  /-- map: function transfromation name × theorem type → lambda theorem -/
+  theorems : HashMap (Name × FunProp.LambdaTheoremType) (Array LambdaTheorem) := {}
+  deriving Inhabited
+
+
+/-- return proof of lambda theorem -/
+def LambdaTheorem.getProof (thm : LambdaTheorem) : MetaM Expr := do
+  mkConstWithFreshMVarLevels thm.thmName
+
+/-- -/
+abbrev LambdaTheoremsExt := SimpleScopedEnvExtension LambdaTheorem LambdaTheorems
+
+/-- Extension storing all lambda theorems. -/
+initialize lambdaTheoremsExt : LambdaTheoremsExt ←
+  registerSimpleScopedEnvExtension {
+    name := by exact decl_name%
+    initial := {}
+    addEntry := fun d e =>
+      {d with theorems :=
+         let es := d.theorems.findD (e.funTransName, e.thmArgs.type) #[]
+         d.theorems.insert (e.funTransName, e.thmArgs.type) (es.push e)}
+  }
+
+/-- Return lambda theorems of type `type` for function transformation `funTransName`
+
+Theorems are filtered and sorted based on the optional argument `nargs`. It specifies the number of
+arguments of the expression we want to transform.
+
+For example when transforming
+```
+deriv (fun x => x * sin x)
+```
+we do not want to use composition theorem stating `deriv (fun x' => f (g x')) x` because our
+expression does not have the concrete point where we differentiate.
+
+On the other hand when transforming
+```
+deriv (fun x' => 1/(1-x')) x
+```
+we prefer the version `deriv (fun x' => f (g x')) x` over `deriv (fun x' => f (g x'))` as the former
+uses `DifferntiableAt` insed of `Differentiable` as preconditions. -/
+def getLambdaTheorems (funTransName : Name) (type : FunProp.LambdaTheoremType) (nargs : Option Nat):
+    CoreM (Option (Array LambdaTheorem)) := do
+  let .some thms := (lambdaTheoremsExt.getState (← getEnv)).theorems.find? (funTransName,type)
+    | return none
+
+  match nargs with
+  | none => return thms
+  | some n =>
+    let thms := thms
+        |>.filter (fun thm => thm.transAppliedArgs ≤ n)
+        |>.qsort (fun t t' => t'.transAppliedArgs < t.transAppliedArgs)
+    return thms
+
+
+----------------------------------------------------------------------------------------------------
+
+
+/-- theorem about specific function (either declared constant or free variable) -/
+structure FunctionTheorem where
+  /-- function transformation name -/
+  funTransName : Name
+  /-- total number of arguments applied to the function transformation  -/
+  transAppliedArgs : Nat
+  /-- theorem name -/
+  thmOrigin   : FunProp.Origin
+  /-- function name -/
+  funOrigin   : FunProp.Origin
+  /-- array of argument indices about which this theorem is about -/
+  mainArgs  : Array Nat
+  /-- total number of arguments applied to the function  -/
+  appliedArgs : Nat
+  /-- priority  -/
+  priority    : Nat  := eval_prio default
+  /-- form of the theorem, see documentation of TheoremForm -/
+  form : FunProp.TheoremForm
+  deriving Inhabited, BEq
+
+
+private local instance : Ord Name := ⟨Name.quickCmp⟩
+
+/-- -/
+structure FunctionTheorems where
+  /-- map: function name → function transformation → function theorem -/
+  theorems : Batteries.RBMap Name (Batteries.RBMap Name (Array FunctionTheorem) compare) compare := {}
+  deriving Inhabited
+
+
+/-- return proof of function theorem -/
+def FunctionTheorem.getProof (thm : FunctionTheorem) : MetaM Expr := do
+  match thm.thmOrigin with
+  | .decl name => mkConstWithFreshMVarLevels name
+  | .fvar id => pure (.fvar id)
+
+
+/-- -/
+abbrev FunctionTheoremsExt := SimpleScopedEnvExtension FunctionTheorem FunctionTheorems
+
+/-- Extension storing all function theorems. -/
+initialize functionTheoremsExt : FunctionTheoremsExt ←
+  registerSimpleScopedEnvExtension {
+    name     := by exact decl_name%
+    initial  := {}
+    addEntry := fun d e =>
+      {d with
+        theorems :=
+          d.theorems.alter e.funOrigin.name fun funTrans =>
+            let funTrans := funTrans.getD {}
+            funTrans.alter e.funTransName fun thms =>
+              let thms := thms.getD #[]
+              thms.push e}
+  }
+
+
+/-- -/
+def getTheoremsForFunction (funName : Name) (funTransName : Name) (nargs : Option Nat) (mainArgs : Option (Array ℕ)) :
+    CoreM (Array FunctionTheorem) := do
+
+  let thms := (functionTheoremsExt.getState (← getEnv)).theorems.findD funName {}
+              |>.findD funTransName #[]
+
+  let thms := thms
+      |>.filter (fun thm =>
+         (nargs.map (fun n => (thm.transAppliedArgs ≤ n : Bool))).getD true
+         &&
+         (mainArgs.map (fun args => FunProp.isOrderedSubsetOf args thm.mainArgs)).getD true)
+      |>.qsort (fun t t' => t'.transAppliedArgs < t.transAppliedArgs)
+
+  return thms
+
+
+
+----------------------------------------------------------------------------------------------------
+
+/-- General theorem about function transformation used for morphism theorems -/
+structure GeneralTheorem where
+  /-- function transformation name -/
+  funTransName   : Name
+  /-- theorem name -/
+  thmName     : Name
+  /-- discriminatory tree keys used to index this theorem -/
+  keys        : List FunProp.RefinedDiscrTree.DTExpr
+  /-- priority -/
+  priority    : Nat  := eval_prio default
+  deriving Inhabited, BEq
+
+/-- Get proof of a theorem. -/
+def GeneralTheorem.getProof (thm : GeneralTheorem) : MetaM Expr := do
+  mkConstWithFreshMVarLevels thm.thmName
+
+/-- -/
+structure GeneralTheorems where
+  /-- -/
+  theorems     : FunProp.RefinedDiscrTree GeneralTheorem := {}
+  deriving Inhabited
+
+/-- -/
+abbrev GeneralTheoremsExt := SimpleScopedEnvExtension GeneralTheorem GeneralTheorems
+
+/-- -/
+initialize morTheoremsExt : GeneralTheoremsExt ←
+  registerSimpleScopedEnvExtension {
+    name     := by exact decl_name%
+    initial  := {}
+    addEntry := fun d e =>
+      {d with theorems := e.keys.foldl (FunProp.RefinedDiscrTree.insertDTExpr · · e) d.theorems}
+  }
+
+
+/-- -/
+initialize fvarTheoremsExt : GeneralTheoremsExt ←
+  registerSimpleScopedEnvExtension {
+    name     := by exact decl_name%
+    initial  := {}
+    addEntry := fun d e =>
+      {d with theorems := e.keys.foldl (FunProp.RefinedDiscrTree.insertDTExpr · · e) d.theorems}
+  }
+
+
+
+--------------------------------------------------------------------------------
+
+
+/-- There are four types of theorems:
+- lam - theorem about basic lambda calculus terms
+- function - theorem about a specific function(declared or free variable) in specific arguments
+- mor - special theorems talking about bundled morphisms/DFunLike.coe
+- transition - theorems inferring one function property from another
+
+Examples:
+- lam
+```
+  theorem Continuous_id : Continuous fun x => x
+  theorem Continuous_comp (hf : Continuous f) (hg : Continuous g) : Continuous fun x => f (g x)
+```
+- function
+```
+  theorem Continuous_add : Continuous (fun x => x.1 + x.2)
+  theorem Continuous_add (hf : Continuous f) (hg : Continuous g) :
+      Continuous (fun x => (f x) + (g x))
+```
+- mor - the head of function body has to be ``DFunLike.code
+```
+  theorem ContDiff.clm_apply {f : E → F →L[𝕜] G} {g : E → F}
+      (hf : ContDiff 𝕜 n f) (hg : ContDiff 𝕜 n g) :
+      ContDiff 𝕜 n fun x => (f x) (g x)
+  theorem clm_linear {f : E →L[𝕜] F} : IsLinearMap 𝕜 f
+```
+- transition - the conclusion has to be in the form `P f` where `f` is a free variable
+```
+  theorem linear_is_continuous [FiniteDimensional ℝ E] {f : E → F} (hf : IsLinearMap 𝕜 f) :
+      Continuous f
+```
+-/
+inductive Theorem where
+  | lam        (thm : LambdaTheorem)
+  | function   (thm : FunctionTheorem)
+  | mor        (thm : GeneralTheorem)
+  | fvar       (thm : GeneralTheorem)
+
+
+/-- -/
+def getTheoremFromConst (declName : Name) (prio : Nat := eval_prio default) : MetaM Theorem := do
+  let info ← getConstInfo declName
+  forallTelescope info.type fun xs b => do
+
+    unless b.isEq do throwError "equality expected"
+
+    let lhs := b.getArg! 1
+
+    let .some (decl,f) ← getFunTrans? lhs
+      | throwError "unrecognized function transformation `{← ppExpr lhs}`"
+    let funTransName := decl.funTransName
+
+    let fData? ← FunProp.getFunctionData? f FunProp.defaultUnfoldPred {zeta:=false}
+
+    if let .some thmArgs ← FunProp.detectLambdaTheoremArgs (← fData?.get) xs then
+      return .lam {
+        funTransName := funTransName
+        transAppliedArgs := lhs.getAppNumArgs
+        thmName := declName
+        thmArgs := thmArgs
+      }
+
+    let .data fData := fData?
+      | throwError s!"function in invalid form {← ppExpr f}"
+
+    match fData.fn with
+    | .const funName _ =>
+
+      let dec ← fData.nontrivialDecomposition
+      let form : FunProp.TheoremForm :=
+        if dec.isSome || funName == ``Prod.mk then .comp else .uncurried
+
+      return .function {
+-- funTransName funName fData.mainArgs fData.args.size thmForm
+        funTransName := funTransName
+        transAppliedArgs := lhs.getAppNumArgs'
+        thmOrigin := .decl declName
+        funOrigin := .decl funName
+        mainArgs := fData.mainArgs
+        appliedArgs := fData.args.size
+        priority := prio
+        form := form
+      }
+    | .fvar .. =>
+      let (_,_,b') ← forallMetaTelescope info.type
+      let keys := ← FunProp.RefinedDiscrTree.mkDTExprs (b'.getArg! 1) {} false
+      let thm : GeneralTheorem := {
+        funTransName := funTransName
+        thmName := declName
+        keys    := keys
+        priority  := prio
+      }
+
+      let n := fData.args.size
+      if n = 1 &&
+         fData.args[0]!.coe.isNone &&
+         fData.args[0]!.expr == fData.mainVar then
+        return .fvar thm
+      else if (n > 0) && fData.args[n-1]!.coe.isSome then
+        return .mor thm
+      else
+        throwError "unrecognized theoremType `{← ppExpr b}`"
+    | _ =>
+      throwError "unrecognized theoremType `{← ppExpr b}`"
+
+
+/-- -/
+def addTheorem (declName : Name) (attrKind : AttributeKind := .global)
+    (prio : Nat := eval_prio default) : MetaM Unit := do
+  match (← getTheoremFromConst declName prio) with
+  | .lam thm =>
+    trace[Meta.Tactic.fun_trans.attr] "\
+lambda theorem: {thm.thmName}
+function transfromations: {thm.funTransName}
+type: {repr thm.thmArgs.type}"
+    lambdaTheoremsExt.add thm attrKind
+  | .function thm =>
+    trace[Meta.Tactic.fun_trans.attr] "\
+function theorem: {thm.thmOrigin.name}
+function transformation: {thm.funTransName}
+function transformation applied args: {thm.transAppliedArgs}
+function name: {thm.funOrigin.name}
+main arguments: {thm.mainArgs}
+applied arguments: {thm.appliedArgs}
+form: {repr thm.form}"
+    functionTheoremsExt.add thm attrKind
+  | .mor thm =>
+    trace[Meta.Tactic.fun_trans.attr] "\
+morphism theorem: {thm.thmName}
+function transformation: {thm.funTransName}
+discr tree key: {thm.keys}"
+    morTheoremsExt.add thm attrKind
+  | .fvar thm =>
+    trace[Meta.Tactic.fun_trans.attr] "\
+fvar theorem: {thm.thmName}
+function transformation: {thm.funTransName}
+discr tree key: {thm.keys}"
+    fvarTheoremsExt.add thm attrKind
diff --git a/SciLean/Tactic/FunTrans/Types.lean b/SciLean/Tactic/FunTrans/Types.lean
new file mode 100644
index 00000000..4832faa3
--- /dev/null
+++ b/SciLean/Tactic/FunTrans/Types.lean
@@ -0,0 +1,24 @@
+/-
+Copyright (c) 2024 Tomas Skrivan. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Tomas Skrivan
+-/
+import Lean.Meta.Tactic.Simp.Types
+
+import Mathlib.Tactic.FunProp.Types
+
+/-!
+## `funTrans`
+-/
+
+namespace Mathlib
+open Lean Meta
+
+namespace Meta.FunTrans
+
+
+structure Config where
+  funPropConfig : FunProp.Config := {}
+deriving Inhabited
+
+initialize funTransConfig : IO.Ref Config ← IO.mkRef {}
diff --git a/SciLean/Tactic/FunTrans2/Core.lean b/SciLean/Tactic/FunTrans2/Core.lean
index acfc5563..54c5f780 100644
--- a/SciLean/Tactic/FunTrans2/Core.lean
+++ b/SciLean/Tactic/FunTrans2/Core.lean
@@ -3,7 +3,7 @@ import Lean.Util.Trace
 
 import SciLean.Lean.Meta.Basic
 
-import Mathlib.Tactic.FunTrans.Core
+import SciLean.Tactic.FunTrans.Core
 
 open Lean Meta
 
diff --git a/SciLean/Tactic/GTrans/Elab.lean b/SciLean/Tactic/GTrans/Elab.lean
index 91a622ff..d2a6bf8a 100644
--- a/SciLean/Tactic/GTrans/Elab.lean
+++ b/SciLean/Tactic/GTrans/Elab.lean
@@ -17,8 +17,6 @@ syntax (name:=gtrans_tac) "gtrans" : tactic
 /-- `gtrans` as conv tactic will fill in meta variables in generalized transformation -/
 syntax (name:=gtrans_conv) "gtrans" : conv
 
-#check Nat
-
 open Lean.Parser.Tactic in
 syntax (name:=gtrans_tac') "gtrans" (config)? (discharger)? (normalizer)? : tactic
 
diff --git a/SciLean/Tactic/GTrans/MetaLCtxM.lean b/SciLean/Tactic/GTrans/MetaLCtxM.lean
index f1a777f9..5e32b136 100644
--- a/SciLean/Tactic/GTrans/MetaLCtxM.lean
+++ b/SciLean/Tactic/GTrans/MetaLCtxM.lean
@@ -65,10 +65,10 @@ instance : MonadLift MetaM MetaLCtxM where
   monadLift x := fun cfg ctx => do let r ← x (.mkCtxCfg ctx cfg); pure (r, ctx)
 
 protected def MetaLCtxM.saveState : MetaLCtxM (SavedState×ContextCtx) :=
-  return ({ core := (← getThe Core.State), meta := (← get) }, ⟨← getLCtx, ← getLocalInstances⟩)
+  return ({ core := (← Core.saveState), meta := (← get) }, ⟨← getLCtx, ← getLocalInstances⟩)
 
 def MetaLCtxM.restore (b : SavedState) (ctx : ContextCtx) : MetaLCtxM Unit := do
-  Core.restore b.core
+  b.restore
   modify fun s => { s with mctx := b.meta.mctx, zetaDeltaFVarIds := b.meta.zetaDeltaFVarIds, postponed := b.meta.postponed }
   modifyThe ContextCtx fun _ => ctx
 
@@ -148,12 +148,12 @@ def introLetDecl (name : Name) (type? : Option Expr) (val : Expr) : MetaLCtxM Ex
     return (fvar, ctx)
 
 
-open Lean Meta Qq in
-#eval show MetaLCtxM Unit from do
-  let e := q(fun a b => a + b + 42)
+-- open Lean Meta Qq in
+-- #eval show MetaLCtxM Unit from do
+--   let e := q(fun a b => a + b + 42)
 
-  let (b, xs) ← lambdaIntro e
+--   let (b, xs) ← lambdaIntro e
 
-  IO.println s!"lambda body: {← ppExpr b}"
-  IO.println s!"lambda vars: {← liftM <| xs.mapM ppExpr}"
-  IO.println s!"lambda: {← ppExpr (← mkLambdaFVars xs b)}"
+--   IO.println s!"lambda body: {← ppExpr b}"
+--   IO.println s!"lambda vars: {← liftM <| xs.mapM ppExpr}"
+--   IO.println s!"lambda: {← ppExpr (← mkLambdaFVars xs b)}"
diff --git a/SciLean/Tactic/LSimp/Main.lean b/SciLean/Tactic/LSimp/Main.lean
index 22969b9a..2cd939f2 100644
--- a/SciLean/Tactic/LSimp/Main.lean
+++ b/SciLean/Tactic/LSimp/Main.lean
@@ -306,17 +306,6 @@ partial def reduce (e : Expr) : LSimpM Expr :=  /- withIncRecDepth -/  do
     reduce e'
 
 
-partial def simpLit (e : Expr) : LSimpM Result := do
-  match e.natLit? with
-  | some n =>
-    /- If `OfNat.ofNat` is marked to be unfolded, we do not pack orphan nat literals as `OfNat.ofNat` applications
-        to avoid non-termination. See issue #788.  -/
-    if (← readThe Simp.Context).isDeclToUnfold ``OfNat.ofNat then
-      return { expr := e }
-    else
-      return { expr := (← mkNumeral (mkConst ``Nat) n) }
-  | none   => return { expr := e }
-
 partial def simpProj (e : Expr) : LSimpM Result := do
   match (← Meta.reduceProj? e) with
   | some e =>
@@ -672,16 +661,13 @@ partial def simpStep (e : Expr) : LSimpM Result := do
   | .const ..    => simpConst e
   | .bvar ..     => unreachable!
   | .sort ..     => return { expr := e }
-  | .lit ..      => simpLit e
+  | .lit ..      => return { expr := e }
   | .mvar ..     => return { expr := (← instantiateMVars e) }
   | .fvar ..     => return { expr := (← reduceFVar (← getConfig) (← Simp.getSimpTheorems) e) }
 
 
 partial def cacheResult (e : Expr) (cfg : Simp.Config) (r : Result) : LSimpM Result := do
   if cfg.memoize && r.cache then
-    let ctx ← readThe Simp.Context
-    let dischargeDepth := ctx.dischargeDepth
-    let r : Result := { r with dischargeDepth }
     let cacheRef := (← getThe State).cache
     cacheRef.modify (fun c => c.insert e r)
   return r
@@ -732,16 +718,11 @@ where
       -- try LSimp.Cache
       let cache ← (← getThe State).cache.get
       if let some result := cache.find? e then
-        if result.dischargeDepth ≤ (← readThe Simp.Context).dischargeDepth then
-          trace[Meta.Tactic.simp.cache] "cached result {e}==>{(←result.bindVars).expr}"
-          return result
+        return result
       -- try Sipm.Cache
       let cache := (← (← getThe State).simpState.get).cache
       if let some result := cache.find? e then
-        if result.dischargeDepth ≤ (← readThe Simp.Context).dischargeDepth then
-          trace[Meta.Tactic.simp.cache] "cached result {e}==>{result.expr}"
-          return { result with }
+        return { result with }
 
     trace[Meta.Tactic.simp.heads] "{repr e.toHeadIndex}"
-    withTraceNode `Meta.Tactic.simp.heads (fun _ => pure s!"{repr e.toHeadIndex}") do
-      simpLoop e
+    simpLoop e
diff --git a/SciLean/Tactic/LSimp/Test.lean b/SciLean/Tactic/LSimp/Test.lean
index 91d4cad1..1d284226 100644
--- a/SciLean/Tactic/LSimp/Test.lean
+++ b/SciLean/Tactic/LSimp/Test.lean
@@ -1,3 +1,4 @@
+import SciLean.Tactic.MathlibCompiledTactics
 import SciLean.Tactic.LSimp.Elab
 import SciLean.Util.RewriteBy
 import SciLean.Core
@@ -67,7 +68,6 @@ def testExpression (n : Nat) : MetaM Q(Float → Float) :=
 #eval show MetaM Unit from do
   IO.println (← ppExpr (← testExpression 8))
 
-
 #check (0 + 1 + 0) rewrite_by lsimp
 
 
@@ -137,7 +137,6 @@ def measureOnTestExpression (n : Nat) : MetaM (Array MeasureData) := do
 
 -- set_option trace.Meta.Tactic.simp.heads true
 
-
 example (n : Nat) :
   n
   =
diff --git a/SciLean/Tactic/LSimp/Types.lean b/SciLean/Tactic/LSimp/Types.lean
index 0b9d0ce5..48981269 100644
--- a/SciLean/Tactic/LSimp/Types.lean
+++ b/SciLean/Tactic/LSimp/Types.lean
@@ -7,8 +7,8 @@ import SciLean.Lean.Meta.Basic
 
 import SciLean.Tactic.GTrans.MetaLCtxM
 
-import Mathlib.Tactic.FunTrans.Core
-import Mathlib.Tactic.FunTrans.Elab
+import SciLean.Tactic.FunTrans.Core
+import SciLean.Tactic.FunTrans.Elab
 
 open Lean Meta
 
@@ -24,7 +24,6 @@ structure Result where
   expr : Expr
   proof? : Option Expr := none
   vars : Array Expr := #[]
-  dischargeDepth : UInt32 := 0
   cache          : Bool := true
   deriving Inhabited
 
@@ -44,7 +43,6 @@ def _root_.Lean.Meta.Simp.Result.toLResult (s : Simp.Result) : Result :=
   { expr := s.expr,
     proof? := s.proof?,
     vars := #[],
-    dischargeDepth := s.dischargeDepth,
     cache := s.cache }
 
 def Result.getProof (r : Result) : MetaM Expr :=
@@ -92,7 +90,7 @@ structure State where
   /-- Cache storing lsimp results. -/
   cache : IO.Ref Cache
   simpState : IO.Ref Simp.State
-  timings : Std.RBMap String Aesop.Nanos compare := {}
+  timings : Batteries.RBMap String Aesop.Nanos compare := {}
 
 
 abbrev LSimpM := ReaderT Simp.Methods $ ReaderT Simp.Context $ StateT State MetaLCtxM
diff --git a/SciLean/Tactic/LetNormalize.lean b/SciLean/Tactic/LetNormalize.lean
index 25f5fad2..edeb6023 100644
--- a/SciLean/Tactic/LetNormalize.lean
+++ b/SciLean/Tactic/LetNormalize.lean
@@ -134,23 +134,24 @@ partial def letNormalize (e : Expr) (config : LetNormalizeConfig) : MetaM Expr :
       -- deconstruct constructors into bunch of let bindings
       if config.splitStructureConstuctors then
         if let .some (ctor, args) ← constructorApp? xValue' then
-          if let .some info := getStructureInfo? (← getEnv) xType.getAppFn.constName! then
-            let mut lctx ← getLCtx
-            let insts ← getLocalInstances
-            let mut fvars : Array Expr := #[]
-            for i in [0:ctor.numFields] do
-              let fvarId ← withLCtx lctx insts mkFreshFVarId
-              let name := xName.appendAfter s!"_{info.fieldNames[i]!}"
-              let val  := args[ctor.numParams + i]!
-              let type ← inferType val
-              lctx := lctx.mkLetDecl fvarId name type val (nonDep := false) default
-              fvars := fvars.push (.fvar fvarId)
-
-            let e' ← withLCtx lctx insts do
-              let xValue'' := mkAppN xValue'.getAppFn (args[0:ctor.numFields].toArray.append fvars)
-              mkLambdaFVars fvars (xBody.instantiate1 xValue'')
-
-            return (← letNormalize e' config)
+        if let .some name := xType.getAppFn.constName? then
+        if let .some info := getStructureInfo? (← getEnv) name then
+          let mut lctx ← getLCtx
+          let insts ← getLocalInstances
+          let mut fvars : Array Expr := #[]
+          for i in [0:ctor.numFields] do
+            let fvarId ← withLCtx lctx insts mkFreshFVarId
+            let name := xName.appendAfter s!"_{info.fieldNames[i]!}"
+            let val  := args[ctor.numParams + i]!
+            let type ← inferType val
+            lctx := lctx.mkLetDecl fvarId name type val (nonDep := false) default
+            fvars := fvars.push (.fvar fvarId)
+
+          let e' ← withLCtx lctx insts do
+            let xValue'' := mkAppN xValue'.getAppFn (args[0:ctor.numFields].toArray.append fvars)
+            mkLambdaFVars fvars (xBody.instantiate1 xValue'')
+
+          return (← letNormalize e' config)
 
       -- in all other cases normalized the body
       withLetDecl xName xType xValue' fun x => do
diff --git a/SciLean/Tactic/MathlibCompiledTactics.lean b/SciLean/Tactic/MathlibCompiledTactics.lean
index a8201e05..620f3306 100644
--- a/SciLean/Tactic/MathlibCompiledTactics.lean
+++ b/SciLean/Tactic/MathlibCompiledTactics.lean
@@ -1,4 +1,5 @@
 import Mathlib.Tactic.FunProp
-import Mathlib.Tactic.FunTrans.Elab
-import Mathlib.Tactic.FunTrans.Attr
+import SciLean.Tactic.FunTrans.Elab
+import SciLean.Tactic.FunTrans.Attr
 import SciLean.Tactic.LSimp.Main
+import SciLean.Tactic.LSimp.Types
diff --git a/SciLean/Tactic/StructuralInverse.lean b/SciLean/Tactic/StructuralInverse.lean
index bbecdfb7..e4195e8a 100644
--- a/SciLean/Tactic/StructuralInverse.lean
+++ b/SciLean/Tactic/StructuralInverse.lean
@@ -329,7 +329,7 @@ def structuralInverse (f : Expr) : MetaM (Option (FunctionInverse × Array MVarI
             let l ← proof.mvarId!.constructor
             l.forM fun m => do
               let (_,m') ← m.intros
-              m'.applyRefl
+              m'.refl
 
             let dec : StructureDecomposition := {
               u := u, v := u₁, w := u₂, X := X, X₁ := X₁, X₂ := X₂
diff --git a/SciLean/Tactic/StructureDecomposition.lean b/SciLean/Tactic/StructureDecomposition.lean
index 03073247..8e0a6387 100644
--- a/SciLean/Tactic/StructureDecomposition.lean
+++ b/SciLean/Tactic/StructureDecomposition.lean
@@ -189,7 +189,7 @@ def decomposeStructure (e : Expr) (split : Nat → Expr → Bool) : MetaM (Optio
       let l ← proof.mvarId!.constructor
       l.forM fun m => do
         let (_,m') ← m.intros
-        m'.applyRefl
+        m'.refl
 
       return .some {u:=u, v:=v, w:=w, X:=X, X₁:=X₁, X₂:=X₂, p₁:=p₁, p₂:=p₂, q:=q, proof := proof}
 
@@ -255,7 +255,7 @@ def factorDomainThroughProjections (f : Expr) : MetaM (Option DomainDecompositio
         let f : Q($dec.X → $Y) := f
 
         let proof ← mkFreshExprMVarQ q(∀ x, $f' ($dec.p₁ x) = $f x)
-        proof.mvarId!.intros >>= fun (_,m) => m.applyRefl
+        proof.mvarId!.intros >>= fun (_,m) => m.refl
 
         return .some {u:= u, Y:=Y, dec:=dec, f:=f, f':=f', proof:=proof}
 
@@ -294,7 +294,7 @@ def factorCodomainThroughProjections (f : Expr) : MetaM (Option CodomainDecompos
       let f : Q($X → $dec.X) := f
 
       let proof ← mkFreshExprMVarQ q(∀ x, $dec.q ($f' x) $y₂ = $f x)
-      proof.mvarId!.intros >>= fun (_,m) => m.applyRefl
+      proof.mvarId!.intros >>= fun (_,m) => m.refl
 
       return .some {u:=u, X:=X, dec:=dec, f:=f, f':=f', y₂:=y₂, proof:=proof}
 
diff --git a/SciLean/Util/DefOptimize.lean b/SciLean/Util/DefOptimize.lean
index 3f3e3a3a..7b8f0473 100644
--- a/SciLean/Util/DefOptimize.lean
+++ b/SciLean/Util/DefOptimize.lean
@@ -21,7 +21,7 @@ elab "def_optimize" f:ident "by " t:convSeq : command => do
       let (value',eq) ← elabConvRewrite val #[] (← `(conv| ($t)))
       pure (← mkLambdaFVars xs value', ← mkLambdaFVars xs eq)
 
-  let optName := info.name.append "optimized"
+  let optName := info.name.append (.mkSimple "optimized")
 
   let optimizedDef : DefinitionVal :=
   {
@@ -41,11 +41,11 @@ elab "def_optimize" f:ident "by " t:convSeq : command => do
     let rhs ← mkAppOptM optName (xs.map .some)
     mkForallFVars xs (← mkEq lhs rhs)
 
-  let thmName := info.name.append "optimize_rule"
+  let thmName := info.name.append (.mkSimple "optimize_rule")
 
   let eqTheorem : TheoremVal :=
   {
-    name  := info.name.append "optimize_rule"
+    name  := info.name.append (.mkSimple "optimize_rule")
     type  := eqType
     value := (← instantiateMVars eq)
     levelParams := info.levelParams
diff --git a/SciLean/Util/Profile.lean b/SciLean/Util/Profile.lean
index 7841ae28..ae11d6c4 100644
--- a/SciLean/Util/Profile.lean
+++ b/SciLean/Util/Profile.lean
@@ -44,7 +44,7 @@ def profileFile (file : FilePath) (flame : FilePath := "/home/tskrivan/Documents
   let stdout ← IO.asTask child.stdout.readToEnd Task.Priority.dedicated
   let stderr ← child.stderr.readToEnd
   let exitCode ← child.wait
-  let stdout ← IO.ofExcept stdout.get
+  let _stdout ← IO.ofExcept stdout.get
 
   if exitCode != 0 then
     throw (IO.Error.userError s!"Error: Failed to run speedscope\n\n{stderr}")
diff --git a/lake-manifest.json b/lake-manifest.json
index c1f5b19f..a7ab4e8f 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -1,11 +1,11 @@
-{"version": 7,
+{"version": "1.0.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/leanprover/std4",
+ [{"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
-   "rev": "e840c18f7334c751efbd4cfe531476e10c943cdb",
-   "name": "std",
+   "rev": "47e4cc5c5800c07d9bf232173c9941fa5bf68589",
+   "name": "batteries",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
@@ -13,7 +13,7 @@
   {"url": "https://github.com/leanprover-community/quote4",
    "type": "git",
    "subDir": null,
-   "rev": "64365c656d5e1bffa127d2a1795f471529ee0178",
+   "rev": "a7bfa63f5dddbcab2d4e0569c4cac74b2585e2c6",
    "name": "Qq",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
@@ -22,25 +22,25 @@
   {"url": "https://github.com/leanprover-community/aesop",
    "type": "git",
    "subDir": null,
-   "rev": "5fefb40a7c9038a7150e7edd92e43b1b94c49e79",
+   "rev": "882561b77bd2aaa98bd8665a56821062bdb3034c",
    "name": "aesop",
    "manifestFile": "lake-manifest.json",
    "inputRev": "master",
    "inherited": true,
-   "configFile": "lakefile.lean"},
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/ProofWidgets4",
    "type": "git",
    "subDir": null,
-   "rev": "fb65c476595a453a9b8ffc4a1cea2db3a89b9cd8",
+   "rev": "e6b6247c61280c77ade6bbf0bc3c66a44fe2e0c5",
    "name": "proofwidgets",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "v0.0.30",
+   "inputRev": "v0.0.36",
    "inherited": true,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/leanprover/lean4-cli",
    "type": "git",
    "subDir": null,
-   "rev": "be8fa79a28b8b6897dce0713ef50e89c4a0f6ef5",
+   "rev": "a11566029bd9ec4f68a65394e8c3ff1af74c1a29",
    "name": "Cli",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
@@ -49,25 +49,25 @@
   {"url": "https://github.com/leanprover-community/import-graph.git",
    "type": "git",
    "subDir": null,
-   "rev": "61a79185b6582573d23bf7e17f2137cd49e7e662",
+   "rev": "1588be870b9c76fe62286e8f42f0b4dafa154c96",
    "name": "importGraph",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
    "inherited": true,
-   "configFile": "lakefile.lean"},
+   "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/mathlib4",
    "type": "git",
    "subDir": null,
-   "rev": "93904a0d036e5321062ae5e705e8a893da24d81b",
+   "rev": "403385804e70ec50fc373b8c349176dcd8333419",
    "name": "mathlib",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "lecopivo/fun_trans",
+   "inputRev": "lecopivo/fun_prop_fixes2",
    "inherited": false,
    "configFile": "lakefile.lean"},
   {"url": "https://github.com/lecopivo/LeanColls.git",
    "type": "git",
    "subDir": null,
-   "rev": "907d7f1ea8d59a7d8fe15fcbbea2d5fe7638da95",
+   "rev": "8f5aa8574f0aeca250009fb0a2c64184f1679a55",
    "name": "leancolls",
    "manifestFile": "lake-manifest.json",
    "inputRev": "main",
diff --git a/lakefile.lean b/lakefile.lean
index 7df9050b..79cdb65b 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -14,7 +14,6 @@ lean_lib CompileTactics where
   precompileModules := true
   roots := #[`SciLean.Tactic.LSimp.LetNormalize,`SciLean.Tactic.MathlibCompiledTactics]
 
-
 lean_exe Doodle {
   root := `examples.Doodle
 }
@@ -58,7 +57,7 @@ lean_exe MNISTClassifier where
 meta if get_config? doc = some "dev" then -- do not download and build doc-gen4 by default
 require «doc-gen4» from git "https://github.com/leanprover/doc-gen4" @ "master"
 
-require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "lecopivo/fun_trans"
+require mathlib from git "https://github.com/leanprover-community/mathlib4" @ "lecopivo/fun_prop_fixes2"
 require leancolls from git "https://github.com/lecopivo/LeanColls.git" @ "main"
 
 set_option linter.unusedVariables false
diff --git a/lean-toolchain b/lean-toolchain
index 9ad30404..29c0cea4 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:v4.7.0
+leanprover/lean4:v4.9.0-rc2
diff --git a/test/lsimp_basic_tests.lean b/test/lsimp_basic_tests.lean
index c397c591..4dd8d121 100644
--- a/test/lsimp_basic_tests.lean
+++ b/test/lsimp_basic_tests.lean
@@ -145,6 +145,8 @@ elab "timeTactic" t:conv : conv => do
 --     unfold scalarGradient
 --     timeTactic lsimp
 
+
+set_option trace.Meta.Tactic.fun_trans true in
 #check (∇ x : Float,
           let x1 := x * x
           let x2 := x * x1
@@ -152,6 +154,7 @@ elab "timeTactic" t:conv : conv => do
           let x4 := x * x3
           let x5 := x * x4
           let x6 := x * x5
+          -- let x7 := x * x6
           -- let x8 := x * x7
           -- let x9 := x * x8
           -- let x10 := x * x9