diff --git a/SciLean/Modules/Prob/DistribDeriv/DistribFwdDeriv.lean b/SciLean/Modules/Prob/DistribDeriv/DistribFwdDeriv.lean
index f615720b..328bfd91 100644
--- a/SciLean/Modules/Prob/DistribDeriv/DistribFwdDeriv.lean
+++ b/SciLean/Modules/Prob/DistribDeriv/DistribFwdDeriv.lean
@@ -1,3 +1,4 @@
+import SciLean.Core.FunctionTransformations
 import SciLean.Modules.Prob.DistribDeriv.DistribDeriv
 
 namespace SciLean.Prob
diff --git a/SciLean/Modules/Prob/DistribDeriv/Measure.lean b/SciLean/Modules/Prob/DistribDeriv/Measure.lean
index 691e9863..4f1edb56 100644
--- a/SciLean/Modules/Prob/DistribDeriv/Measure.lean
+++ b/SciLean/Modules/Prob/DistribDeriv/Measure.lean
@@ -45,8 +45,10 @@ theorem measure.distribDeriv_comp
     ⟪distribDeriv (fun y => (μ y).toDistribution) y dy, φ⟫ := by
 
   simp [distribDeriv]
-  rw [fderiv.comp_rule_at ℝ (fun y => ∫ (x : Z), φ x ∂(μ y)) f x hφ.diff hf]
-  dsimp
+  have h := fderiv.comp (𝕜:=ℝ) (x:=x) (g:=fun y => ∫ (x : Z), φ x ∂(μ y)) (f:=f) hφ.diff hf
+  -- rw[h] -- ugh
+  -- rw [fderiv.comp x (g:=fun y => ∫ (x : Z), φ x ∂(μ y)) (f:=f)f x hφ.diff hf]
+  sorry -- dsimp
 
 
 @[simp ↓]