unfold parDistribFwdDeriv
R : Type u_1
inst✝⁸ : RealScalar R
W : Type ?u.8688
inst✝⁷ : Vec R W
X : Type u_5
inst✝⁶ : Vec R X
Y : Type u_4
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type u_2
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type u_3
inst✝¹ : Vec R U
V : Type ?u.10339
inst✝ : Vec R V
f : Y → 𝒟'(Z, U)
g : X → Y
hf : DistribDifferentiable f
hg : CDifferentiable R g
⊢ (parDistribFwdDeriv fun x => f (g x)) = fun x dx =>
    let ydy := ∂> g x dx;
    parDistribFwdDeriv f ydy.1 ydy.2
R : Type u_1
inst✝⁸ : RealScalar R
W : Type ?u.8688
inst✝⁷ : Vec R W
X : Type u_5
inst✝⁶ : Vec R X
Y : Type u_4
inst✝⁵ : Vec R Y
inst✝⁴ : Module ℝ Y
Z : Type u_2
inst✝³ : Vec R Z
inst✝² : Module ℝ Z
U : Type u_3
inst✝¹ : Vec R U
V : Type ?u.10339
inst✝ : Vec R V
f : Y → 𝒟'(Z, U)
g : X → Y
hf : DistribDifferentiable f
hg : CDifferentiable R g
⊢ (fun x dx =>
      let dz := postComp (parDistribDeriv (fun x => f (g x)) x dx) (fun dz ⊸[R] (0, dz));
      let z := postComp ((fun x => f (g x)) x) (fun z ⊸[R] (z, 0));
      z + dz) =
    fun x dx =>
    let ydy := ∂> g x dx;
    let dz := postComp (parDistribDeriv f ydy.1 ydy.2) (fun dz ⊸[R] (0, dz));
    let z := postComp (f ydy.1) (fun z ⊸[R] (z, 0));
    z + dz