simp
R : Type u_1
inst✝⁸ : RealScalar R
W : Type ?u.8636
inst✝⁷ : SemiInnerProductSpace R W
X : Type u_5
inst✝⁶ : SemiInnerProductSpace R X
Y : Type u_4
inst✝⁵ : SemiInnerProductSpace R Y
inst✝⁴ : Module ℝ Y
Z : Type u_2
inst✝³ : SemiInnerProductSpace R Z
inst✝² : Module ℝ Z
U : Type u_3
inst✝¹ : SemiInnerProductSpace R U
V : Type ?u.10463
inst✝ : SemiInnerProductSpace R V
f : Y → 𝒟'(Z, U)
g : X → Y
hf : DistribDifferentiable f
hg : HasAdjDiff R g
⊢ (parDistribRevDeriv fun x => f (g x)) = fun x =>
    let ydg := revDeriv' R g x;
    let udf := parDistribRevDeriv f ydg.1;
    postComp udf (fun udf' ⊸[R] (udf'.1, fun du ⊸[R] ydg.2 (udf'.2 du)))
R : Type u_1
inst✝⁸ : RealScalar R
W : Type ?u.8636
inst✝⁷ : SemiInnerProductSpace R W
X : Type u_5
inst✝⁶ : SemiInnerProductSpace R X
Y : Type u_4
inst✝⁵ : SemiInnerProductSpace R Y
inst✝⁴ : Module ℝ Y
Z : Type u_2
inst✝³ : SemiInnerProductSpace R Z
inst✝² : Module ℝ Z
U : Type u_3
inst✝¹ : SemiInnerProductSpace R U
V : Type ?u.10463
inst✝ : SemiInnerProductSpace R V
f : Y → 𝒟'(Z, U)
g : X → Y
hf : DistribDifferentiable f
hg : HasAdjDiff R g
⊢ (parDistribRevDeriv fun x => f (g x)) = fun x =>
    postComp (parDistribRevDeriv f (g x)) (fun udf' ⊸[R] (udf'.1, fun du ⊸[R] (<∂ g x).2 (udf'.2 du)))