Theorem: SciLean.SciLean.Norm2.norm2.arg_a0.CDifferentiableAt_rule (SciLean/Core/FunctionPropositions/CDifferentiable.lean)

State before:
K✝ : Type ?u.34717
inst✝¹⁴ : RCLike K✝
X✝¹ : Type ?u.34723
inst✝¹³ : Vec K✝ X✝¹
Y✝¹ : Type ?u.34736
inst✝¹² : Vec K✝ Y✝¹
Z✝ : Type ?u.34747
inst✝¹¹ : Vec K✝ Z✝
ι✝ : Type ?u.34758
inst✝¹⁰ : IndexType ι✝
E✝ : ι✝ → Type ?u.34767
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type ?u.34783
inst✝⁸ : RCLike K
X✝ : Type ?u.34789
inst✝⁷ : Vec K X✝
Y✝ : Type ?u.34802
inst✝⁶ : Vec K Y✝
Z : Type ?u.34813
inst✝⁵ : Vec K Z
ι : Type ?u.34824
inst✝⁴ : IndexType ι
E : ι → Type ?u.34833
inst✝³ : (i : ι) → Vec K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : Vec R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f : X → Y
x : X
hf : CDifferentiableAt R f x
⊢ CDifferentiableAt R (fun x => ‖f x‖₂²) x
Tactic:
simp[← SemiInnerProductSpace.inner_norm2]
State after:
K✝ : Type ?u.34717
inst✝¹⁴ : RCLike K✝
X✝¹ : Type ?u.34723
inst✝¹³ : Vec K✝ X✝¹
Y✝¹ : Type ?u.34736
inst✝¹² : Vec K✝ Y✝¹
Z✝ : Type ?u.34747
inst✝¹¹ : Vec K✝ Z✝
ι✝ : Type ?u.34758
inst✝¹⁰ : IndexType ι✝
E✝ : ι✝ → Type ?u.34767
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type ?u.34783
inst✝⁸ : RCLike K
X✝ : Type ?u.34789
inst✝⁷ : Vec K X✝
Y✝ : Type ?u.34802
inst✝⁶ : Vec K Y✝
Z : Type ?u.34813
inst✝⁵ : Vec K Z
ι : Type ?u.34824
inst✝⁴ : IndexType ι
E : ι → Type ?u.34833
inst✝³ : (i : ι) → Vec K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : Vec R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f : X → Y
x : X
hf : CDifferentiableAt R f x
⊢ CDifferentiableAt R (fun x => ⟪f x, f x⟫_R) x

State before:
K✝ : Type ?u.34717
inst✝¹⁴ : RCLike K✝
X✝¹ : Type ?u.34723
inst✝¹³ : Vec K✝ X✝¹
Y✝¹ : Type ?u.34736
inst✝¹² : Vec K✝ Y✝¹
Z✝ : Type ?u.34747
inst✝¹¹ : Vec K✝ Z✝
ι✝ : Type ?u.34758
inst✝¹⁰ : IndexType ι✝
E✝ : ι✝ → Type ?u.34767
inst✝⁹ : (i : ι✝) → Vec K✝ (E✝ i)
K : Type ?u.34783
inst✝⁸ : RCLike K
X✝ : Type ?u.34789
inst✝⁷ : Vec K X✝
Y✝ : Type ?u.34802
inst✝⁶ : Vec K Y✝
Z : Type ?u.34813
inst✝⁵ : Vec K Z
ι : Type ?u.34824
inst✝⁴ : IndexType ι
E : ι → Type ?u.34833
inst✝³ : (i : ι) → Vec K (E i)
R : Type u_1
inst✝² : RealScalar R
X : Type u_2
inst✝¹ : Vec R X
Y : Type u_3
inst✝ : SemiHilbert R Y
f : X → Y
x : X
hf : CDifferentiableAt R f x
⊢ CDifferentiableAt R (fun x => ⟪f x, f x⟫_R) x
Tactic:
fun_prop
State after:
no goals