Theorem: SciLean.parDistribRevDeriv.bind_rule
Proof state before:
case h.a.a
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
φ : 𝒟 Z
⊢ ((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))
        φ).1 =
    ((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))])
        φ).1

case h.a.a.a
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
φ : 𝒟 Z
x✝ : W
⊢ ((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))
          φ).2
      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))])
          φ).2
      x✝
Tactic:
simp
Proof state after:
case h.a.a
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
φ : 𝒟 Z
⊢ ⟪g x, fun x_1 => ⟪f x x_1, ⇑φ⟫[fun v ⊸[R] fun r ⊸[R] r • v]⟫[L] =
    ⟪fun φ ⊸ ((g x) φ, fun dz ⊸[R] semiAdjoint R (fun dx => ∂ (x:=x;dx), (g x) φ) dz), fun x_1 =>
        ⟪fun φ ⊸ ((f x x_1) φ, fun dz ⊸[R] semiAdjoint R (fun dx => ∂ (x:=x;dx), (f x x_1) φ) dz),
          ⇑φ⟫[fun v ⊸[R]
            fun r ⊸[R]
              r •
                v]⟫[fun x ⊸
          fun vdf ⊸
            ((L x.1) vdf.1,
              fun dw ⊸[R]
                vdf.2 (semiAdjoint R (fun x_1 => (L x.1) x_1) dw) + x.2 (semiAdjoint R (fun x => (L x) vdf.1) dw))].1

case h.a.a.a
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
φ : 𝒟 Z
x✝ : W
⊢ ((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))
          φ).2
      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))])
          φ).2
      x✝