[GOAL]
𝕜 : Type u
inst✝⁷ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
f : 𝕜 → F
inst✝⁴ : StarRing 𝕜
inst✝³ : TrivialStar 𝕜
inst✝² : StarAddMonoid F
inst✝¹ : ContinuousStar F
inst✝ : StarModule 𝕜 F
f' : F
x : 𝕜
L : Filter 𝕜
h : HasDerivAtFilter f f' x L
⊢ HasDerivAtFilter (fun x => star (f x)) (star f') x L
[PROOFSTEP]
simpa using h.star.hasDerivAtFilter
[GOAL]
𝕜 : Type u
inst✝⁷ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁶ : NormedAddCommGroup F
inst✝⁵ : NormedSpace 𝕜 F
f : 𝕜 → F
inst✝⁴ : StarRing 𝕜
inst✝³ : TrivialStar 𝕜
inst✝² : StarAddMonoid F
inst✝¹ : ContinuousStar F
inst✝ : StarModule 𝕜 F
f' : F
x : 𝕜
h : HasStrictDerivAt f f' x
⊢ HasStrictDerivAt (fun x => star (f x)) (star f') x
[PROOFSTEP]
simpa using h.star.hasStrictDerivAt
