funext x
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
⊢ (fun x =>
      fun φ ⊸
        let df' := semiAdjoint R fun dx => ∂ (x:=x;dx), ((fun x => f (g x)) x) φ;
        let z := ((fun x => f (g x)) x) φ;
        (z, fun dz ⊸[R] df' dz)) =
    fun x =>
    fun φ ⊸[R]
      (fun udf' ⊸[R] (udf'.1, fun du ⊸[R] (<∂ g x).2 (udf'.2 du)))
        ((fun φ ⊸
            let df' := semiAdjoint R fun dx => ∂ (x:=g x;dx), (f x) φ;
            let z := (f (g x)) φ;
            (z, fun dz ⊸[R] df' dz))
          φ)
case h
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
x : X
⊢ (fun φ ⊸
      let df' := semiAdjoint R fun dx => ∂ (x:=x;dx), ((fun x => f (g x)) x) φ;
      let z := ((fun x => f (g x)) x) φ;
      (z, fun dz ⊸[R] df' dz)) =
    fun φ ⊸[R]
      (fun udf' ⊸[R] (udf'.1, fun du ⊸[R] (<∂ g x).2 (udf'.2 du)))
        ((fun φ ⊸
            let df' := semiAdjoint R fun dx => ∂ (x:=g x;dx), (f x) φ;
            let z := (f (g x)) φ;
            (z, fun dz ⊸[R] df' dz))
          φ)