simp[Function.toDistribution]
case h.h.a
R : Type u_1
inst✝¹⁰ : RealScalar R
W : Type u_2
inst✝⁹ : Vec R W
inst✝⁸ : Module ℝ W
X : Type u_4
inst✝⁷ : SemiHilbert R X
inst✝⁶ : MeasureSpace X
Y : Type u_3
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.64712
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.65630
inst✝¹ : Vec R U
V : Type ?u.65651
inst✝ : Vec R V
f : W → X → Y
hf : ∀ (x : X), CDifferentiable R fun x_1 => f x_1 x
x dx : W
φ : 𝒟 X
⊢ (fun φ ⊸ ∂ (x':=x;dx), ((fun w => ↑fun x => f w x) x') φ) φ = (↑fun x_1 => ∂ (x:=x;dx), f x x_1) φ
case h.h.a
R : Type u_1
inst✝¹⁰ : RealScalar R
W : Type u_2
inst✝⁹ : Vec R W
inst✝⁸ : Module ℝ W
X : Type u_4
inst✝⁷ : SemiHilbert R X
inst✝⁶ : MeasureSpace X
Y : Type u_3
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.64712
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type ?u.65630
inst✝¹ : Vec R U
V : Type ?u.65651
inst✝ : Vec R V
f : W → X → Y
hf : ∀ (x : X), CDifferentiable R fun x_1 => f x_1 x
x dx : W
φ : 𝒟 X
⊢ ∂ (x':=x;dx), ∫' x, φ x • f x' x = ∫' x_1, φ x_1 • ∂ (x:=x;dx), f x x_1