Theorem: SciLean.parDistribRevDeriv.bind_rule
Proof state before:
case h
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
⊢ (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)) =
    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))]
Tactic:
ext φ
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
⊢ ((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✝