funext x
R : Type u_1
inst✝⁸ : RealScalar R
W : Type u_6
inst✝⁷ : SemiInnerProductSpace R W
X : Type u_7
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_5
inst✝¹ : SemiInnerProductSpace R U
V : Type u_3
inst✝ : SemiInnerProductSpace R V
f : X → Y → 𝒟'(Z, V)
g : X → 𝒟'(Y, U)
L : U ⊸[R] V ⊸[R] W
⊢ (fun x =>
      fun φ ⊸
        let df' :=
          semiAdjoint R fun dx =>
            ∂ (x:=x;dx), ((fun x => fun φ ⊸[R] ⟪g x, fun x_1 => ⟪f x x_1, ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v]⟫[L]) x) φ;
        let z := ((fun x => fun φ ⊸[R] ⟪g x, fun x_1 => ⟪f x x_1, ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v]⟫[L]) x) φ;
        (z, fun dz ⊸[R] df' dz)) =
    fun x =>
    let ydg :=
      fun φ ⊸
        let df' := semiAdjoint R fun dx => ∂ (x:=x;dx), (g x) φ;
        let z := (g x) φ;
        (z, fun dz ⊸[R] df' dz);
    let zdf := fun y =>
      fun φ ⊸
        let df' := semiAdjoint R fun dx => ∂ (x:=x;dx), ((fun x => f x y) x) φ;
        let z := ((fun x => f x y) x) φ;
        (z, fun dz ⊸[R] df' dz);
    fun φ ⊸[R]
      ⟪ydg, fun x =>
        ⟪zdf x, ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v]⟫[fun x ⊸
          match x with
          | (u, dg) =>
            fun vdf ⊸
              ((L u) vdf.1,
                fun dw ⊸[R] vdf.2 (semiAdjoint R (fun x => (L u) x) dw) + dg (semiAdjoint R (fun x => (L x) vdf.1) dw))]
case h
R : Type u_1
inst✝⁸ : RealScalar R
W : Type u_6
inst✝⁷ : SemiInnerProductSpace R W
X : Type u_7
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_5
inst✝¹ : SemiInnerProductSpace R U
V : Type u_3
inst✝ : SemiInnerProductSpace R V
f : X → Y → 𝒟'(Z, V)
g : X → 𝒟'(Y, U)
L : U ⊸[R] V ⊸[R] W
x : X
⊢ (fun φ ⊸
      let df' :=
        semiAdjoint R fun dx =>
          ∂ (x:=x;dx), ((fun x => fun φ ⊸[R] ⟪g x, fun x_1 => ⟪f x x_1, ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v]⟫[L]) x) φ;
      let z := ((fun x => fun φ ⊸[R] ⟪g x, fun x_1 => ⟪f x x_1, ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v]⟫[L]) x) φ;
      (z, fun dz ⊸[R] df' dz)) =
    let ydg :=
      fun φ ⊸
        let df' := semiAdjoint R fun dx => ∂ (x:=x;dx), (g x) φ;
        let z := (g x) φ;
        (z, fun dz ⊸[R] df' dz);
    let zdf := fun y =>
      fun φ ⊸
        let df' := semiAdjoint R fun dx => ∂ (x:=x;dx), ((fun x => f x y) x) φ;
        let z := ((fun x => f x y) x) φ;
        (z, fun dz ⊸[R] df' dz);
    fun φ ⊸[R]
      ⟪ydg, fun x =>
        ⟪zdf x, ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v]⟫[fun x ⊸
          match x with
          | (u, dg) =>
            fun vdf ⊸
              ((L u) vdf.1,
                fun dw ⊸[R] vdf.2 (semiAdjoint R (fun x => (L u) x) dw) + dg (semiAdjoint R (fun x => (L x) vdf.1) dw))]