Theorem: SciLean.parDistribRevDeriv.comp_rule (SciLean/Core/Distribution/ParametricDistribRevDeriv.lean)

State before:
R : Type u_1
inst✝⁸ : RealScalar R
W : Type ?u.8636
inst✝⁷ : SemiInnerProductSpace R W
X : Type u_5
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_3
inst✝¹ : SemiInnerProductSpace R U
V : Type ?u.10463
inst✝ : SemiInnerProductSpace R V
f : Y → 𝒟'(Z, U)
g : X → Y
hf : DistribDifferentiable f
hg : HasAdjDiff R g
⊢ (parDistribRevDeriv fun x => f (g x)) = fun x =>
    let ydg := revDeriv' R g x;
    let udf := parDistribRevDeriv f ydg.1;
    postComp udf (fun udf' ⊸[R] (udf'.1, fun du ⊸[R] ydg.2 (udf'.2 du)))
Tactic:
simp
State after:
R : Type u_1
inst✝⁸ : RealScalar R
W : Type ?u.8636
inst✝⁷ : SemiInnerProductSpace R W
X : Type u_5
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_3
inst✝¹ : SemiInnerProductSpace R U
V : Type ?u.10463
inst✝ : SemiInnerProductSpace R V
f : Y → 𝒟'(Z, U)
g : X → Y
hf : DistribDifferentiable f
hg : HasAdjDiff R g
⊢ (parDistribRevDeriv fun x => f (g x)) = fun x =>
    postComp (parDistribRevDeriv f (g x)) (fun udf' ⊸[R] (udf'.1, fun du ⊸[R] (<∂ g x).2 (udf'.2 du)))

State before:
R : Type u_1
inst✝⁸ : RealScalar R
W : Type ?u.8636
inst✝⁷ : SemiInnerProductSpace R W
X : Type u_5
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_3
inst✝¹ : SemiInnerProductSpace R U
V : Type ?u.10463
inst✝ : SemiInnerProductSpace R V
f : Y → 𝒟'(Z, U)
g : X → Y
hf : DistribDifferentiable f
hg : HasAdjDiff R g
⊢ (parDistribRevDeriv fun x => f (g x)) = fun x =>
    postComp (parDistribRevDeriv f (g x)) (fun udf' ⊸[R] (udf'.1, fun du ⊸[R] (<∂ g x).2 (udf'.2 du)))
Tactic:
unfold parDistribRevDeriv postComp
State after:
R : Type u_1
inst✝⁸ : RealScalar R
W : Type ?u.8636
inst✝⁷ : SemiInnerProductSpace R W
X : Type u_5
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_3
inst✝¹ : SemiInnerProductSpace R U
V : Type ?u.10463
inst✝ : SemiInnerProductSpace R V
f : Y → 𝒟'(Z, U)
g : X → Y
hf : DistribDifferentiable f
hg : HasAdjDiff R g
⊢ (fun x =>
      fun φ ⊸
        let df' := semiAdjoint R fun dx => ∂ (x:=x;dx), ((fun x => f (g x)) x) φ;
        let z := ((fun x => f (g x)) x) φ;
        (z, fun dz ⊸[R] df' dz)) =
    fun x =>
    fun φ ⊸[R]
      (fun udf' ⊸[R] (udf'.1, fun du ⊸[R] (<∂ g x).2 (udf'.2 du)))
        ((fun φ ⊸
            let df' := semiAdjoint R fun dx => ∂ (x:=g x;dx), (f x) φ;
            let z := (f (g x)) φ;
            (z, fun dz ⊸[R] df' dz))
          φ)

State before:
R : Type u_1
inst✝⁸ : RealScalar R
W : Type ?u.8636
inst✝⁷ : SemiInnerProductSpace R W
X : Type u_5
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_3
inst✝¹ : SemiInnerProductSpace R U
V : Type ?u.10463
inst✝ : SemiInnerProductSpace R V
f : Y → 𝒟'(Z, U)
g : X → Y
hf : DistribDifferentiable f
hg : HasAdjDiff R g
⊢ (fun x =>
      fun φ ⊸
        let df' := semiAdjoint R fun dx => ∂ (x:=x;dx), ((fun x => f (g x)) x) φ;
        let z := ((fun x => f (g x)) x) φ;
        (z, fun dz ⊸[R] df' dz)) =
    fun x =>
    fun φ ⊸[R]
      (fun udf' ⊸[R] (udf'.1, fun du ⊸[R] (<∂ g x).2 (udf'.2 du)))
        ((fun φ ⊸
            let df' := semiAdjoint R fun dx => ∂ (x:=g x;dx), (f x) φ;
            let z := (f (g x)) φ;
            (z, fun dz ⊸[R] df' dz))
          φ)
Tactic:
funext x
State after:
case h
R : Type u_1
inst✝⁸ : RealScalar R
W : Type ?u.8636
inst✝⁷ : SemiInnerProductSpace R W
X : Type u_5
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_3
inst✝¹ : SemiInnerProductSpace R U
V : Type ?u.10463
inst✝ : SemiInnerProductSpace R V
f : Y → 𝒟'(Z, U)
g : X → Y
hf : DistribDifferentiable f
hg : HasAdjDiff R g
x : X
⊢ (fun φ ⊸
      let df' := semiAdjoint R fun dx => ∂ (x:=x;dx), ((fun x => f (g x)) x) φ;
      let z := ((fun x => f (g x)) x) φ;
      (z, fun dz ⊸[R] df' dz)) =
    fun φ ⊸[R]
      (fun udf' ⊸[R] (udf'.1, fun du ⊸[R] (<∂ g x).2 (udf'.2 du)))
        ((fun φ ⊸
            let df' := semiAdjoint R fun dx => ∂ (x:=g x;dx), (f x) φ;
            let z := (f (g x)) φ;
            (z, fun dz ⊸[R] df' dz))
          φ)

State before:
case h
R : Type u_1
inst✝⁸ : RealScalar R
W : Type ?u.8636
inst✝⁷ : SemiInnerProductSpace R W
X : Type u_5
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_3
inst✝¹ : SemiInnerProductSpace R U
V : Type ?u.10463
inst✝ : SemiInnerProductSpace R V
f : Y → 𝒟'(Z, U)
g : X → Y
hf : DistribDifferentiable f
hg : HasAdjDiff R g
x : X
⊢ (fun φ ⊸
      let df' := semiAdjoint R fun dx => ∂ (x:=x;dx), ((fun x => f (g x)) x) φ;
      let z := ((fun x => f (g x)) x) φ;
      (z, fun dz ⊸[R] df' dz)) =
    fun φ ⊸[R]
      (fun udf' ⊸[R] (udf'.1, fun du ⊸[R] (<∂ g x).2 (udf'.2 du)))
        ((fun φ ⊸
            let df' := semiAdjoint R fun dx => ∂ (x:=g x;dx), (f x) φ;
            let z := (f (g x)) φ;
            (z, fun dz ⊸[R] df' dz))
          φ)
Tactic:
ext φ
State after:
case h.a.a
R : Type u_1
inst✝⁸ : RealScalar R
W : Type ?u.8636
inst✝⁷ : SemiInnerProductSpace R W
X : Type u_5
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_3
inst✝¹ : SemiInnerProductSpace R U
V : Type ?u.10463
inst✝ : SemiInnerProductSpace R V
f : Y → 𝒟'(Z, U)
g : X → Y
hf : DistribDifferentiable f
hg : HasAdjDiff R g
x : X
φ : 𝒟 Z
⊢ ((fun φ ⊸
          let df' := semiAdjoint R fun dx => ∂ (x:=x;dx), ((fun x => f (g x)) x) φ;
          let z := ((fun x => f (g x)) x) φ;
          (z, fun dz ⊸[R] df' dz))
        φ).1 =
    ((fun φ ⊸[R]
          (fun udf' ⊸[R] (udf'.1, fun du ⊸[R] (<∂ g x).2 (udf'.2 du)))
            ((fun φ ⊸
                let df' := semiAdjoint R fun dx => ∂ (x:=g x;dx), (f x) φ;
                let z := (f (g x)) φ;
                (z, fun dz ⊸[R] df' dz))
              φ))
        φ).1

case h.a.a.a
R : Type u_1
inst✝⁸ : RealScalar R
W : Type ?u.8636
inst✝⁷ : SemiInnerProductSpace R W
X : Type u_5
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_3
inst✝¹ : SemiInnerProductSpace R U
V : Type ?u.10463
inst✝ : SemiInnerProductSpace R V
f : Y → 𝒟'(Z, U)
g : X → Y
hf : DistribDifferentiable f
hg : HasAdjDiff R g
x : X
φ : 𝒟 Z
x✝ : U
⊢ ((fun φ ⊸
            let df' := semiAdjoint R fun dx => ∂ (x:=x;dx), ((fun x => f (g x)) x) φ;
            let z := ((fun x => f (g x)) x) φ;
            (z, fun dz ⊸[R] df' dz))
          φ).2
      x✝ =
    ((fun φ ⊸[R]
            (fun udf' ⊸[R] (udf'.1, fun du ⊸[R] (<∂ g x).2 (udf'.2 du)))
              ((fun φ ⊸
                  let df' := semiAdjoint R fun dx => ∂ (x:=g x;dx), (f x) φ;
                  let z := (f (g x)) φ;
                  (z, fun dz ⊸[R] df' dz))
                φ))
          φ).2
      x✝

State before:
case h.a.a
R : Type u_1
inst✝⁸ : RealScalar R
W : Type ?u.8636
inst✝⁷ : SemiInnerProductSpace R W
X : Type u_5
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_3
inst✝¹ : SemiInnerProductSpace R U
V : Type ?u.10463
inst✝ : SemiInnerProductSpace R V
f : Y → 𝒟'(Z, U)
g : X → Y
hf : DistribDifferentiable f
hg : HasAdjDiff R g
x : X
φ : 𝒟 Z
⊢ ((fun φ ⊸
          let df' := semiAdjoint R fun dx => ∂ (x:=x;dx), ((fun x => f (g x)) x) φ;
          let z := ((fun x => f (g x)) x) φ;
          (z, fun dz ⊸[R] df' dz))
        φ).1 =
    ((fun φ ⊸[R]
          (fun udf' ⊸[R] (udf'.1, fun du ⊸[R] (<∂ g x).2 (udf'.2 du)))
            ((fun φ ⊸
                let df' := semiAdjoint R fun dx => ∂ (x:=g x;dx), (f x) φ;
                let z := (f (g x)) φ;
                (z, fun dz ⊸[R] df' dz))
              φ))
        φ).1

case h.a.a.a
R : Type u_1
inst✝⁸ : RealScalar R
W : Type ?u.8636
inst✝⁷ : SemiInnerProductSpace R W
X : Type u_5
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_3
inst✝¹ : SemiInnerProductSpace R U
V : Type ?u.10463
inst✝ : SemiInnerProductSpace R V
f : Y → 𝒟'(Z, U)
g : X → Y
hf : DistribDifferentiable f
hg : HasAdjDiff R g
x : X
φ : 𝒟 Z
x✝ : U
⊢ ((fun φ ⊸
            let df' := semiAdjoint R fun dx => ∂ (x:=x;dx), ((fun x => f (g x)) x) φ;
            let z := ((fun x => f (g x)) x) φ;
            (z, fun dz ⊸[R] df' dz))
          φ).2
      x✝ =
    ((fun φ ⊸[R]
            (fun udf' ⊸[R] (udf'.1, fun du ⊸[R] (<∂ g x).2 (udf'.2 du)))
              ((fun φ ⊸
                  let df' := semiAdjoint R fun dx => ∂ (x:=g x;dx), (f x) φ;
                  let z := (f (g x)) φ;
                  (z, fun dz ⊸[R] df' dz))
                φ))
          φ).2
      x✝
Tactic:
simp
State after:
case h.a.a.a
R : Type u_1
inst✝⁸ : RealScalar R
W : Type ?u.8636
inst✝⁷ : SemiInnerProductSpace R W
X : Type u_5
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_3
inst✝¹ : SemiInnerProductSpace R U
V : Type ?u.10463
inst✝ : SemiInnerProductSpace R V
f : Y → 𝒟'(Z, U)
g : X → Y
hf : DistribDifferentiable f
hg : HasAdjDiff R g
x : X
φ : 𝒟 Z
x✝ : U
⊢ ((fun φ ⊸
            let df' := semiAdjoint R fun dx => ∂ (x:=x;dx), ((fun x => f (g x)) x) φ;
            let z := ((fun x => f (g x)) x) φ;
            (z, fun dz ⊸[R] df' dz))
          φ).2
      x✝ =
    ((fun φ ⊸[R]
            (fun udf' ⊸[R] (udf'.1, fun du ⊸[R] (<∂ g x).2 (udf'.2 du)))
              ((fun φ ⊸
                  let df' := semiAdjoint R fun dx => ∂ (x:=g x;dx), (f x) φ;
                  let z := (f (g x)) φ;
                  (z, fun dz ⊸[R] df' dz))
                φ))
          φ).2
      x✝

State before:
case h.a.a.a
R : Type u_1
inst✝⁸ : RealScalar R
W : Type ?u.8636
inst✝⁷ : SemiInnerProductSpace R W
X : Type u_5
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_3
inst✝¹ : SemiInnerProductSpace R U
V : Type ?u.10463
inst✝ : SemiInnerProductSpace R V
f : Y → 𝒟'(Z, U)
g : X → Y
hf : DistribDifferentiable f
hg : HasAdjDiff R g
x : X
φ : 𝒟 Z
x✝ : U
⊢ ((fun φ ⊸
            let df' := semiAdjoint R fun dx => ∂ (x:=x;dx), ((fun x => f (g x)) x) φ;
            let z := ((fun x => f (g x)) x) φ;
            (z, fun dz ⊸[R] df' dz))
          φ).2
      x✝ =
    ((fun φ ⊸[R]
            (fun udf' ⊸[R] (udf'.1, fun du ⊸[R] (<∂ g x).2 (udf'.2 du)))
              ((fun φ ⊸
                  let df' := semiAdjoint R fun dx => ∂ (x:=g x;dx), (f x) φ;
                  let z := (f (g x)) φ;
                  (z, fun dz ⊸[R] df' dz))
                φ))
          φ).2
      x✝
Tactic:
sorry_proof
State after:
no goals