Theorem: HasFDerivAt.const_clm_comp (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
u : α → E →L[𝕜] F
u' : α →L[𝕜] E →L[𝕜] F
x : α
hu : HasFDerivAt u u' x
⊢ HasFDerivAt (fun y => ContinuousLinearMap.comp c (u y))
    (ContinuousLinearMap.comp ((ContinuousLinearMap.compL 𝕜 E F G) c) u') x
Tactic:
refine HasFDerivAt.congr_fderiv (HasFDerivAt.clm_comp (hasFDerivAt_const c x) hu) ?_
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
u : α → E →L[𝕜] F
u' : α →L[𝕜] E →L[𝕜] F
x : α
hu : HasFDerivAt u u' x
⊢ ContinuousLinearMap.comp ((ContinuousLinearMap.compL 𝕜 E F G) c) u' +
      ContinuousLinearMap.comp ((ContinuousLinearMap.flip (ContinuousLinearMap.compL 𝕜 E F G)) (u x)) 0 =
    ContinuousLinearMap.comp ((ContinuousLinearMap.compL 𝕜 E F G) c) u'

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
u : α → E →L[𝕜] F
u' : α →L[𝕜] E →L[𝕜] F
x : α
hu : HasFDerivAt u u' x
⊢ ContinuousLinearMap.comp ((ContinuousLinearMap.compL 𝕜 E F G) c) u' +
      ContinuousLinearMap.comp ((ContinuousLinearMap.flip (ContinuousLinearMap.compL 𝕜 E F G)) (u x)) 0 =
    ContinuousLinearMap.comp ((ContinuousLinearMap.compL 𝕜 E F G) c) u'
Tactic:
rw [ContinuousLinearMap.comp_zero, add_zero]
State after:
no goals