conv => lhs; unfold fwdDeriv
R✝ : Type ?u.6372
inst✝⁶ : RCLike R✝
X✝ : Type ?u.6378
inst✝⁵ : Vec R✝ X✝
R : Type u_1
inst✝⁴ : RCLike R
W : Type u_3
inst✝³ : Vec R W
X : Type u_2
inst✝² : Vec R X
Y : Type ?u.6424
inst✝¹ : Vec R Y
Z : Type ?u.6436
inst✝ : Vec R Z
f : W → R → X → X
t₀ t : W → R
x₀ : W → X
hf :
  CDifferentiable R fun x =>
    match x with
    | (w, t, x) => f w t x
ht₀ : CDifferentiable R t₀
ht : CDifferentiable R t
hx : CDifferentiable R x₀
⊢ ∂> w, odeSolve (f w) (t₀ w) (t w) (x₀ w) = fun w dw =>
    let t₀dt₀ := ∂> t₀ w dw;
    let tdt := ∂> t₀ w dw;
    let x₀dx₀ := ∂> x₀ w dw;
    let Tf := ∂> wkx, f wkx.1 wkx.2.1 wkx.2.2;
    let F := fun t xdx =>
      let x := xdx.1;
      let dx := xdx.2;
      Tf (w, t, x) (dw, t₀dt₀.2, dx);
    let xdx := odeSolve F t₀dt₀.1 tdt.1 x₀dx₀;
    (xdx.1, xdx.2 + tdt.2 • f w tdt.1 xdx.1)
R✝ : Type ?u.6372
inst✝⁶ : RCLike R✝
X✝ : Type ?u.6378
inst✝⁵ : Vec R✝ X✝
R : Type u_1
inst✝⁴ : RCLike R
W : Type u_3
inst✝³ : Vec R W
X : Type u_2
inst✝² : Vec R X
Y : Type ?u.6424
inst✝¹ : Vec R Y
Z : Type ?u.6436
inst✝ : Vec R Z
f : W → R → X → X
t₀ t : W → R
x₀ : W → X
hf :
  CDifferentiable R fun x =>
    match x with
    | (w, t, x) => f w t x
ht₀ : CDifferentiable R t₀
ht : CDifferentiable R t
hx : CDifferentiable R x₀
⊢ (fun x dx => ((fun w => odeSolve (f w) (t₀ w) (t w) (x₀ w)) x, ∂ (w:=x;dx), odeSolve (f w) (t₀ w) (t w) (x₀ w))) =
    fun w dw =>
    let t₀dt₀ := ∂> t₀ w dw;
    let tdt := ∂> t₀ w dw;
    let x₀dx₀ := ∂> x₀ w dw;
    let Tf := ∂> wkx, f wkx.1 wkx.2.1 wkx.2.2;
    let F := fun t xdx =>
      let x := xdx.1;
      let dx := xdx.2;
      Tf (w, t, x) (dw, t₀dt₀.2, dx);
    let xdx := odeSolve F t₀dt₀.1 tdt.1 x₀dx₀;
    (xdx.1, xdx.2 + tdt.2 • f w tdt.1 xdx.1)