unfold backwardEuler
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' => ∂ (Δt:=Δt'), backwardEuler f t Δt x) = 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
⊢ (Filter.limit (nhds 0) fun Δt' => ∂ (Δt:=Δt'), solve x', x' = x + Δt • f (t + Δt) x') = f t x