Theorem: HasFDerivAt.clm_apply_const (ForML/ContinuousLinearMap.lean)

State before:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup α
inst✝⁶ : NormedSpace 𝕜 α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
c : α → F →L[𝕜] G
v : F
c' : α →L[𝕜] F →L[𝕜] G
x : α
hc : HasFDerivAt c c' x
⊢ HasFDerivAt (fun y => (c y) v) ((ContinuousLinearMap.flip c') v) x
Tactic:
refine HasFDerivAt.congr_fderiv (HasFDerivAt.clm_apply hc (hasFDerivAt_const v x)) ?_
State after:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup α
inst✝⁶ : NormedSpace 𝕜 α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
c : α → F →L[𝕜] G
v : F
c' : α →L[𝕜] F →L[𝕜] G
x : α
hc : HasFDerivAt c c' x
⊢ ContinuousLinearMap.comp (c x) 0 + (ContinuousLinearMap.flip c') v = (ContinuousLinearMap.flip c') v

State before:
𝕜 : Type u_1
α : Type u_2
E : Type u_3
F : Type u_4
G : Type u_5
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : NormedAddCommGroup α
inst✝⁶ : NormedSpace 𝕜 α
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
c : α → F →L[𝕜] G
v : F
c' : α →L[𝕜] F →L[𝕜] G
x : α
hc : HasFDerivAt c c' x
⊢ ContinuousLinearMap.comp (c x) 0 + (ContinuousLinearMap.flip c') v = (ContinuousLinearMap.flip c') v
Tactic:
simp
State after:
no goals