funext x dx
R : Type u_1
inst✝⁸ : RealScalar R
W : Type u_6
inst✝⁷ : Vec R W
X : Type u_7
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_5
inst✝¹ : Vec R U
V : Type u_3
inst✝ : Vec R V
f : X → Y → 𝒟'(Z, V)
g : X → 𝒟'(Y, U)
L : U ⊸[R] V ⊸[R] W
hf :
  DistribDifferentiable fun x =>
    match x with
    | (x, y) => f x y
hg : DistribDifferentiable g
⊢ (fun x =>
      let z :=
        postComp (fun φ ⊸[R] ⟪g x, fun x_1 => ⟪f x x_1, ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v]⟫[L]) (fun z ⊸[R] (z, 0));
      fun dx =>
      let dz :=
        postComp
          (parDistribDeriv (fun x => fun φ ⊸[R] ⟪g x, fun x_1 => ⟪f x x_1, ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v]⟫[L]) x dx)
          (fun dz ⊸[R] (0, dz));
      z + dz) =
    fun x =>
    let z := postComp (g x) (fun z ⊸[R] (z, 0));
    fun dx =>
    let dz := postComp (parDistribDeriv g x dx) (fun dz ⊸[R] (0, dz));
    let ydy := z + dz;
    fun φ ⊸[R]
      ⟪ydy, fun x_1 =>
        let dz := postComp (parDistribDeriv (fun x => f x x_1) x dx) (fun dz ⊸[R] (0, dz));
        let z := postComp (f x x_1) (fun z ⊸[R] (z, 0));
        ⟪z + dz,
          ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v]⟫[fun x ⊸[R] fun x_1 ⊸[R] ((L x.1) x_1.1, (L x.1) x_1.2 + (L x.2) x_1.1)]
case h.h
R : Type u_1
inst✝⁸ : RealScalar R
W : Type u_6
inst✝⁷ : Vec R W
X : Type u_7
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_5
inst✝¹ : Vec R U
V : Type u_3
inst✝ : Vec R V
f : X → Y → 𝒟'(Z, V)
g : X → 𝒟'(Y, U)
L : U ⊸[R] V ⊸[R] W
hf :
  DistribDifferentiable fun x =>
    match x with
    | (x, y) => f x y
hg : DistribDifferentiable g
x dx : X
⊢ (let z := postComp (fun φ ⊸[R] ⟪g x, fun x_1 => ⟪f x x_1, ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v]⟫[L]) (fun z ⊸[R] (z, 0));
      fun dx =>
      let dz :=
        postComp
          (parDistribDeriv (fun x => fun φ ⊸[R] ⟪g x, fun x_1 => ⟪f x x_1, ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v]⟫[L]) x dx)
          (fun dz ⊸[R] (0, dz));
      z + dz)
      dx =
    (let z := postComp (g x) (fun z ⊸[R] (z, 0));
      fun dx =>
      let dz := postComp (parDistribDeriv g x dx) (fun dz ⊸[R] (0, dz));
      let ydy := z + dz;
      fun φ ⊸[R]
        ⟪ydy, fun x_1 =>
          let dz := postComp (parDistribDeriv (fun x => f x x_1) x dx) (fun dz ⊸[R] (0, dz));
          let z := postComp (f x x_1) (fun z ⊸[R] (z, 0));
          ⟪z + dz,
            ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v]⟫[fun x ⊸[R] fun x_1 ⊸[R] ((L x.1) x_1.1, (L x.1) x_1.2 + (L x.2) x_1.1)])
      dx