-- Mathlib/Analysis/Calculus/FDeriv/Analytic.lean
theorem AnalyticOn.iteratedFDerivWithin (h : AnalyticOn 𝕜 f s)
    (hu : UniqueDiffOn 𝕜 s) (n : ℕ) :
    AnalyticOn 𝕜 (iteratedFDerivWithin 𝕜 n f s) s

Proof state:
case zero
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : AnalyticOn 𝕜 f s
hu : UniqueDiffOn 𝕜 s
⊢ AnalyticOn 𝕜 (iteratedFDerivWithin 𝕜 0 f s) s

Tactic:
rw [iteratedFDerivWithin_zero_eq_comp]

Result:
case zero
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : AnalyticOn 𝕜 f s
hu : UniqueDiffOn 𝕜 s
⊢ AnalyticOn 𝕜 (⇑(continuousMultilinearCurryFin0 𝕜 E F).symm ∘ f) s

Proof state:
case zero
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : AnalyticOn 𝕜 f s
hu : UniqueDiffOn 𝕜 s
⊢ AnalyticOn 𝕜 (⇑(continuousMultilinearCurryFin0 𝕜 E F).symm ∘ f) s

Tactic:
exact ((continuousMultilinearCurryFin0 𝕜 E F).symm : F →L[𝕜] E[×0]→L[𝕜] F)
  |>.comp_analyticOn h

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : AnalyticOn 𝕜 f s
hu : UniqueDiffOn 𝕜 s
n : ℕ
IH : AnalyticOn 𝕜 (iteratedFDerivWithin 𝕜 n f s) s
⊢ AnalyticOnNhd 𝕜 (⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F).symm) univ

Tactic:
apply LinearIsometryEquiv.analyticOnNhd

Result:
no goals

Proof state:
case succ
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : AnalyticOn 𝕜 f s
hu : UniqueDiffOn 𝕜 s
n : ℕ
IH : AnalyticOn 𝕜 (iteratedFDerivWithin 𝕜 n f s) s
⊢ AnalyticOn 𝕜
    (⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F).symm ∘ fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f s) s) s

Tactic:
apply AnalyticOnNhd.comp_analyticOn _ (IH.fderivWithin hu) (mapsTo_univ _ _)

Result:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : AnalyticOn 𝕜 f s
hu : UniqueDiffOn 𝕜 s
n : ℕ
IH : AnalyticOn 𝕜 (iteratedFDerivWithin 𝕜 n f s) s
⊢ AnalyticOnNhd 𝕜 (⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F).symm) univ

Proof state:
case succ
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : AnalyticOn 𝕜 f s
hu : UniqueDiffOn 𝕜 s
n : ℕ
IH : AnalyticOn 𝕜 (iteratedFDerivWithin 𝕜 n f s) s
⊢ AnalyticOn 𝕜 (iteratedFDerivWithin 𝕜 (n + 1) f s) s

Tactic:
rw [iteratedFDerivWithin_succ_eq_comp_left]

Result:
case succ
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : AnalyticOn 𝕜 f s
hu : UniqueDiffOn 𝕜 s
n : ℕ
IH : AnalyticOn 𝕜 (iteratedFDerivWithin 𝕜 n f s) s
⊢ AnalyticOn 𝕜
    (⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F).symm ∘ fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 n f s) s) s

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
s : Set E
h : AnalyticOn 𝕜 f s
hu : UniqueDiffOn 𝕜 s
n : ℕ
⊢ AnalyticOn 𝕜 (iteratedFDerivWithin 𝕜 n f s) s

Tactic:
induction n with
| zero =>
  rw [iteratedFDerivWithin_zero_eq_comp]
  exact ((continuousMultilinearCurryFin0 𝕜 E F).symm : F →L[𝕜] E[×0]→L[𝕜] F)
    |>.comp_analyticOn h
| succ n IH =>
  rw [iteratedFDerivWithin_succ_eq_comp_left]
  apply AnalyticOnNhd.comp_analyticOn _ (IH.fderivWithin hu) (mapsTo_univ _ _)
  apply LinearIsometryEquiv.analyticOnNhd

Result:
no goals