-- Mathlib/Analysis/Complex/TaylorSeries.lean
/-- A function that is complex differentiable on the open ball of radius `r` around `c`
is given by evaluating its Taylor series at `c` on this open ball. -/
lemma hasSum_taylorSeries_on_ball :
    HasSum (fun n : ℕ ↦ (n ! : ℂ)⁻¹ • (z - c) ^ n • iteratedDeriv n f c) (f z)

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r : ℝ
hf : DifferentiableOn ℂ f (Metric.ball c r)
z : ℂ
hz : z ∈ Metric.ball c r
⊢ HasSum (fun n => (↑n !)⁻¹ • (z - c) ^ n • iteratedDeriv n f c) (f z)

Tactic:
obtain ⟨r', hr', hr'₀, hzr'⟩ : ∃ r' < r, 0 < r' ∧ z ∈ Metric.ball c r' := by
  obtain ⟨r', h₁, h₂⟩ := exists_between (Metric.mem_ball'.mp hz)
  exact ⟨r', h₂, Metric.pos_of_mem_ball h₁, Metric.mem_ball'.mpr h₁⟩

Result:
case intro.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r : ℝ
hf : DifferentiableOn ℂ f (Metric.ball c r)
z : ℂ
hz : z ∈ Metric.ball c r
r' : ℝ
hr' : r' < r
hr'₀ : 0 < r'
hzr' : z ∈ Metric.ball c r'
⊢ HasSum (fun n => (↑n !)⁻¹ • (z - c) ^ n • iteratedDeriv n f c) (f z)

Proof state:
case intro.intro.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r : ℝ
hf : DifferentiableOn ℂ f (Metric.ball c r)
z : ℂ
hz : z ∈ Metric.ball c r
r' : NNReal
hr' : ↑r' < r
hr'₀ : 0 < ↑r'
hzr' : z ∈ Metric.ball c ↑r'
hz' : z - c ∈ EMetric.ball 0 ↑r'
⊢ HasSum (fun n => (↑n !)⁻¹ • (z - c) ^ n • iteratedDeriv n f c) (f z)

Tactic:
have H := (hf.mono <| Metric.closedBall_subset_ball hr').hasFPowerSeriesOnBall hr'₀
    |>.hasSum_iteratedFDeriv hz'

Result:
case intro.intro.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r : ℝ
hf : DifferentiableOn ℂ f (Metric.ball c r)
z : ℂ
hz : z ∈ Metric.ball c r
r' : NNReal
hr' : ↑r' < r
hr'₀ : 0 < ↑r'
hzr' : z ∈ Metric.ball c ↑r'
hz' : z - c ∈ EMetric.ball 0 ↑r'
H : HasSum (fun n => (↑n !)⁻¹ • (iteratedFDeriv ℂ n f c) fun x => z - c) (f (c + (z - c)))
⊢ HasSum (fun n => (↑n !)⁻¹ • (z - c) ^ n • iteratedDeriv n f c) (f z)

Proof state:
case intro.intro.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r : ℝ
hf : DifferentiableOn ℂ f (Metric.ball c r)
z : ℂ
hz : z ∈ Metric.ball c r
r' : NNReal
hr' : ↑r' < r
hr'₀ : 0 < ↑r'
hzr' : z ∈ Metric.ball c ↑r'
hz' : z - c ∈ EMetric.ball 0 ↑r'
H : HasSum (fun n => (↑n !)⁻¹ • (iteratedFDeriv ℂ n f c) fun x => z - c) (f z)
⊢ HasSum (fun n => (↑n !)⁻¹ • (z - c) ^ n • iteratedDeriv n f c) (f z)

Tactic:
convert H using 4 with n

Result:
case h.e'_5.h.h.e'_6
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r : ℝ
hf : DifferentiableOn ℂ f (Metric.ball c r)
z : ℂ
hz : z ∈ Metric.ball c r
r' : NNReal
hr' : ↑r' < r
hr'₀ : 0 < ↑r'
hzr' : z ∈ Metric.ball c ↑r'
hz' : z - c ∈ EMetric.ball 0 ↑r'
H : HasSum (fun n => (↑n !)⁻¹ • (iteratedFDeriv ℂ n f c) fun x => z - c) (f z)
n : ℕ
⊢ (z - c) ^ n • iteratedDeriv n f c = (iteratedFDeriv ℂ n f c) fun x => z - c

Proof state:
case intro.intro.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r : ℝ
hf : DifferentiableOn ℂ f (Metric.ball c r)
z : ℂ
hz : z ∈ Metric.ball c r
r' : NNReal
hr' : ↑r' < r
hr'₀ : 0 < ↑r'
hzr' : z ∈ Metric.ball c ↑r'
hz' : z - c ∈ EMetric.ball 0 ↑r'
H : HasSum (fun n => (↑n !)⁻¹ • (iteratedFDeriv ℂ n f c) fun x => z - c) (f (c + (z - c)))
⊢ HasSum (fun n => (↑n !)⁻¹ • (z - c) ^ n • iteratedDeriv n f c) (f z)

Tactic:
simp only [add_sub_cancel] at H

Result:
case intro.intro.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r : ℝ
hf : DifferentiableOn ℂ f (Metric.ball c r)
z : ℂ
hz : z ∈ Metric.ball c r
r' : NNReal
hr' : ↑r' < r
hr'₀ : 0 < ↑r'
hzr' : z ∈ Metric.ball c ↑r'
hz' : z - c ∈ EMetric.ball 0 ↑r'
H : HasSum (fun n => (↑n !)⁻¹ • (iteratedFDeriv ℂ n f c) fun x => z - c) (f z)
⊢ HasSum (fun n => (↑n !)⁻¹ • (z - c) ^ n • iteratedDeriv n f c) (f z)

Proof state:
case intro.intro.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r : ℝ
hf : DifferentiableOn ℂ f (Metric.ball c r)
z : ℂ
hz : z ∈ Metric.ball c r
r' : NNReal
hr' : ↑r' < r
hr'₀ : 0 < ↑r'
hzr' : z ∈ Metric.ball c ↑r'
⊢ HasSum (fun n => (↑n !)⁻¹ • (z - c) ^ n • iteratedDeriv n f c) (f z)

Tactic:
have hz' : z - c ∈ EMetric.ball 0 r' := by
  rw [Metric.emetric_ball_nnreal]
  exact mem_ball_zero_iff.mpr hzr'

Result:
case intro.intro.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r : ℝ
hf : DifferentiableOn ℂ f (Metric.ball c r)
z : ℂ
hz : z ∈ Metric.ball c r
r' : NNReal
hr' : ↑r' < r
hr'₀ : 0 < ↑r'
hzr' : z ∈ Metric.ball c ↑r'
hz' : z - c ∈ EMetric.ball 0 ↑r'
⊢ HasSum (fun n => (↑n !)⁻¹ • (z - c) ^ n • iteratedDeriv n f c) (f z)

Proof state:
case intro.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r : ℝ
hf : DifferentiableOn ℂ f (Metric.ball c r)
z : ℂ
hz : z ∈ Metric.ball c r
r' : ℝ
hr' : r' < r
hr'₀ : 0 < r'
hzr' : z ∈ Metric.ball c r'
⊢ HasSum (fun n => (↑n !)⁻¹ • (z - c) ^ n • iteratedDeriv n f c) (f z)

Tactic:
lift r' to NNReal using hr'₀.le

Result:
case intro.intro.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r : ℝ
hf : DifferentiableOn ℂ f (Metric.ball c r)
z : ℂ
hz : z ∈ Metric.ball c r
r' : NNReal
hr' : ↑r' < r
hr'₀ : 0 < ↑r'
hzr' : z ∈ Metric.ball c ↑r'
⊢ HasSum (fun n => (↑n !)⁻¹ • (z - c) ^ n • iteratedDeriv n f c) (f z)

Proof state:
case h.e'_5.h.h.e'_6
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r : ℝ
hf : DifferentiableOn ℂ f (Metric.ball c r)
z : ℂ
hz : z ∈ Metric.ball c r
r' : NNReal
hr' : ↑r' < r
hr'₀ : 0 < ↑r'
hzr' : z ∈ Metric.ball c ↑r'
hz' : z - c ∈ EMetric.ball 0 ↑r'
H : HasSum (fun n => (↑n !)⁻¹ • (iteratedFDeriv ℂ n f c) fun x => z - c) (f z)
n : ℕ
⊢ (z - c) ^ n • iteratedDeriv n f c = (iteratedFDeriv ℂ n f c) fun x => z - c

Tactic:
simpa only [iteratedDeriv_eq_iteratedFDeriv, smul_eq_mul, mul_one, Finset.prod_const,
  Finset.card_fin]
  using ((iteratedFDeriv ℂ n f c).map_smul_univ (fun _ ↦ z - c) (fun _ ↦ 1)).symm

Result:
no goals

Proof state:
case intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r : ℝ
hf : DifferentiableOn ℂ f (Metric.ball c r)
z : ℂ
hz : z ∈ Metric.ball c r
r' : ℝ
h₁ : dist c z < r'
h₂ : r' < r
⊢ ∃ r' < r, 0 < r' ∧ z ∈ Metric.ball c r'

Tactic:
exact ⟨r', h₂, Metric.pos_of_mem_ball h₁, Metric.mem_ball'.mpr h₁⟩

Result:
no goals

Proof state:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r : ℝ
hf : DifferentiableOn ℂ f (Metric.ball c r)
z : ℂ
hz : z ∈ Metric.ball c r
⊢ ∃ r' < r, 0 < r' ∧ z ∈ Metric.ball c r'

Tactic:
obtain ⟨r', h₁, h₂⟩ := exists_between (Metric.mem_ball'.mp hz)

Result:
case intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r : ℝ
hf : DifferentiableOn ℂ f (Metric.ball c r)
z : ℂ
hz : z ∈ Metric.ball c r
r' : ℝ
h₁ : dist c z < r'
h₂ : r' < r
⊢ ∃ r' < r, 0 < r' ∧ z ∈ Metric.ball c r'