-- 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's
𝕜 : 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 ⊆ EMetric.ball x r

Tactic:
exact inter_subset_right

Result:
no goals

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∞
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
⊢ (iteratedFDerivWithin 𝕜 n f s x) v = ∑ σ : Perm (Fin n), (p n) fun i => v (σ i)

Tactic:
rw [this]

Result:
𝕜 : 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
⊢ (iteratedFDerivWithin 𝕜 n f (s ∩ EMetric.ball x r) x) v = ∑ σ : Perm (Fin n), (p n) fun i => v (σ i)

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∞
inst✝ : 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)

Tactic:
have : iteratedFDerivWithin 𝕜 n f s x
    = iteratedFDerivWithin 𝕜 n f (s ∩ EMetric.ball x r) x :=
  (iteratedFDerivWithin_inter_open EMetric.isOpen_ball (EMetric.mem_ball_self h.r_pos)).symm

Result:
𝕜 : 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
⊢ (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
⊢ s ∩ EMetric.ball x r ⊆ insert x s ∩ EMetric.ball x r

Tactic:
rw [insert_eq_of_mem hx]

Result:
no goals

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∞
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
⊢ (iteratedFDerivWithin 𝕜 n f (s ∩ EMetric.ball x r) x) v = ∑ σ : Perm (Fin n), (p n) fun i => v (σ i)

Tactic:
apply HasFPowerSeriesWithinOnBall.iteratedFDerivWithin_eq_sum_of_subset

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
⊢ HasFPowerSeriesWithinOnBall f p (s ∩ EMetric.ball x r) x ?r

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)

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)

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

case h's
𝕜 : 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 ⊆ EMetric.ball x ?r

case r
𝕜 : 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
⊢ ℝ≥0∞