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

State before:
R : Type u_1
inst✝⁸ : RealScalar R
W : Type ?u.8688
inst✝⁷ : Vec R W
X : Type u_5
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_3
inst✝¹ : Vec R U
V : Type ?u.10339
inst✝ : Vec R V
f : Y → 𝒟'(Z, U)
g : X → Y
hf : DistribDifferentiable f
hg : CDifferentiable R g
⊢ (parDistribFwdDeriv fun x => f (g x)) = fun x dx =>
    let ydy := ∂> g x dx;
    parDistribFwdDeriv f ydy.1 ydy.2
Tactic:
unfold parDistribFwdDeriv
State after:
R : Type u_1
inst✝⁸ : RealScalar R
W : Type ?u.8688
inst✝⁷ : Vec R W
X : Type u_5
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_3
inst✝¹ : Vec R U
V : Type ?u.10339
inst✝ : Vec R V
f : Y → 𝒟'(Z, U)
g : X → Y
hf : DistribDifferentiable f
hg : CDifferentiable R g
⊢ (fun x dx =>
      let dz := postComp (parDistribDeriv (fun x => f (g x)) x dx) (fun dz ⊸[R] (0, dz));
      let z := postComp ((fun x => f (g x)) x) (fun z ⊸[R] (z, 0));
      z + dz) =
    fun x dx =>
    let ydy := ∂> g x dx;
    let dz := postComp (parDistribDeriv f ydy.1 ydy.2) (fun dz ⊸[R] (0, dz));
    let z := postComp (f ydy.1) (fun z ⊸[R] (z, 0));
    z + dz

State before:
R : Type u_1
inst✝⁸ : RealScalar R
W : Type ?u.8688
inst✝⁷ : Vec R W
X : Type u_5
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_3
inst✝¹ : Vec R U
V : Type ?u.10339
inst✝ : Vec R V
f : Y → 𝒟'(Z, U)
g : X → Y
hf : DistribDifferentiable f
hg : CDifferentiable R g
⊢ (fun x dx =>
      let dz := postComp (parDistribDeriv (fun x => f (g x)) x dx) (fun dz ⊸[R] (0, dz));
      let z := postComp ((fun x => f (g x)) x) (fun z ⊸[R] (z, 0));
      z + dz) =
    fun x dx =>
    let ydy := ∂> g x dx;
    let dz := postComp (parDistribDeriv f ydy.1 ydy.2) (fun dz ⊸[R] (0, dz));
    let z := postComp (f ydy.1) (fun z ⊸[R] (z, 0));
    z + dz
Tactic:
funext x dx
State after:
case h.h
R : Type u_1
inst✝⁸ : RealScalar R
W : Type ?u.8688
inst✝⁷ : Vec R W
X : Type u_5
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_3
inst✝¹ : Vec R U
V : Type ?u.10339
inst✝ : Vec R V
f : Y → 𝒟'(Z, U)
g : X → Y
hf : DistribDifferentiable f
hg : CDifferentiable R g
x dx : X
⊢ (let dz := postComp (parDistribDeriv (fun x => f (g x)) x dx) (fun dz ⊸[R] (0, dz));
    let z := postComp ((fun x => f (g x)) x) (fun z ⊸[R] (z, 0));
    z + dz) =
    let ydy := ∂> g x dx;
    let dz := postComp (parDistribDeriv f ydy.1 ydy.2) (fun dz ⊸[R] (0, dz));
    let z := postComp (f ydy.1) (fun z ⊸[R] (z, 0));
    z + dz

State before:
case h.h
R : Type u_1
inst✝⁸ : RealScalar R
W : Type ?u.8688
inst✝⁷ : Vec R W
X : Type u_5
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_3
inst✝¹ : Vec R U
V : Type ?u.10339
inst✝ : Vec R V
f : Y → 𝒟'(Z, U)
g : X → Y
hf : DistribDifferentiable f
hg : CDifferentiable R g
x dx : X
⊢ (let dz := postComp (parDistribDeriv (fun x => f (g x)) x dx) (fun dz ⊸[R] (0, dz));
    let z := postComp ((fun x => f (g x)) x) (fun z ⊸[R] (z, 0));
    z + dz) =
    let ydy := ∂> g x dx;
    let dz := postComp (parDistribDeriv f ydy.1 ydy.2) (fun dz ⊸[R] (0, dz));
    let z := postComp (f ydy.1) (fun z ⊸[R] (z, 0));
    z + dz
Tactic:
fun_trans [action_push,fwdDeriv]
State after:
no goals