Theorem: SciLean.odeSolve.arg_ft₀tx₀.fwdDeriv_rule
Proof state before:
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 =>
      (odeSolve (f x) (t₀ x) (t x) (x₀ x),
        (odeSolve (fun t xdx => ∂> (wkx:=(x, t, xdx.1);(dx, (∂> (w:=x;dx), t₀ w).2, xdx.2)), f wkx.1 wkx.2.1 wkx.2.2)
              (∂> (w:=x;dx), t₀ w).1 (∂> (w:=x;dx), t₀ w).1 (∂> (w:=x;dx), x₀ w)).2 +
          (∂> (w:=x;dx), t₀ w).2 •
            f x (∂> (w:=x;dx), t₀ w).1
              (odeSolve
                  (fun t xdx => ∂> (wkx:=(x, t, xdx.1);(dx, (∂> (w:=x;dx), t₀ w).2, xdx.2)), f wkx.1 wkx.2.1 wkx.2.2)
                  (∂> (w:=x;dx), t₀ w).1 (∂> (w:=x;dx), t₀ w).1 (∂> (w:=x;dx), x₀ w)).1)) =
    fun w dw =>
    ((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)
Tactic:
funext w dw
Proof state after:
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)