Theorem: SciLean.parDistribFwdDeriv.bind_rule
Proof 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]
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
⊢ ⟪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