funext x
K : Type u_3
inst✝⁹ : RCLike K
X : Type u_1
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace K X
Y : Type u_2
inst✝⁶ : NormedAddCommGroup Y
inst✝⁵ : NormedSpace K Y
Z : Type ?u.133916
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace K Z
ι : Type ?u.134051
inst✝² : Fintype ι
E : ι → Type ?u.134059
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace K (E i)
f : X → Y
⊢ (fderiv K fun x => -f x) = fun x => fun dx =>L[K] -(fderiv K f x) dx
case h
K : Type u_3
inst✝⁹ : RCLike K
X : Type u_1
inst✝⁸ : NormedAddCommGroup X
inst✝⁷ : NormedSpace K X
Y : Type u_2
inst✝⁶ : NormedAddCommGroup Y
inst✝⁵ : NormedSpace K Y
Z : Type ?u.133916
inst✝⁴ : NormedAddCommGroup Z
inst✝³ : NormedSpace K Z
ι : Type ?u.134051
inst✝² : Fintype ι
E : ι → Type ?u.134059
inst✝¹ : (i : ι) → NormedAddCommGroup (E i)
inst✝ : (i : ι) → NormedSpace K (E i)
f : X → Y
x : X
⊢ fderiv K (fun x => -f x) x = fun dx =>L[K] -(fderiv K f x) dx