-- Mathlib/Analysis/Analytic/IteratedFDeriv.lean
theorem HasFPowerSeriesWithinOnBall.iteratedFDerivWithin
    (h : HasFPowerSeriesWithinOnBall f p s x r) (h' : AnalyticOn 𝕜 f s)
    (k : ℕ) (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) :
    HasFPowerSeriesWithinOnBall (iteratedFDerivWithin 𝕜 k f s)
      (p.iteratedFDerivSeries k) s x r

Proof state:
case zero
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
⊢ HasFPowerSeriesWithinOnBall (iteratedFDerivWithin 𝕜 0 f s) (p.iteratedFDerivSeries 0) s x r

Tactic:
exact (continuousMultilinearCurryFin0 𝕜 E F).symm
  |>.toContinuousLinearEquiv.toContinuousLinearMap.comp_hasFPowerSeriesWithinOnBall h

Result:
no goals

Proof state:
case succ
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
k : ℕ
ih : HasFPowerSeriesWithinOnBall (iteratedFDerivWithin 𝕜 k f s) (p.iteratedFDerivSeries k) s x r
⊢ HasFPowerSeriesWithinOnBall (iteratedFDerivWithin 𝕜 (k + 1) f s) (p.iteratedFDerivSeries (k + 1)) s x r

Tactic:
rw [iteratedFDerivWithin_succ_eq_comp_left]

Result:
case succ
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
k : ℕ
ih : HasFPowerSeriesWithinOnBall (iteratedFDerivWithin 𝕜 k f s) (p.iteratedFDerivSeries k) s x r
⊢ HasFPowerSeriesWithinOnBall
    (⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F).symm ∘ fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 k f s) s)
    (p.iteratedFDerivSeries (k + 1)) s x r

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
k : ℕ
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
⊢ HasFPowerSeriesWithinOnBall (iteratedFDerivWithin 𝕜 k f s) (p.iteratedFDerivSeries k) s x r

Tactic:
induction k with
| zero =>
  exact (continuousMultilinearCurryFin0 𝕜 E F).symm
    |>.toContinuousLinearEquiv.toContinuousLinearMap.comp_hasFPowerSeriesWithinOnBall h
| succ k ih =>
  rw [iteratedFDerivWithin_succ_eq_comp_left]
  apply (continuousMultilinearCurryLeftEquiv 𝕜 (fun _ : Fin (k + 1) ↦ E) F).symm
    |>.toContinuousLinearEquiv.toContinuousLinearMap.comp_hasFPowerSeriesWithinOnBall
      (ih.fderivWithin_of_mem_of_analyticOn (h'.iteratedFDerivWithin hs _) hs hx)

Result:
no goals

Proof state:
case succ
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : AnalyticOn 𝕜 f s
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
k : ℕ
ih : HasFPowerSeriesWithinOnBall (iteratedFDerivWithin 𝕜 k f s) (p.iteratedFDerivSeries k) s x r
⊢ HasFPowerSeriesWithinOnBall
    (⇑(continuousMultilinearCurryLeftEquiv 𝕜 (fun x => E) F).symm ∘ fderivWithin 𝕜 (iteratedFDerivWithin 𝕜 k f s) s)
    (p.iteratedFDerivSeries (k + 1)) s x r

Tactic:
apply (continuousMultilinearCurryLeftEquiv 𝕜 (fun _ : Fin (k + 1) ↦ E) F).symm
  |>.toContinuousLinearEquiv.toContinuousLinearMap.comp_hasFPowerSeriesWithinOnBall
    (ih.fderivWithin_of_mem_of_analyticOn (h'.iteratedFDerivWithin hs _) hs hx)

Result:
no goals