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

State before:
ι : Sort ?u.58553
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
⊢ HasAdjDiffM K fun x => pure (a0 x)
Tactic:
apply RevDerivMonad.HasAdjDiffM_pure a0 ha0
State after:
no goals