Theorem: SciLean.forwardEuler.isOdeStepper (SciLean/Modules/DifferentialEquations/OdeSolvers/ForwardEuler.lean)

State before:
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
⊢ ∀ (t : R) (x : X), (Filter.limit (nhds 0) fun Δt' => ∂ (Δt:=Δt'), forwardEuler f t Δt x) = f t x
Tactic:
unfold forwardEuler
State after:
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
⊢ ∀ (t : R) (x : X), (Filter.limit (nhds 0) fun Δt' => ∂ (Δt:=Δt'), (x + Δt • f t x)) = f t x

State before:
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
⊢ ∀ (t : R) (x : X), (Filter.limit (nhds 0) fun Δt' => ∂ (Δt:=Δt'), (x + Δt • f t x)) = f t x
Tactic:
autodiff
State after:
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
⊢ ∀ (t : R) (x : X),
    let y := f t x;
    (Filter.limit (nhds 0) fun Δt' => y) = f t x

State before:
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
⊢ ∀ (t : R) (x : X),
    let y := f t x;
    (Filter.limit (nhds 0) fun Δt' => y) = f t x
Tactic:
simp
State after:
no goals