Theorem: SciLean.parDistribFwdDeriv.bind_rule (SciLean/Core/Distribution/ParametricDistribFwdDeriv.lean)

State before:
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))
Tactic:
unfold parDistribFwdDeriv Distribution.bind
State after:
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)]

State before:
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)]
Tactic:
autodiff
State after:
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)]

State before:
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)]
Tactic:
funext x dx
State after:
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

State before:
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
Tactic:
fun_trans [action_push,fwdDeriv]
State after:
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
⊢ 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)) +
      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)) =
    fun φ ⊸[R]
      ⟪postComp (g x) (fun z ⊸[R] (z, 0)), fun x_1 =>
          ⟪postComp (f x x_1) (fun z ⊸[R] (z, 0)), ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v] +
            ⟪postComp (parDistribDeriv (fun x => f x x_1) x dx) (fun dz ⊸[R] (0, 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)] +
        ⟪postComp (parDistribDeriv g x dx) (fun dz ⊸[R] (0, dz)), fun x_1 =>
          ⟪postComp (f x x_1) (fun z ⊸[R] (z, 0)), ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v] +
            ⟪postComp (parDistribDeriv (fun x => f x x_1) x dx) (fun dz ⊸[R] (0, 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)]

State before:
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
⊢ 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)) +
      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)) =
    fun φ ⊸[R]
      ⟪postComp (g x) (fun z ⊸[R] (z, 0)), fun x_1 =>
          ⟪postComp (f x x_1) (fun z ⊸[R] (z, 0)), ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v] +
            ⟪postComp (parDistribDeriv (fun x => f x x_1) x dx) (fun dz ⊸[R] (0, 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)] +
        ⟪postComp (parDistribDeriv g x dx) (fun dz ⊸[R] (0, dz)), fun x_1 =>
          ⟪postComp (f x x_1) (fun z ⊸[R] (z, 0)), ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v] +
            ⟪postComp (parDistribDeriv (fun x => f x x_1) x dx) (fun dz ⊸[R] (0, 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)]
Tactic:
ext φ
State after:
case h.h.a.a
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
φ : 𝒟 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)) +
          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)))
        φ).1 =
    ((fun φ ⊸[R]
          ⟪postComp (g x) (fun z ⊸[R] (z, 0)), fun x_1 =>
              ⟪postComp (f x x_1) (fun z ⊸[R] (z, 0)), ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v] +
                ⟪postComp (parDistribDeriv (fun x => f x x_1) x dx) (fun dz ⊸[R] (0, 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)] +
            ⟪postComp (parDistribDeriv g x dx) (fun dz ⊸[R] (0, dz)), fun x_1 =>
              ⟪postComp (f x x_1) (fun z ⊸[R] (z, 0)), ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v] +
                ⟪postComp (parDistribDeriv (fun x => f x x_1) x dx) (fun dz ⊸[R] (0, 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)])
        φ).1

case h.h.a.a
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
φ : 𝒟 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)) +
          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)))
        φ).2 =
    ((fun φ ⊸[R]
          ⟪postComp (g x) (fun z ⊸[R] (z, 0)), fun x_1 =>
              ⟪postComp (f x x_1) (fun z ⊸[R] (z, 0)), ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v] +
                ⟪postComp (parDistribDeriv (fun x => f x x_1) x dx) (fun dz ⊸[R] (0, 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)] +
            ⟪postComp (parDistribDeriv g x dx) (fun dz ⊸[R] (0, dz)), fun x_1 =>
              ⟪postComp (f x x_1) (fun z ⊸[R] (z, 0)), ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v] +
                ⟪postComp (parDistribDeriv (fun x => f x x_1) x dx) (fun dz ⊸[R] (0, 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)])
        φ).2

State before:
case h.h.a.a
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
φ : 𝒟 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)) +
          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)))
        φ).1 =
    ((fun φ ⊸[R]
          ⟪postComp (g x) (fun z ⊸[R] (z, 0)), fun x_1 =>
              ⟪postComp (f x x_1) (fun z ⊸[R] (z, 0)), ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v] +
                ⟪postComp (parDistribDeriv (fun x => f x x_1) x dx) (fun dz ⊸[R] (0, 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)] +
            ⟪postComp (parDistribDeriv g x dx) (fun dz ⊸[R] (0, dz)), fun x_1 =>
              ⟪postComp (f x x_1) (fun z ⊸[R] (z, 0)), ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v] +
                ⟪postComp (parDistribDeriv (fun x => f x x_1) x dx) (fun dz ⊸[R] (0, 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)])
        φ).1

case h.h.a.a
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
φ : 𝒟 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)) +
          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)))
        φ).2 =
    ((fun φ ⊸[R]
          ⟪postComp (g x) (fun z ⊸[R] (z, 0)), fun x_1 =>
              ⟪postComp (f x x_1) (fun z ⊸[R] (z, 0)), ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v] +
                ⟪postComp (parDistribDeriv (fun x => f x x_1) x dx) (fun dz ⊸[R] (0, 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)] +
            ⟪postComp (parDistribDeriv g x dx) (fun dz ⊸[R] (0, dz)), fun x_1 =>
              ⟪postComp (f x x_1) (fun z ⊸[R] (z, 0)), ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v] +
                ⟪postComp (parDistribDeriv (fun x => f x x_1) x dx) (fun dz ⊸[R] (0, 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)])
        φ).2
Tactic:
simp only [ftrans_simp, action_push, postComp]
State after:
case h.h.a.a
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
φ : 𝒟 Z
⊢ ⟪g x, fun x_1 => ⟪f x x_1, ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v]⟫[L] =
    (⟪fun φ ⊸[R] ((g x) φ, 0), fun x_1 =>
          ⟪fun φ ⊸[R] ((f x x_1) φ, 0), ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v] +
            ⟪fun φ ⊸[R] (0, ∂ (x':=x;dx), (f x' x_1) φ),
              ⇑φ⟫[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)] +
        ⟪fun φ ⊸[R] (0, ∂ (x':=x;dx), (g x') φ), fun x_1 =>
          ⟪fun φ ⊸[R] ((f x x_1) φ, 0), ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v] +
            ⟪fun φ ⊸[R] (0, ∂ (x':=x;dx), (f x' x_1) φ),
              ⇑φ⟫[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)]).1

case h.h.a.a
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
φ : 𝒟 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)) +
          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)))
        φ).2 =
    ((fun φ ⊸[R]
          ⟪postComp (g x) (fun z ⊸[R] (z, 0)), fun x_1 =>
              ⟪postComp (f x x_1) (fun z ⊸[R] (z, 0)), ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v] +
                ⟪postComp (parDistribDeriv (fun x => f x x_1) x dx) (fun dz ⊸[R] (0, 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)] +
            ⟪postComp (parDistribDeriv g x dx) (fun dz ⊸[R] (0, dz)), fun x_1 =>
              ⟪postComp (f x x_1) (fun z ⊸[R] (z, 0)), ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v] +
                ⟪postComp (parDistribDeriv (fun x => f x x_1) x dx) (fun dz ⊸[R] (0, 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)])
        φ).2

State before:
case h.h.a.a
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
φ : 𝒟 Z
⊢ ⟪g x, fun x_1 => ⟪f x x_1, ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v]⟫[L] =
    (⟪fun φ ⊸[R] ((g x) φ, 0), fun x_1 =>
          ⟪fun φ ⊸[R] ((f x x_1) φ, 0), ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v] +
            ⟪fun φ ⊸[R] (0, ∂ (x':=x;dx), (f x' x_1) φ),
              ⇑φ⟫[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)] +
        ⟪fun φ ⊸[R] (0, ∂ (x':=x;dx), (g x') φ), fun x_1 =>
          ⟪fun φ ⊸[R] ((f x x_1) φ, 0), ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v] +
            ⟪fun φ ⊸[R] (0, ∂ (x':=x;dx), (f x' x_1) φ),
              ⇑φ⟫[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)]).1

case h.h.a.a
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
φ : 𝒟 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)) +
          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)))
        φ).2 =
    ((fun φ ⊸[R]
          ⟪postComp (g x) (fun z ⊸[R] (z, 0)), fun x_1 =>
              ⟪postComp (f x x_1) (fun z ⊸[R] (z, 0)), ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v] +
                ⟪postComp (parDistribDeriv (fun x => f x x_1) x dx) (fun dz ⊸[R] (0, 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)] +
            ⟪postComp (parDistribDeriv g x dx) (fun dz ⊸[R] (0, dz)), fun x_1 =>
              ⟪postComp (f x x_1) (fun z ⊸[R] (z, 0)), ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v] +
                ⟪postComp (parDistribDeriv (fun x => f x x_1) x dx) (fun dz ⊸[R] (0, 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)])
        φ).2
Tactic:
sorry_proof
State after:
case h.h.a.a
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
φ : 𝒟 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)) +
          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)))
        φ).2 =
    ((fun φ ⊸[R]
          ⟪postComp (g x) (fun z ⊸[R] (z, 0)), fun x_1 =>
              ⟪postComp (f x x_1) (fun z ⊸[R] (z, 0)), ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v] +
                ⟪postComp (parDistribDeriv (fun x => f x x_1) x dx) (fun dz ⊸[R] (0, 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)] +
            ⟪postComp (parDistribDeriv g x dx) (fun dz ⊸[R] (0, dz)), fun x_1 =>
              ⟪postComp (f x x_1) (fun z ⊸[R] (z, 0)), ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v] +
                ⟪postComp (parDistribDeriv (fun x => f x x_1) x dx) (fun dz ⊸[R] (0, 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)])
        φ).2

State before:
case h.h.a.a
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
φ : 𝒟 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)) +
          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)))
        φ).2 =
    ((fun φ ⊸[R]
          ⟪postComp (g x) (fun z ⊸[R] (z, 0)), fun x_1 =>
              ⟪postComp (f x x_1) (fun z ⊸[R] (z, 0)), ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v] +
                ⟪postComp (parDistribDeriv (fun x => f x x_1) x dx) (fun dz ⊸[R] (0, 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)] +
            ⟪postComp (parDistribDeriv g x dx) (fun dz ⊸[R] (0, dz)), fun x_1 =>
              ⟪postComp (f x x_1) (fun z ⊸[R] (z, 0)), ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v] +
                ⟪postComp (parDistribDeriv (fun x => f x x_1) x dx) (fun dz ⊸[R] (0, 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)])
        φ).2
Tactic:
sorry_proof
State after:
no goals