rw[Filter.limit_of_continuous _ _ sorry_proof]
R : Type u_1
inst✝³ : RCLike R
X : Type u_2
inst✝² : Vec R X
Y : Type ?u.676
inst✝¹ : Vec R Y
Z : Type ?u.688
inst✝ : Vec R Z
f : R → X → X
hf : CDifferentiable R fun tx => f tx.1 tx.2
hf' : ∀ (tₙ Δt : R), Diffeomorphism R fun x => x - Δt • f (tₙ + Δt) x
t : R
x : X
⊢ (Filter.limit (nhds 0) fun Δt' =>
      let y := Function.invFun (fun x' => x' - Δt' • f (t + Δt') x') x;
      let y_1 := f (t + Δt') y;
      let y_2 := t + Δt';
      let dz := ∂ (x0:=y_2;1), f x0 y;
      let dfdx_y := -(Δt' • dz + y_1);
      let z := y - Δt' • f (t + Δt') y;
      let y := Function.invFun (fun x' => x' - Δt' • f (t + Δt') x') z;
      let dy := Function.invFun (fun dx => dx - Δt' • ∂ (x:=y;dx), f (t + Δt') x) dfdx_y;
      -dy) =
    f t x
R : Type u_1
inst✝³ : RCLike R
X : Type u_2
inst✝² : Vec R X
Y : Type ?u.676
inst✝¹ : Vec R Y
Z : Type ?u.688
inst✝ : Vec R Z
f : R → X → X
hf : CDifferentiable R fun tx => f tx.1 tx.2
hf' : ∀ (tₙ Δt : R), Diffeomorphism R fun x => x - Δt • f (tₙ + Δt) x
t : R
x : X
⊢ (let y := Function.invFun (fun x' => x' - 0 • f (t + 0) x') x;
    let y_1 := f (t + 0) y;
    let y_2 := t + 0;
    let dz := ∂ (x0:=y_2;1), f x0 y;
    let dfdx_y := -(0 • dz + y_1);
    let z := y - 0 • f (t + 0) y;
    let y := Function.invFun (fun x' => x' - 0 • f (t + 0) x') z;
    let dy := Function.invFun (fun dx => dx - 0 • ∂ (x:=y;dx), f (t + 0) x) dfdx_y;
    -dy) =
    f t x