simp [diracRevDeriv,revDeriv, parDistribRevDeriv, postComp]
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
φ : 𝒟 X
this : HasAdjDiff R ⇑φ
⊢ (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))))
      φ
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
φ : 𝒟 X
this : HasAdjDiff R ⇑φ
⊢ (fun dz ⊸[R] semiAdjoint R (fun dx => ∂ (x_1:=w;dx), φ (x x_1)) dz) =
    fun dr ⊸[R] semiAdjoint R (∂ x w) (semiAdjoint R (∂ ⇑φ (x w)) dr)