From cc84860c875246ec5f69207ef05824a5eb0b89c1 Mon Sep 17 00:00:00 2001
From: lecopivo <skrivantomas@seznam.cz>
Date: Tue, 12 Mar 2024 15:37:48 -0400
Subject: [PATCH] fix distribution derivative

---
 SciLean/Modules/Prob/DistribDeriv/DistribFwdDeriv.lean | 1 +
 SciLean/Modules/Prob/DistribDeriv/Measure.lean         | 6 ++++--
 2 files changed, 5 insertions(+), 2 deletions(-)

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 ↓]