-- Mathlib/Analysis/Analytic/IteratedFDeriv.lean
theorem HasFPowerSeriesWithinOnBall.iteratedFDerivWithin_eq_sum_of_completeSpace [CompleteSpace F]
    (h : HasFPowerSeriesWithinOnBall f p s x r)
    (hs : UniqueDiffOn 𝕜 s) (hx : x ∈ s) {n : ℕ} (v : Fin n → E) :
    iteratedFDerivWithin 𝕜 n f s x v = ∑ σ : Perm (Fin n), p n (fun i ↦ v (σ i))

Proof state:
case h
𝕜 : 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∞
inst✝ : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
this : iteratedFDerivWithin 𝕜 n f s x = iteratedFDerivWithin 𝕜 n f (s ∩ EMetric.ball x r) x
⊢ HasFPowerSeriesWithinOnBall f p (s ∩ EMetric.ball x r) x ?r

Tactic:
exact h.mono inter_subset_left

Result:
no goals

Proof state:
case hs
𝕜 : 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∞
inst✝ : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
this : iteratedFDerivWithin 𝕜 n f s x = iteratedFDerivWithin 𝕜 n f (s ∩ EMetric.ball x r) x
⊢ UniqueDiffOn 𝕜 (s ∩ EMetric.ball x r)

Tactic:
exact hs.inter EMetric.isOpen_ball

Result:
no goals

Proof state:
case hx
𝕜 : 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∞
inst✝ : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
this : iteratedFDerivWithin 𝕜 n f s x = iteratedFDerivWithin 𝕜 n f (s ∩ EMetric.ball x r) x
⊢ x ∈ s ∩ EMetric.ball x r

Tactic:
exact ⟨hx, EMetric.mem_ball_self h.r_pos⟩

Result:
no goals

Proof state:
case h'
𝕜 : 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∞
inst✝ : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
this : iteratedFDerivWithin 𝕜 n f s x = iteratedFDerivWithin 𝕜 n f (s ∩ EMetric.ball x r) x
⊢ AnalyticOn 𝕜 f (s ∩ EMetric.ball x r)

Tactic:
apply h.analyticOn.mono

Result:
case h'
𝕜 : 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∞
inst✝ : CompleteSpace F
h : HasFPowerSeriesWithinOnBall f p s x r
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
v : Fin n → E
this : iteratedFDerivWithin 𝕜 n f s x = iteratedFDerivWithin 𝕜 n f (s ∩ EMetric.ball x r) x
⊢ s ∩ EMetric.ball x r ⊆ insert x s ∩ EMetric.ball x r