Theorem: AnalyticAt.deriv (Ray/Analytic/Analytic.lean)

State before:
𝕜 : Type
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
inst✝¹⁰ : CompleteSpace E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : CompleteSpace F
G : Type
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace 𝕜 G
inst✝⁴ : CompleteSpace G
H : Type
inst✝³ : NormedAddCommGroup H
inst✝² : NormedSpace 𝕜 H
inst✝¹ : CompleteSpace H
f : 𝕜 → 𝕜
c : 𝕜
fa : AnalyticAt 𝕜 f c
inst✝ : CompleteSpace 𝕜
⊢ AnalyticAt 𝕜 (fun x => _root_.deriv f x) c
Tactic:
simp only [← fderiv_deriv]
State after:
𝕜 : Type
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
inst✝¹⁰ : CompleteSpace E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : CompleteSpace F
G : Type
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace 𝕜 G
inst✝⁴ : CompleteSpace G
H : Type
inst✝³ : NormedAddCommGroup H
inst✝² : NormedSpace 𝕜 H
inst✝¹ : CompleteSpace H
f : 𝕜 → 𝕜
c : 𝕜
fa : AnalyticAt 𝕜 f c
inst✝ : CompleteSpace 𝕜
⊢ AnalyticAt 𝕜 (fun x => (_root_.fderiv 𝕜 f x) 1) c

State before:
𝕜 : Type
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
inst✝¹⁰ : CompleteSpace E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : CompleteSpace F
G : Type
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace 𝕜 G
inst✝⁴ : CompleteSpace G
H : Type
inst✝³ : NormedAddCommGroup H
inst✝² : NormedSpace 𝕜 H
inst✝¹ : CompleteSpace H
f : 𝕜 → 𝕜
c : 𝕜
fa : AnalyticAt 𝕜 f c
inst✝ : CompleteSpace 𝕜
⊢ AnalyticAt 𝕜 (fun x => (_root_.fderiv 𝕜 f x) 1) c
Tactic:
have a1 : ∀ g, AnalyticAt 𝕜 (fun g : 𝕜 →L[𝕜] 𝕜 ↦ ContinuousLinearMap.apply 𝕜 𝕜 1 g) g := fun g ↦
  ContinuousLinearMap.analyticAt _ _
State after:
𝕜 : Type
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
inst✝¹⁰ : CompleteSpace E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : CompleteSpace F
G : Type
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace 𝕜 G
inst✝⁴ : CompleteSpace G
H : Type
inst✝³ : NormedAddCommGroup H
inst✝² : NormedSpace 𝕜 H
inst✝¹ : CompleteSpace H
f : 𝕜 → 𝕜
c : 𝕜
fa : AnalyticAt 𝕜 f c
inst✝ : CompleteSpace 𝕜
a1 : ∀ (g : 𝕜 →L[𝕜] 𝕜), AnalyticAt 𝕜 (fun g => ((ContinuousLinearMap.apply 𝕜 𝕜) 1) g) g
⊢ AnalyticAt 𝕜 (fun x => (_root_.fderiv 𝕜 f x) 1) c

State before:
𝕜 : Type
inst✝¹³ : NontriviallyNormedField 𝕜
E : Type
inst✝¹² : NormedAddCommGroup E
inst✝¹¹ : NormedSpace 𝕜 E
inst✝¹⁰ : CompleteSpace E
F : Type
inst✝⁹ : NormedAddCommGroup F
inst✝⁸ : NormedSpace 𝕜 F
inst✝⁷ : CompleteSpace F
G : Type
inst✝⁶ : NormedAddCommGroup G
inst✝⁵ : NormedSpace 𝕜 G
inst✝⁴ : CompleteSpace G
H : Type
inst✝³ : NormedAddCommGroup H
inst✝² : NormedSpace 𝕜 H
inst✝¹ : CompleteSpace H
f : 𝕜 → 𝕜
c : 𝕜
fa : AnalyticAt 𝕜 f c
inst✝ : CompleteSpace 𝕜
a1 : ∀ (g : 𝕜 →L[𝕜] 𝕜), AnalyticAt 𝕜 (fun g => ((ContinuousLinearMap.apply 𝕜 𝕜) 1) g) g
⊢ AnalyticAt 𝕜 (fun x => (_root_.fderiv 𝕜 f x) 1) c
Tactic:
refine (a1 _).comp fa.fderiv
State after:
no goals