funext w
R : Type u_1
inst✝⁸ : RealScalar R
W : Type u_2
inst✝⁷ : SemiInnerProductSpace R W
X : Type u_3
inst✝⁶ : SemiInnerProductSpace R X
Y : Type ?u.85890
inst✝⁵ : SemiInnerProductSpace R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.86767
inst✝³ : SemiInnerProductSpace R Z
inst✝² : Module ℝ Z
U : Type ?u.87639
inst✝¹ : SemiInnerProductSpace R U
V : Type ?u.87663
inst✝ : SemiInnerProductSpace R V
x : W → X
hx : HasAdjDiff R x
⊢ (parDistribRevDeriv fun w => dirac (x w)) = fun w =>
    let xdx := revDeriv' R x w;
    postComp (diracRevDeriv xdx.1)
      (fun x ⊸
        match x with
        | (r, dφ) => (r, fun dr ⊸[R] xdx.2 (dφ dr)))
case h
R : Type u_1
inst✝⁸ : RealScalar R
W : Type u_2
inst✝⁷ : SemiInnerProductSpace R W
X : Type u_3
inst✝⁶ : SemiInnerProductSpace R X
Y : Type ?u.85890
inst✝⁵ : SemiInnerProductSpace R Y
inst✝⁴ : Module ℝ Y
Z : Type ?u.86767
inst✝³ : SemiInnerProductSpace R Z
inst✝² : Module ℝ Z
U : Type ?u.87639
inst✝¹ : SemiInnerProductSpace R U
V : Type ?u.87663
inst✝ : SemiInnerProductSpace R V
x : W → X
hx : HasAdjDiff R x
w : W
⊢ parDistribRevDeriv (fun w => dirac (x w)) w =
    let xdx := revDeriv' R x w;
    postComp (diracRevDeriv xdx.1)
      (fun x ⊸
        match x with
        | (r, dφ) => (r, fun dr ⊸[R] xdx.2 (dφ dr)))