Theorem: Pure.pure.arg_a0.fwdDerivM_rule (SciLean/Core/Monads/FwdDerivMonad.lean)

State before:
ι : Sort ?u.26156
K : Type
inst✝⁹ : RCLike K
m m' : Type → Type
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : FwdDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
X : Type
inst✝³ : Vec K X
Y : Type
inst✝² : Vec K Y
Z : Type
inst✝¹ : Vec K Z
E : ι → Type
inst✝ : (i : ι) → Vec K (E i)
a0 : X → Y
ha0 : CDifferentiable K a0
⊢ (fwdDerivM K fun x => pure (a0 x)) = fun x dx => pure (fwdDeriv K a0 x dx)
Tactic:
apply FwdDerivMonad.fwdDerivM_pure a0 ha0
State after:
no goals