unfold parDistribDeriv postComp Function.toDistribution
case h.h
R : Type u_1
inst✝¹² : RealScalar R
W : Type u_2
inst✝¹¹ : Vec R W
X : Type u_3
inst✝¹⁰ : Vec R X
inst✝⁹ : MeasureSpace X
Y : Type u_5
inst✝⁸ : Vec R Y
inst✝⁷ : Module ℝ Y
Z : Type u_4
inst✝⁶ : Vec R Z
inst✝⁵ : Module ℝ Z
U : Type ?u.142717
inst✝⁴ : Vec R U
V : Type ?u.142738
inst✝³ : Vec R V
inst✝² : MeasureSpace X
inst✝¹ : MeasureSpace Y
inst✝ : MeasureSpace (X × Y)
f : W → X → Y → Z
w dw : W
⊢ parDistribDeriv (fun w => ↑fun x => ∫' y, f w x y) w dw =
    let Tf := fun w => ↑fun x => ↑fun y => f w x y;
    postComp (parDistribDeriv Tf w dw) (fun T ⊸[R] ⟪T, fun x => 1⟫[fun z ⊸[R] fun r ⊸[R] r • z])
case h.h
R : Type u_1
inst✝¹² : RealScalar R
W : Type u_2
inst✝¹¹ : Vec R W
X : Type u_3
inst✝¹⁰ : Vec R X
inst✝⁹ : MeasureSpace X
Y : Type u_5
inst✝⁸ : Vec R Y
inst✝⁷ : Module ℝ Y
Z : Type u_4
inst✝⁶ : Vec R Z
inst✝⁵ : Module ℝ Z
U : Type ?u.142717
inst✝⁴ : Vec R U
V : Type ?u.142738
inst✝³ : Vec R V
inst✝² : MeasureSpace X
inst✝¹ : MeasureSpace Y
inst✝ : MeasureSpace (X × Y)
f : W → X → Y → Z
w dw : W
⊢ (fun φ ⊸ ∂ (x':=w;dw), ((fun w => fun φ ⊸[R] ∫' x, φ x • (fun x => ∫' y, f w x y) x) x') φ) =
    let Tf := fun w => fun φ ⊸[R] ∫' x, φ x • (fun x => fun φ ⊸[R] ∫' x_1, φ x_1 • (fun y => f w x y) x_1) x;
    fun φ ⊸[R] (fun T ⊸[R] ⟪T, fun x => 1⟫[fun z ⊸[R] fun r ⊸[R] r • z]) ((fun φ ⊸ ∂ (x':=w;dw), (Tf x') φ) φ)