Theorem: SciLean.SciLean.semiAdjoint.arg_y.CDifferentiableAt_rule (SciLean/Core/FunctionPropositions/HasAdjDiff.lean)

State before:
K✝ : Type ?u.91165
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.91171
inst✝¹⁶ : SemiInnerProductSpace K✝ X✝
Y✝ : Type ?u.91184
inst✝¹⁵ : SemiInnerProductSpace K✝ Y✝
Z✝ : Type ?u.91195
inst✝¹⁴ : SemiInnerProductSpace K✝ Z✝
ι✝ : Type ?u.91206
inst✝¹³ : IndexType ι✝
inst✝¹² : LawfulIndexType ι✝
inst✝¹¹ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.91233
inst✝¹⁰ : (i : ι✝) → SemiInnerProductSpace K✝ (E✝ i)
K : Type u_2
inst✝⁹ : RCLike K
X : Type u_3
inst✝⁸ : SemiInnerProductSpace K X
Y : Type u_4
inst✝⁷ : SemiInnerProductSpace K Y
Z : Type ?u.91279
inst✝⁶ : SemiInnerProductSpace K Z
W✝ : Type ?u.91290
inst✝⁵ : SemiInnerProductSpace K W✝
ι : Type ?u.91301
inst✝⁴ : IndexType ι
inst✝³ : LawfulIndexType ι
inst✝² : DecidableEq ι
E : ι → Type ?u.91328
inst✝¹ : (i : ι) → SemiInnerProductSpace K (E i)
W : Type u_1
inst✝ : Vec K W
w : W
f : X → Y
a0 : W → Y
hf : CDifferentiable K f
ha0 : CDifferentiableAt K a0 w
⊢ CDifferentiableAt K (fun w => semiAdjoint K f (a0 w)) w
Tactic:
fun_prop
State after:
no goals