simp (disch := assumption) only [distribution_action_normalize, distribDeriv_comp]
W : Type u_1
inst✝¹¹ : NormedAddCommGroup W
inst✝¹⁰ : NormedSpace ℝ W
inst✝⁹ : CompleteSpace W
X : Type u_3
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace ℝ X
inst✝⁶ : CompleteSpace X
Y : Type u_2
inst✝⁵ : NormedAddCommGroup Y
inst✝⁴ : NormedSpace ℝ Y
inst✝³ : CompleteSpace Y
Z : Type u_1
inst✝² : NormedAddCommGroup Z
inst✝¹ : NormedSpace ℝ Z
inst✝ : CompleteSpace Z
f : Y → Distribution Z
g : X → Y
x dx : X
φ : Z → W × W
hf : DistribDifferentiable f
hg : DifferentiableAt ℝ g x
⊢ ((f (g x)).action fun x => (φ x).1,
      ((distribDeriv (fun x => f (g x)) x dx).action fun x => (φ x).1) + (f (g x)).action fun x => (φ x).2) =
    ((f (g x)).action fun x => (φ x).1,
      ((distribDeriv f (g x) ((fderiv ℝ g x) dx)).action fun x => (φ x).1) + (f (g x)).action fun x => (φ x).2)
no goals