Theorem: SciLean.odeSolve.arg_ft₀tx₀.fwdDeriv_rule (SciLean/Modules/DifferentialEquations/OdeSolve.lean)

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₀
⊢ ∂> 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)
Tactic:
(conv => lhs; unfold fwdDeriv)
State after:
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)

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 => ((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)
Tactic:
fun_trans
State after:
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)

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
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)

State before:
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)
Tactic:
simp[fwdDeriv]
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 => (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

State before:
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
Tactic:
sorry_proof
State after:
no goals

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₀
⊢ ∂> 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)
Tactic:
conv => lhs; unfold fwdDeriv
State after:
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)