case zero
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : AnalyticOn 𝕜 f s
⊢ AnalyticOn 𝕜 (_root_.iteratedFDeriv 𝕜 Nat.zero f) s

case succ
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : AnalyticOn 𝕜 f s
n : ℕ
IH : AnalyticOn 𝕜 (_root_.iteratedFDeriv 𝕜 n f) s
⊢ AnalyticOn 𝕜 (_root_.iteratedFDeriv 𝕜 (Nat.succ n) f) s
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : AnalyticOn 𝕜 f s
n : ℕ
⊢ AnalyticOn 𝕜 (_root_.iteratedFDeriv 𝕜 n f) s
induction' n with n IH
case zero
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : AnalyticOn 𝕜 f s
⊢ AnalyticOn 𝕜 (↑(LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 𝕜 E F)) ∘ f) s
case zero
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : AnalyticOn 𝕜 f s
⊢ AnalyticOn 𝕜 (_root_.iteratedFDeriv 𝕜 Nat.zero f) s
rw [iteratedFDeriv_zero_eq_comp]
no goals
case zero
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : AnalyticOn 𝕜 f s
⊢ AnalyticOn 𝕜 (↑(LinearIsometryEquiv.symm (continuousMultilinearCurryFin0 𝕜 E F)) ∘ f) s
exact ((continuousMultilinearCurryFin0 𝕜 E F).symm : F →L[𝕜] E[×0]→L[𝕜] F).comp_analyticOn h
case succ
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : AnalyticOn 𝕜 f s
n : ℕ
IH : AnalyticOn 𝕜 (_root_.iteratedFDeriv 𝕜 n f) s
⊢ AnalyticOn 𝕜 (↑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F) ∘ _root_.fderiv 𝕜 (_root_.iteratedFDeriv 𝕜 n f))
    s
case succ
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : AnalyticOn 𝕜 f s
n : ℕ
IH : AnalyticOn 𝕜 (_root_.iteratedFDeriv 𝕜 n f) s
⊢ AnalyticOn 𝕜 (_root_.iteratedFDeriv 𝕜 (Nat.succ n) f) s
rw [iteratedFDeriv_succ_eq_comp_left]
case h.e'_9.h.e'_4
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : AnalyticOn 𝕜 f s
n : ℕ
IH : AnalyticOn 𝕜 (_root_.iteratedFDeriv 𝕜 n f) s
⊢ ↑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F) = ↑?g

case g
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : AnalyticOn 𝕜 f s
n : ℕ
IH : AnalyticOn 𝕜 (_root_.iteratedFDeriv 𝕜 n f) s
⊢ (E →L[𝕜] ContinuousMultilinearMap 𝕜 (fun i => E) F) →L[𝕜] ContinuousMultilinearMap 𝕜 (fun x => E) F
case succ
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : AnalyticOn 𝕜 f s
n : ℕ
IH : AnalyticOn 𝕜 (_root_.iteratedFDeriv 𝕜 n f) s
⊢ AnalyticOn 𝕜 (↑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F) ∘ _root_.fderiv 𝕜 (_root_.iteratedFDeriv 𝕜 n f))
    s
convert @ContinuousLinearMap.comp_analyticOn 𝕜 E
  ?_ (ContinuousMultilinearMap 𝕜 (fun _ : Fin (n + 1) ↦ E) F)
  ?_ ?_ ?_ ?_ ?_ ?_ ?_ ?_
  s ?g IH.fderiv
case h.e'_9.h.e'_4
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : AnalyticOn 𝕜 f s
n : ℕ
IH : AnalyticOn 𝕜 (_root_.iteratedFDeriv 𝕜 n f) s
⊢ ↑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F) =
    ↑↑(ContinuousLinearEquiv.mk (continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F).toLinearEquiv)
case h.e'_9.h.e'_4
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : AnalyticOn 𝕜 f s
n : ℕ
IH : AnalyticOn 𝕜 (_root_.iteratedFDeriv 𝕜 n f) s
⊢ ↑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F) = ↑?g

case g
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : AnalyticOn 𝕜 f s
n : ℕ
IH : AnalyticOn 𝕜 (_root_.iteratedFDeriv 𝕜 n f) s
⊢ (E →L[𝕜] ContinuousMultilinearMap 𝕜 (fun i => E) F) →L[𝕜] ContinuousMultilinearMap 𝕜 (fun x => E) F
case g =>
  exact ↑(continuousMultilinearCurryLeftEquiv 𝕜 (fun _ : Fin (n + 1) => E) F)
no goals
case h.e'_9.h.e'_4
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : AnalyticOn 𝕜 f s
n : ℕ
IH : AnalyticOn 𝕜 (_root_.iteratedFDeriv 𝕜 n f) s
⊢ ↑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F) =
    ↑↑(ContinuousLinearEquiv.mk (continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F).toLinearEquiv)
rfl
no goals
𝕜 : Type u_2
inst✝⁵ : NontriviallyNormedField 𝕜
E : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace 𝕜 E
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
f : E → F
x : E
s : Set E
inst✝ : CompleteSpace F
h : AnalyticOn 𝕜 f s
n : ℕ
IH : AnalyticOn 𝕜 (_root_.iteratedFDeriv 𝕜 n f) s
⊢ (E →L[𝕜] ContinuousMultilinearMap 𝕜 (fun i => E) F) →L[𝕜] ContinuousMultilinearMap 𝕜 (fun x => E) F
exact ↑(continuousMultilinearCurryLeftEquiv 𝕜 (fun _ : Fin (n + 1) => E) F)