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

State before:
K✝ : Type ?u.91910
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.91916
inst✝¹⁶ : SemiInnerProductSpace K✝ X✝
Y✝ : Type ?u.91929
inst✝¹⁵ : SemiInnerProductSpace K✝ Y✝
Z✝ : Type ?u.91940
inst✝¹⁴ : SemiInnerProductSpace K✝ Z✝
ι✝ : Type ?u.91951
inst✝¹³ : IndexType ι✝
inst✝¹² : LawfulIndexType ι✝
inst✝¹¹ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.91978
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.92024
inst✝⁶ : SemiInnerProductSpace K Z
W✝ : Type ?u.92035
inst✝⁵ : SemiInnerProductSpace K W✝
ι : Type ?u.92046
inst✝⁴ : IndexType ι
inst✝³ : LawfulIndexType ι
inst✝² : DecidableEq ι
E : ι → Type ?u.92073
inst✝¹ : (i : ι) → SemiInnerProductSpace K (E i)
W : Type u_1
inst✝ : Vec K W
f : X → Y
a0 : W → Y
hf : CDifferentiable K f
ha0 : CDifferentiable K a0
⊢ CDifferentiable K fun w => semiAdjoint K f (a0 w)
Tactic:
intro x
State after:
K✝ : Type ?u.91910
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.91916
inst✝¹⁶ : SemiInnerProductSpace K✝ X✝
Y✝ : Type ?u.91929
inst✝¹⁵ : SemiInnerProductSpace K✝ Y✝
Z✝ : Type ?u.91940
inst✝¹⁴ : SemiInnerProductSpace K✝ Z✝
ι✝ : Type ?u.91951
inst✝¹³ : IndexType ι✝
inst✝¹² : LawfulIndexType ι✝
inst✝¹¹ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.91978
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.92024
inst✝⁶ : SemiInnerProductSpace K Z
W✝ : Type ?u.92035
inst✝⁵ : SemiInnerProductSpace K W✝
ι : Type ?u.92046
inst✝⁴ : IndexType ι
inst✝³ : LawfulIndexType ι
inst✝² : DecidableEq ι
E : ι → Type ?u.92073
inst✝¹ : (i : ι) → SemiInnerProductSpace K (E i)
W : Type u_1
inst✝ : Vec K W
f : X → Y
a0 : W → Y
hf : CDifferentiable K f
ha0 : CDifferentiable K a0
x : W
⊢ CDifferentiableAt K (fun w => semiAdjoint K f (a0 w)) x

State before:
K✝ : Type ?u.91910
inst✝¹⁷ : RCLike K✝
X✝ : Type ?u.91916
inst✝¹⁶ : SemiInnerProductSpace K✝ X✝
Y✝ : Type ?u.91929
inst✝¹⁵ : SemiInnerProductSpace K✝ Y✝
Z✝ : Type ?u.91940
inst✝¹⁴ : SemiInnerProductSpace K✝ Z✝
ι✝ : Type ?u.91951
inst✝¹³ : IndexType ι✝
inst✝¹² : LawfulIndexType ι✝
inst✝¹¹ : DecidableEq ι✝
E✝ : ι✝ → Type ?u.91978
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.92024
inst✝⁶ : SemiInnerProductSpace K Z
W✝ : Type ?u.92035
inst✝⁵ : SemiInnerProductSpace K W✝
ι : Type ?u.92046
inst✝⁴ : IndexType ι
inst✝³ : LawfulIndexType ι
inst✝² : DecidableEq ι
E : ι → Type ?u.92073
inst✝¹ : (i : ι) → SemiInnerProductSpace K (E i)
W : Type u_1
inst✝ : Vec K W
f : X → Y
a0 : W → Y
hf : CDifferentiable K f
ha0 : CDifferentiable K a0
x : W
⊢ CDifferentiableAt K (fun w => semiAdjoint K f (a0 w)) x
Tactic:
fun_prop
State after:
no goals