simp[fwdDeriv]
case h.h
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 dw : W
⊢ (odeSolve (f w) (t₀ w) (t w) (x₀ w),
      (odeSolve (fun t xdx => ∂> (wkx:=(w, t, xdx.1);(dw, (∂> (w:=w;dw), t₀ w).2, xdx.2)), f wkx.1 wkx.2.1 wkx.2.2)
            (∂> (w:=w;dw), t₀ w).1 (∂> (w:=w;dw), t₀ w).1 (∂> (w:=w;dw), x₀ w)).2 +
        (∂> (w:=w;dw), t₀ w).2 •
          f w (∂> (w:=w;dw), t₀ w).1
            (odeSolve
                (fun t xdx => ∂> (wkx:=(w, t, xdx.1);(dw, (∂> (w:=w;dw), t₀ w).2, xdx.2)), f wkx.1 wkx.2.1 wkx.2.2)
                (∂> (w:=w;dw), t₀ w).1 (∂> (w:=w;dw), t₀ w).1 (∂> (w:=w;dw), x₀ w)).1) =
    ((odeSolve (fun t xdx => ∂> (wkx:=(w, t, xdx.1);(dw, (∂> t₀ w dw).2, xdx.2)), f wkx.1 wkx.2.1 wkx.2.2)
          (∂> t₀ w dw).1 (∂> t₀ w dw).1 (∂> x₀ w dw)).1,
      (odeSolve (fun t xdx => ∂> (wkx:=(w, t, xdx.1);(dw, (∂> t₀ w dw).2, xdx.2)), f wkx.1 wkx.2.1 wkx.2.2)
            (∂> t₀ w dw).1 (∂> t₀ w dw).1 (∂> x₀ w dw)).2 +
        (∂> t₀ w dw).2 •
          f w (∂> t₀ w dw).1
            (odeSolve (fun t xdx => ∂> (wkx:=(w, t, xdx.1);(dw, (∂> t₀ w dw).2, xdx.2)), f wkx.1 wkx.2.1 wkx.2.2)
                (∂> t₀ w dw).1 (∂> t₀ w dw).1 (∂> x₀ w dw)).1)
case h.h
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 dw : W
⊢ odeSolve (f w) (t₀ w) (t w) (x₀ w) =
    (odeSolve (fun t xdx => (f w t xdx.1, ∂ (wkx:=(w, t, xdx.1);(dw, ∂ t₀ w dw, xdx.2)), f wkx.1 wkx.2.1 wkx.2.2))
        (t₀ w) (t₀ w) (x₀ w, ∂ x₀ w dw)).1