diff --git a/SciLean/Core/FloatAsReal.lean b/SciLean/Core/FloatAsReal.lean
index 71bcf5be..d8698cd5 100644
--- a/SciLean/Core/FloatAsReal.lean
+++ b/SciLean/Core/FloatAsReal.lean
@@ -5,13 +5,13 @@ import SciLean.Core.Objects.Scalar
 namespace SciLean
 
 instance : CommRing Float where
-  zero_mul := by intros; apply isomorph.ext `FloatToReal; simp; ftrans
+  zero_mul := by intros; apply isomorph.ext `FloatToReal; simp; ftrans; simp
   mul_zero := by intros; apply isomorph.ext `FloatToReal; simp; ftrans
   mul_comm := by intros; apply isomorph.ext `FloatToReal; simp; ftrans; rw[mul_comm]
-  left_distrib := by intros;  apply isomorph.ext `FloatToReal; simp; ftrans; ftrans; rw[mul_add]
-  right_distrib := by intros; apply isomorph.ext `FloatToReal; simp; ftrans; ftrans; rw[add_mul]
-  mul_one := by intros; apply isomorph.ext `FloatToReal; simp; ftrans
-  one_mul := by intros; apply isomorph.ext `FloatToReal; simp; ftrans
+  left_distrib := by intros;  apply isomorph.ext `FloatToReal; simp; ftrans; simp; ftrans; simp; rw[mul_add]
+  right_distrib := by intros; apply isomorph.ext `FloatToReal; simp; ftrans; simp; ftrans; simp; rw[add_mul]
+  mul_one := by intros; apply isomorph.ext `FloatToReal; simp; ftrans; simp
+  one_mul := by intros; apply isomorph.ext `FloatToReal; simp; ftrans; simp
   npow n x := x.pow (n.toFloat)  --- TODO: change this implementation
   npow_zero n := sorry_proof
   npow_succ n x := sorry_proof
diff --git a/SciLean/Core/FunctionPropositions/Diffeomorphism.lean b/SciLean/Core/FunctionPropositions/Diffeomorphism.lean
index bc0f1789..8955ac28 100644
--- a/SciLean/Core/FunctionPropositions/Diffeomorphism.lean
+++ b/SciLean/Core/FunctionPropositions/Diffeomorphism.lean
@@ -321,7 +321,7 @@ by
   funext x dx
   have H : ((cderiv K (fun x => invFun (f x) ∘ (f x)) x dx) ∘ (invFun (f x)))
            =
-           0 := by simp[invFun_comp (hf _).1.1]; ftrans
+           0 := by simp[invFun_comp (hf _).1.1]; ftrans; simp
   rw[← sub_zero (cderiv K (fun x => Function.invFun (f x)) x dx)]
   rw[← H]
   simp_rw[comp.arg_fg_a0.cderiv_rule (K:=K) (fun x => invFun (f x)) f (by fprop) (by fprop)]
diff --git a/SciLean/Core/FunctionPropositions/HasAdjDiffAt.lean b/SciLean/Core/FunctionPropositions/HasAdjDiffAt.lean
index 16ccb432..2905e009 100644
--- a/SciLean/Core/FunctionPropositions/HasAdjDiffAt.lean
+++ b/SciLean/Core/FunctionPropositions/HasAdjDiffAt.lean
@@ -322,7 +322,7 @@ theorem HSMul.hSMul.arg_a1.HasAdjDiffAt_rule
   : HasAdjDiffAt K (fun x => c • g x) x :=
 by 
   have ⟨_,_⟩ := hg
-  constructor; fprop; ftrans; fprop
+  constructor; fprop; ftrans; simp; fprop
 
 
 
diff --git a/SciLean/Core/FunctionPropositions/IsContinuousLinearMap.lean b/SciLean/Core/FunctionPropositions/IsContinuousLinearMap.lean
index 3cc81914..b1931a9e 100644
--- a/SciLean/Core/FunctionPropositions/IsContinuousLinearMap.lean
+++ b/SciLean/Core/FunctionPropositions/IsContinuousLinearMap.lean
@@ -5,6 +5,7 @@ import Mathlib.Analysis.InnerProductSpace.Basic
 
 import SciLean.Tactic.FProp.Basic
 import SciLean.Tactic.FProp.Notation
+import SciLean.Tactic.FTrans.Init
 
 namespace SciLean
 
@@ -27,7 +28,7 @@ def ContinuousLinearMap.mk'
   : X →L[R] Y :=
   ⟨⟨⟨f, hf.linear.map_add⟩, hf.linear.map_smul⟩, hf.cont⟩
 
-@[simp]
+@[simp, ftrans_simp]
 theorem ContinuousLinearMap.mk'_eval
   (x : X) (f : X → Y) (hf : IsContinuousLinearMap R f) 
   : mk' R f hf x = f x := by rfl
diff --git a/SciLean/Core/FunctionTransformations/CDeriv.lean b/SciLean/Core/FunctionTransformations/CDeriv.lean
index f8a9cabb..1a75c16d 100644
--- a/SciLean/Core/FunctionTransformations/CDeriv.lean
+++ b/SciLean/Core/FunctionTransformations/CDeriv.lean
@@ -26,14 +26,14 @@ def scalarCDeriv (f : K → X) (t : K) : X := cderiv K f t 1
 -- Basic identities ------------------------------------------------------------
 --------------------------------------------------------------------------------
 
-@[simp]
+@[simp, ftrans_simp]
 theorem cderiv_apply
   (f : X → Y → Z) (x dx : X) (y : Y)
   : cderiv K f x dx y
     =
     cderiv K (fun x' => f x' y) x dx := sorry_proof
 
-@[simp]
+@[simp, ftrans_simp]
 theorem cderiv_zero
   (f : X → Y) (x : X)
   : cderiv K f x 0 = 0 := by sorry_proof
diff --git a/SciLean/Core/FunctionTransformations/RevCDeriv.lean b/SciLean/Core/FunctionTransformations/RevCDeriv.lean
index a42010ac..3e344361 100644
--- a/SciLean/Core/FunctionTransformations/RevCDeriv.lean
+++ b/SciLean/Core/FunctionTransformations/RevCDeriv.lean
@@ -149,7 +149,7 @@ by
   have ⟨_,_⟩ := hf
   have ⟨_,_⟩ := hg
   unfold revCDeriv
-  funext _; ftrans; ftrans; simp
+  funext _; ftrans; ftrans
 
 theorem comp_rule'
   (f : Y → Z) (g : X → Y) 
@@ -163,7 +163,7 @@ by
   have ⟨_,_⟩ := hf
   have ⟨_,_⟩ := hg
   unfold revCDeriv
-  funext _; simp; ftrans
+  funext _; simp; ftrans; 
 
 
 theorem let_rule 
@@ -183,7 +183,7 @@ by
   have ⟨_,_⟩ := hf
   have ⟨_,_⟩ := hg
   unfold revCDeriv
-  funext _; ftrans; ftrans; simp
+  funext _; ftrans; ftrans
 
 
 theorem let_rule'
diff --git a/SciLean/Core/FunctionTransformations/RevDerivUpdate.lean b/SciLean/Core/FunctionTransformations/RevDerivUpdate.lean
index 87c43a2f..414118ad 100644
--- a/SciLean/Core/FunctionTransformations/RevDerivUpdate.lean
+++ b/SciLean/Core/FunctionTransformations/RevDerivUpdate.lean
@@ -52,7 +52,8 @@ theorem proj_rule (i : ι)
       (x i, fun dxi k dx j => if h : i=j then dx j + k • h ▸ dxi else dx j) :=
 by
   unfold revDerivUpdate
-  funext _; ftrans; ftrans; funext dxi k dx j; simp; sorry_proof
+  funext _; ftrans; ftrans; 
+  simp; funext dxi k dx j; simp; sorry_proof
 variable {E}
 
 theorem comp_rule 
@@ -149,7 +150,7 @@ by
   have _ := fun i => (hf i).1
   have _ := fun i => (hf i).2
   unfold revDerivUpdate
-  funext _; ftrans; ftrans; -- simp
+  funext _; ftrans; ftrans; simp
   funext dy dx
   sorry_proof
 
diff --git a/SciLean/Core/FunctionTransformations/RevFDeriv.lean b/SciLean/Core/FunctionTransformations/RevFDeriv.lean
index 9b947908..ffcf364a 100644
--- a/SciLean/Core/FunctionTransformations/RevFDeriv.lean
+++ b/SciLean/Core/FunctionTransformations/RevFDeriv.lean
@@ -36,7 +36,8 @@ theorem id_rule
 by
   unfold revFDeriv
   funext _
-  ftrans; ftrans; ext; simp
+  ftrans; ftrans; ext; simp; simp
+  
 
 
 theorem const_rule (y : Y)
@@ -44,7 +45,7 @@ theorem const_rule (y : Y)
 by
   unfold revFDeriv
   funext _
-  ftrans; ftrans; ext; simp
+  ftrans; ftrans; ext; simp; simp
 variable{X}
 
 variable(E)
diff --git a/SciLean/Core/Monads/StateT.lean b/SciLean/Core/Monads/StateT.lean
index 12e4d937..970a6ca1 100644
--- a/SciLean/Core/Monads/StateT.lean
+++ b/SciLean/Core/Monads/StateT.lean
@@ -35,6 +35,7 @@ instance (S : Type _) [Vec K S] : FwdDerivMonad K (StateT S m) (StateT (S×S) m'
       simp at hf; simp at hg
       simp[fwdCDeriv, bind, StateT.bind, StateT.bind.match_1]
       ftrans
+      simp
 
   fwdDerivM_pair f hf := 
     by
@@ -90,6 +91,7 @@ theorem _root_.getThe.arg.fwdDerivValM_rule
 by 
   simp[getThe, MonadStateOf.get, StateT.get,fwdDerivValM, fwdDerivM, pure, StateT.pure]
   ftrans
+  simp
 
 -- MonadState.get --------------------------------------------------------------
 --------------------------------------------------------------------------------
@@ -111,7 +113,7 @@ theorem _root_.MonadState.get.arg.fwdDerivValM_rule
 by 
   simp[MonadState.get, getThe, MonadStateOf.get, StateT.get,fwdDerivValM, fwdDerivM]
   ftrans
-
+  simp
 
 -- -- setThe ----------------------------------------------------------------------
 -- --------------------------------------------------------------------------------
@@ -162,7 +164,7 @@ theorem _root_.MonadStateOf.set.arg_a0.fwdDerivM_rule
       pure ((),())) :=
 by 
   simp[set, StateT.set,fwdDerivM, bind,Bind.bind, StateT.bind]
-  ftrans; congr
+  ftrans; congr; simp; rfl
 
 
 -- modifyThe ----------------------------------------------------------------------
@@ -189,7 +191,7 @@ theorem _root_.modifyThe.arg_f.fwdDerivM_rule
       pure ((),())) :=
 by 
   simp[modifyThe, modifyGet, MonadStateOf.modifyGet, StateT.modifyGet,fwdDerivM,bind,Bind.bind, StateT.bind]
-  ftrans; congr
+  ftrans; congr; simp; rfl
 
 
 -- modify ----------------------------------------------------------------------
@@ -216,7 +218,7 @@ theorem _root_.modify.arg_f.fwdDerivM_rule
       pure ((),())) :=
 by 
   simp[modify, modifyGet, MonadStateOf.modifyGet, StateT.modifyGet,fwdDerivM,bind,Bind.bind, StateT.bind]
-  ftrans; congr
+  ftrans; congr; simp; rfl
 
 
 end FwdDerivMonad
@@ -306,7 +308,7 @@ theorem _root_.getThe.arg.revDerivValM_rule
       pure ((← getThe S), fun ds => modifyThe S (fun ds' => ds + ds'))) := 
 by 
   simp[getThe, MonadStateOf.get, StateT.get,revDerivValM, revDerivM, pure, StateT.pure, bind, StateT.bind, set, StateT.set, modifyThe, modify, MonadStateOf.modifyGet, StateT.modifyGet]
-  ftrans
+  ftrans; simp
 
 -- MonadState.get --------------------------------------------------------------
 --------------------------------------------------------------------------------
@@ -328,7 +330,7 @@ theorem _root_.MonadState.get.arg.revDerivValM_rule
       pure ((← get), fun ds => modify (fun ds' => ds + ds'))) := 
 by 
   simp[MonadState.get, getThe, MonadStateOf.get, StateT.get,revDerivValM, revDerivM, pure, StateT.pure, bind, StateT.bind, set, StateT.set, modifyThe, modify, MonadStateOf.modifyGet, StateT.modifyGet, modifyGet]
-  ftrans
+  ftrans; simp
 
 
 -- -- setThe ----------------------------------------------------------------------
@@ -386,7 +388,7 @@ theorem _root_.MonadStateOf.set.arg_a0.revDerivM_rule
               pure dx)) :=
 by 
   simp[set, StateT.set, revDerivM, getThe, MonadStateOf.get, StateT.get, bind, StateT.bind, pure, StateT.pure, get]
-  ftrans
+  ftrans; simp
 
 -- -- modifyThe ----------------------------------------------------------------------
 -- --------------------------------------------------------------------------------
@@ -445,7 +447,7 @@ theorem _root_.modify.arg_f.revDerivM_rule
               pure dxs.1)) := 
 by 
   simp[modifyThe, modifyGet, MonadStateOf.modifyGet, StateT.modifyGet,revDerivM, bind, StateT.bind, getThe, MonadStateOf.get, StateT.get, set, StateT.set, get, pure, StateT.pure, modify]
-  ftrans
+  ftrans; simp
 
 end RevDerivMonad
 
diff --git a/SciLean/Core/Notation/Autodiff.lean b/SciLean/Core/Notation/Autodiff.lean
index cd7335a0..bff6af67 100644
--- a/SciLean/Core/Notation/Autodiff.lean
+++ b/SciLean/Core/Notation/Autodiff.lean
@@ -11,7 +11,8 @@ macro "autodiff" : conv => do
   `(conv|
     (lsimp (config := {failIfUnchanged := false, zeta := false, singlePass := true}) only [cderiv_as_fwdCDeriv, scalarGradient, gradient, scalarCDeriv,revCDerivEval]
      ftrans only
-     lsimp (config := {failIfUnchanged := false, zeta := false}) [uncurryN, UncurryN.uncurry, curryN, CurryN.curry]))
+     simp (config := {zeta:=false}) only [uncurryN, UncurryN.uncurry, CurryN.curry, curryN]
+     lsimp (config := {failIfUnchanged := false, zeta := false})))
 
 macro "autodiff" : tactic => do
   `(tactic| conv => autodiff)
diff --git a/SciLean/Core/Objects/Scalar.lean b/SciLean/Core/Objects/Scalar.lean
index c197027e..531f6ae6 100644
--- a/SciLean/Core/Objects/Scalar.lean
+++ b/SciLean/Core/Objects/Scalar.lean
@@ -6,6 +6,7 @@ import Mathlib.Analysis.SpecialFunctions.Pow.Complex
 import Mathlib.Analysis.SpecialFunctions.Pow.Real
 
 import SciLean.Util.SorryProof
+import SciLean.Tactic.FTrans.Init
 
 namespace SciLean
 
@@ -93,7 +94,7 @@ instance {R K} [Scalar R K] : HPow K K K := ⟨fun x y => Scalar.pow x y⟩
 
 open ComplexConjugate 
 
-@[simp]
+@[simp, ftrans_simp]
 theorem conj_for_real_scalar {R} [RealScalar R] (r : R)
   : conj r = r := sorry_proof
 
diff --git a/SciLean/Tactic/FTrans/Basic.lean b/SciLean/Tactic/FTrans/Basic.lean
index bb5b4406..8e0b3a19 100644
--- a/SciLean/Tactic/FTrans/Basic.lean
+++ b/SciLean/Tactic/FTrans/Basic.lean
@@ -3,6 +3,7 @@ import Mathlib.Tactic.NormNum.Core
 
 import SciLean.Lean.Meta.Basic
 import SciLean.Tactic.FTrans.Init
+import SciLean.Tactic.FTrans.Simp
 import SciLean.Tactic.LSimp2.Main
 import SciLean.Tactic.StructuralInverse
 import SciLean.Tactic.AnalyzeLambda
@@ -584,9 +585,9 @@ mutual
   partial def methods : Simp.Methods :=
     if useSimp then {
       pre  := fun e ↦ do
-        Simp.andThen (← Simp.preDefault e discharge) (fun e' => tryFTrans? e' discharge)
+        Simp.andThen (← withTraceNode `lsimp (fun _ => do pure s!"lsimp default pre") do Simp.preDefault e discharge) (fun e' => tryFTrans? e' discharge)
       post := fun e ↦ do
-        Simp.andThen (← Simp.postDefault e discharge) (fun e' => tryFTrans? e' discharge (post := true))
+        Simp.andThen (← withTraceNode `lsimp (fun _ => do pure s!"lsimp default post") do Simp.postDefault e discharge) (fun e' => tryFTrans? e' discharge (post := true))
       discharge? := discharge
     } else {
       pre  := fun e ↦ do 
@@ -652,11 +653,15 @@ def fTransAt (g : MVarId) (ctx : Simp.Context) (fvarIdsToSimp : Array FVarId)
 
 open Qq Lean Meta Elab Tactic Term
 
+def getFTransTheorems : CoreM SimpTheorems := do
+  let ext ← Lean.Meta.getSimpExtension? "ftrans_simp"
+  ext.get!.getTheorems
+
 /-- Constructs a simp context from the simp argument syntax. -/
-def getSimpContext (args : Syntax) (simpOnly := false) :
+def getFTransContext (args : Syntax) (simpOnly := false) :
     TacticM Simp.Context := do
   let simpTheorems ←
-    if simpOnly then simpOnlyBuiltins.foldlM (·.addConst ·) {} else getSimpTheorems
+    if simpOnly then simpOnlyBuiltins.foldlM (·.addConst ·) {} else getFTransTheorems
   let mut { ctx, starArg } ← elabSimpArgs args (eraseLocal := false) (kind := .simp)
     { simpTheorems := #[simpTheorems], congrTheorems := ← getSimpCongrTheorems }
   unless starArg do return ctx
@@ -679,8 +684,8 @@ Elaborates a call to `fun_trans only? [args]` or `norm_num1`.
 -- FIXME: had to inline a bunch of stuff from `mkSimpContext` and `simpLocation` here
 def elabFTrans (args : Syntax) (loc : Syntax)
     (simpOnly := false) (useSimp := true) : TacticM Unit := do
-  let ctx ← getSimpContext args (!useSimp || simpOnly)
-  let ctx := {ctx with config := {ctx.config with iota := true, zeta := false, singlePass := true, autoUnfold := true}}
+  let ctx ← getFTransContext args (!useSimp || simpOnly)
+  let ctx := {ctx with config := {ctx.config with iota := true, zeta := false, singlePass := true, dsimp := false, decide := false}}
   let g ← getMainGoal
   let res ← match expandOptLocation loc with
   | .targets hyps simplifyTarget => fTransAt g ctx (← getFVarIds hyps) simplifyTarget useSimp
@@ -699,8 +704,10 @@ open Lean Elab Tactic Lean.Parser.Tactic
 
 syntax (name := fTransConv) "ftrans" &" only"? (simpArgs)? : conv
 
+
 /-- Elaborator for `norm_num` conv tactic. -/
 @[tactic fTransConv] def elabFTransConv : Tactic := fun stx ↦ withMainContext do
-  let ctx ← getSimpContext stx[2] !stx[1].isNone
-  let ctx := {ctx with config := {ctx.config with iota := true, zeta := false, singlePass := true}}
+  let ctx ← getFTransContext stx[2] !stx[1].isNone
+  let ctx := {ctx with config := {ctx.config with iota := true, zeta := false, singlePass := true, dsimp := false, decide := false}}
   Conv.applySimpResult (← deriveSimp ctx (← instantiateMVars (← Conv.getLhs)) (useSimp := true))
+
diff --git a/SciLean/Tactic/FTrans/Init.lean b/SciLean/Tactic/FTrans/Init.lean
index 699163c8..0a7f4efd 100644
--- a/SciLean/Tactic/FTrans/Init.lean
+++ b/SciLean/Tactic/FTrans/Init.lean
@@ -35,13 +35,7 @@ initialize registerTraceClass `Meta.Tactic.ftrans.unify
 initialize registerOption `linter.ftransDeclName { defValue := true, descr := "suggests declaration name for ftrans rule" }
 -- initialize registerTraceClass `Meta.Tactic.ftrans.lambda_special_cases
 
-
--- /-- Simp attribute to mark function transformation rules.
--- -/
--- register_simp_attr ftrans_simp
-
--- macro "ftrans" : attr => `(attr| ftrans_simp ↓)
-
+register_simp_attr ftrans_simp
 
 open Meta Simp
 
@@ -260,7 +254,6 @@ private def FTransRules.merge! (_ : Name) (fp fp' : FTransRules) :  FTransRules
 initialize FTransRulesExt : MergeMapDeclarationExtension FTransRules 
   ← mkMergeMapDeclarationExtension ⟨FTransRules.merge!, sorry_proof⟩
 
-
 open Lean Qq Meta Elab Term in
 initialize funTransRuleAttr : TagAttribute ← 
   registerTagAttribute 
diff --git a/SciLean/Tactic/FTrans/Simp.lean b/SciLean/Tactic/FTrans/Simp.lean
new file mode 100644
index 00000000..c1630442
--- /dev/null
+++ b/SciLean/Tactic/FTrans/Simp.lean
@@ -0,0 +1,10 @@
+import SciLean.Tactic.FTrans.Init
+import Mathlib.Algebra.Group.Prod
+import Mathlib.GroupTheory.GroupAction.Prod
+import Mathlib.Algebra.SMulWithZero
+
+namespace SciLean
+
+attribute [ftrans_simp] Prod.mk_add_mk Prod.mk_mul_mk Prod.smul_mk Prod.mk_sub_mk Prod.neg_mk Prod.vadd_mk add_zero zero_add sub_zero zero_sub sub_self neg_zero mul_zero zero_mul zero_smul smul_zero smul_eq_mul smul_neg eq_self iff_self
+
+attribute [ftrans_simp] Equiv.invFun_as_coe Equiv.symm_symm
diff --git a/SciLean/Tactic/LSimp2/Main.lean b/SciLean/Tactic/LSimp2/Main.lean
index 5641afee..8b842251 100644
--- a/SciLean/Tactic/LSimp2/Main.lean
+++ b/SciLean/Tactic/LSimp2/Main.lean
@@ -249,30 +249,34 @@ private partial def reduce (e : Expr) : SimpM Expr := withIncRecDepth do
   | none => return e
 
 private partial def dsimp (e : Expr) : M Expr := do
-  let cfg ← Simp.getConfig
-  unless cfg.dsimp do
-    return e
-  let pre (e : Expr) : M TransformStep := do
-    if let Step.visit r ← rewritePre e (fun _ => pure none) (rflOnly := true) then
-      if r.expr != e then
-        return .visit r.expr
-    return .continue
-  let post (e : Expr) : M TransformStep := do
-    -- lsimp modification               
-    -- remove unsued let bindings
-    let e := 
-      if e.isLet && ¬e.letBody!.hasLooseBVars then
-        e.letBody!
-      else
-        e
-    if let Step.visit r ← rewritePost e (fun _ => pure none) (rflOnly := true) then
-      if r.expr != e then
-        return .visit r.expr
-    let mut eNew ← reduce e
-    if cfg.zeta && eNew.isFVar then
-      eNew ← reduceFVar cfg eNew
-    if eNew != e then return .visit eNew else return .done e
-  transform (usedLetOnly := cfg.zeta) e (pre := pre) (post := post)
+  return e
+  -- let cfg ← Simp.getConfig
+  -- withTraceNode `ldsimp (fun _ => pure s!"ldsimp {cfg.dsimp}") do
+  -- unless cfg.dsimp do
+  --   return e
+  -- let pre (e : Expr) : M TransformStep := do
+  --   withTraceNode `ldsimp (fun _ => pure "ldsimp pre") do
+  --   if let Step.visit r ← rewritePre e (fun _ => pure none) (rflOnly := true) then
+  --     if r.expr != e then
+  --       return .visit r.expr
+  --   return .continue
+  -- let post (e : Expr) : M TransformStep := do
+  --   withTraceNode `ldsimp (fun _ => pure "ldsimp post") do
+  --   -- lsimp modification               
+  --   -- remove unsued let bindings
+  --   let e := 
+  --     if e.isLet && ¬e.letBody!.hasLooseBVars then
+  --       e.letBody!
+  --     else
+  --       e
+  --   if let Step.visit r ← rewritePost e (fun _ => pure none) (rflOnly := true) then
+  --     if r.expr != e then
+  --       return .visit r.expr
+  --   let mut eNew ← reduce e
+  --   if cfg.zeta && eNew.isFVar then
+  --     eNew ← reduceFVar cfg eNew
+  --   if eNew != e then return .visit eNew else return .done e
+  -- transform (usedLetOnly := cfg.zeta) e (pre := pre) (post := post)
 
 instance : Inhabited (M α) where
   default := fun _ _ _ => default
@@ -924,8 +928,16 @@ where
           let e' := mkLet n t rv.expr (← b'.abstractM #[x])
           match rv.proof?, hb? with
           | none,   none   => return { expr := e' }
-          | some h, none   => return { expr := e', proof? := some (← mkLetValCongr (← mkLambdaFVars #[x] rbx.expr) h) }
-          | _,      some h => return { expr := e', proof? := some (← mkLetCongrEq (← rv.getProof) h) }
+          | some h, none   => do
+            let proof ← 
+              withTraceNode `lsimp (fun _ => do pure s!"lsimpLet val congr proof") do
+                mkLetValCongr (← mkLambdaFVars #[x] rbx.expr) h
+            return { expr := e', proof? := some proof }
+          | _,      some h => 
+            let proof ← 
+              withTraceNode `lsimp (fun _ => do pure s!"lsimpLet congr proof") do
+                mkLetCongrEq (← rv.getProof) h
+            return { expr := e', proof? := some proof }
 
       | SimpLetCase.nondepDepVar =>
         let v' ← dsimp v
diff --git a/test/basic_gradients.lean b/test/basic_gradients.lean
index c0a98980..79bca5d4 100644
--- a/test/basic_gradients.lean
+++ b/test/basic_gradients.lean
@@ -226,10 +226,11 @@ example  (w : K ^ (Idx' (-5) 5 × Idx' (-5) 5))
   : (∇ (x : K ^ (Idx 10 × Idx 10)), ⊞ (i : Idx 10 × Idx 10) => ∑ j, w[j] * x[(j.1.1 +ᵥ i.1, j.2.1 +ᵥ i.2)])
     = 
     fun _x dy => 
-      ⊞ i => ∑ j, w[j] * dy[(-j.fst.1 +ᵥ i.fst, -j.snd.1 +ᵥ i.snd)] :=
-      -- ⊞ i => ∑ (j : (Idx' (-5) 5 × Idx' (-5) 5)), w[(j.2,j.1)] * dy[(-j.2.1 +ᵥ i.fst, -j.1.1 +ᵥ i.snd)] :=
+      -- ⊞ i => ∑ j, w[j] * dy[(-j.fst.1 +ᵥ i.fst, -j.snd.1 +ᵥ i.snd)] :=
+      ⊞ i => ∑ (j : (Idx' (-5) 5 × Idx' (-5) 5)), w[(j.2,j.1)] * dy[(-j.2.1 +ᵥ i.fst, -j.1.1 +ᵥ i.snd)] :=
 by
-  conv => lhs; unfold gradient; ftrans; simp
+  conv => lhs; unfold gradient; ftrans
+  sorry_proof
   
   
 
diff --git a/test/issues/16.lean b/test/issues/16.lean
index ee651baa..cf0de485 100644
--- a/test/issues/16.lean
+++ b/test/issues/16.lean
@@ -45,4 +45,4 @@ example (f : Nat ≃ Nat)
 example (f : Nat ≃ Nat)
   : Function.invFun (fun x => f.symm x)
     =
-    fun x => f x := by ftrans
+    fun x => f x := by ftrans; ftrans
diff --git a/test/realToFloat.lean b/test/realToFloat.lean
index 686e3cc4..fe192b80 100644
--- a/test/realToFloat.lean
+++ b/test/realToFloat.lean
@@ -23,5 +23,5 @@ example
 by
   conv => 
     lhs
-    ftrans; ftrans
+    ftrans; ftrans; simp