unfold parDistribFwdDeriv Distribution.bind
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
⊢ (parDistribFwdDeriv fun x => Distribution.bind (g x) (f x) L) = fun x dx =>
    let ydy := parDistribFwdDeriv g x dx;
    let zdz := fun y => parDistribFwdDeriv (fun x => f x y) x dx;
    Distribution.bind ydy zdz
      (fun x ⊸[R]
        match x with
        | (r, dr) =>
          fun x ⊸[R]
            match x with
            | (s, ds) => ((L r) s, (L r) ds + (L dr) s))
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 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));
      let z :=
        postComp ((fun x => fun φ ⊸[R] ⟪g x, fun x_1 => ⟪f x x_1, ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v]⟫[L]) x)
          (fun z ⊸[R] (z, 0));
      z + dz) =
    fun x dx =>
    let ydy :=
      let dz := postComp (parDistribDeriv g x dx) (fun dz ⊸[R] (0, dz));
      let z := postComp (g x) (fun z ⊸[R] (z, 0));
      z + dz;
    let zdz := fun y =>
      let dz := postComp (parDistribDeriv (fun x => f x y) x dx) (fun dz ⊸[R] (0, dz));
      let z := postComp ((fun x => f x y) x) (fun z ⊸[R] (z, 0));
      z + dz;
    fun φ ⊸[R]
      ⟪ydy, fun x =>
        ⟪zdz x, ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v]⟫[fun x ⊸[R]
          match x with
          | (r, dr) =>
            fun x ⊸[R]
              match x with
              | (s, ds) => ((L r) s, (L r) ds + (L dr) s)]