Theorem: Pure.pure.arg_a0.revDerivM_rule (SciLean/Core/Monads/RevDerivMonad.lean)

State before:
ι : Sort ?u.59125
K : Type
inst✝⁹ : RCLike K
m m' : Type → Type
inst✝⁸ : Monad m
inst✝⁷ : Monad m'
inst✝⁶ : RevDerivMonad K m m'
inst✝⁵ : LawfulMonad m
inst✝⁴ : LawfulMonad m'
X : Type
inst✝³ : SemiInnerProductSpace K X
Y : Type
inst✝² : SemiInnerProductSpace K Y
Z : Type
inst✝¹ : SemiInnerProductSpace K Z
E : ι → Type
inst✝ : (i : ι) → SemiInnerProductSpace K (E i)
a0 : X → Y
ha0 : HasAdjDiff K a0
⊢ (revDerivM K fun x => pure (a0 x)) = fun x =>
    let ydf := revDeriv K a0 x;
    pure (ydf.1, fun dy => pure (ydf.2 dy))
Tactic:
apply RevDerivMonad.revDerivM_pure a0 ha0
State after:
no goals