Theorem: Probly.randFwdDeriv_comp (Probly/RandFwdDeriv.lean)

State before:
W : Type ?u.1352
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type u_2
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type u_1
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.1821
inst✝¹ : MeasurableSpace α
β : Type ?u.1827
inst✝ : MeasurableSpace β
f : Y → Rand Z
g : X → Y
hf : RandDifferentiable f
hg : Differentiable ℝ g
⊢ (randFwdDeriv fun x => f (g x)) = fun x dx =>
    let ydy := fwdDeriv ℝ g x dx;
    randFwdDeriv f ydy.1 ydy.2
Tactic:
funext x dx
State after:
case h.h
W : Type ?u.1352
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type u_2
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type u_1
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.1821
inst✝¹ : MeasurableSpace α
β : Type ?u.1827
inst✝ : MeasurableSpace β
f : Y → Rand Z
g : X → Y
hf : RandDifferentiable f
hg : Differentiable ℝ g
x dx : X
⊢ randFwdDeriv (fun x => f (g x)) x dx =
    let ydy := fwdDeriv ℝ g x dx;
    randFwdDeriv f ydy.1 ydy.2

State before:
case h.h
W : Type ?u.1352
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type u_2
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type u_1
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.1821
inst✝¹ : MeasurableSpace α
β : Type ?u.1827
inst✝ : MeasurableSpace β
f : Y → Rand Z
g : X → Y
hf : RandDifferentiable f
hg : Differentiable ℝ g
x dx : X
⊢ randFwdDeriv (fun x => f (g x)) x dx =
    let ydy := fwdDeriv ℝ g x dx;
    randFwdDeriv f ydy.1 ydy.2
Tactic:
unfold randFwdDeriv fwdDeriv
State after:
case h.h
W : Type ?u.1352
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type u_2
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type u_1
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.1821
inst✝¹ : MeasurableSpace α
β : Type ?u.1827
inst✝ : MeasurableSpace β
f : Y → Rand Z
g : X → Y
hf : RandDifferentiable f
hg : Differentiable ℝ g
x dx : X
⊢ { val := (fun x => f (g x)) x, dval := randDeriv (fun x => f (g x)) x dx } =
    let ydy := (g x, (fderiv ℝ g x) dx);
    { val := f ydy.1, dval := randDeriv f ydy.1 ydy.2 }

State before:
case h.h
W : Type ?u.1352
inst✝¹³ : NormedAddCommGroup W
inst✝¹² : NormedSpace ℝ W
inst✝¹¹ : MeasurableSpace W
X : Type u_2
inst✝¹⁰ : NormedAddCommGroup X
inst✝⁹ : NormedSpace ℝ X
inst✝⁸ : MeasurableSpace X
Y : Type u_1
inst✝⁷ : NormedAddCommGroup Y
inst✝⁶ : NormedSpace ℝ Y
inst✝⁵ : MeasurableSpace Y
Z : Type
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace ℝ Z
inst✝² : MeasurableSpace Z
α : Type ?u.1821
inst✝¹ : MeasurableSpace α
β : Type ?u.1827
inst✝ : MeasurableSpace β
f : Y → Rand Z
g : X → Y
hf : RandDifferentiable f
hg : Differentiable ℝ g
x dx : X
⊢ { val := (fun x => f (g x)) x, dval := randDeriv (fun x => f (g x)) x dx } =
    let ydy := (g x, (fderiv ℝ g x) dx);
    { val := f ydy.1, dval := randDeriv f ydy.1 ydy.2 }
Tactic:
simp (disch := first | apply hf | apply hg) only [rand_simp,randDeriv_comp]
State after:
no goals