𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L L₁ L₂ : Filter 𝕜
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
c : 𝕜 → F →L[𝕜] G
c' : F →L[𝕜] G
d : 𝕜 → E →L[𝕜] F
d' : E →L[𝕜] F
u : 𝕜 → F
u' : F
hc : HasDerivAt c c' x
hu : HasDerivAt u u' x
this :
  HasDerivAt (fun y => ↑(c y) (u y))
    (↑(comp (c x) (smulRight 1 u') + ↑(ContinuousLinearMap.flip (smulRight 1 c')) (u x)) 1) x
⊢ HasDerivAt (fun y => ↑(c y) (u y)) (↑c' (u x) + ↑(c x) u') x
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L L₁ L₂ : Filter 𝕜
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
c : 𝕜 → F →L[𝕜] G
c' : F →L[𝕜] G
d : 𝕜 → E →L[𝕜] F
d' : E →L[𝕜] F
u : 𝕜 → F
u' : F
hc : HasDerivAt c c' x
hu : HasDerivAt u u' x
⊢ HasDerivAt (fun y => ↑(c y) (u y)) (↑c' (u x) + ↑(c x) u') x
have := (hc.hasFDerivAt.clm_apply hu.hasFDerivAt).hasDerivAt
no goals
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
E : Type w
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
f f₀ f₁ g : 𝕜 → F
f' f₀' f₁' g' : F
x : 𝕜
s t : Set 𝕜
L L₁ L₂ : Filter 𝕜
G : Type u_1
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
c : 𝕜 → F →L[𝕜] G
c' : F →L[𝕜] G
d : 𝕜 → E →L[𝕜] F
d' : E →L[𝕜] F
u : 𝕜 → F
u' : F
hc : HasDerivAt c c' x
hu : HasDerivAt u u' x
this :
  HasDerivAt (fun y => ↑(c y) (u y))
    (↑(comp (c x) (smulRight 1 u') + ↑(ContinuousLinearMap.flip (smulRight 1 c')) (u x)) 1) x
⊢ HasDerivAt (fun y => ↑(c y) (u y)) (↑c' (u x) + ↑(c x) u') x
rwa [add_apply, comp_apply, flip_apply, smulRight_apply, smulRight_apply, one_apply, one_smul,
  one_smul, add_comm] at this