-- 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_emetric_ball :
    HasSum (fun n : ℕ ↦ (n ! : ℂ)⁻¹ • (z - c) ^ n • iteratedDeriv n f c) (f z)

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

Tactic:
lift r' to NNReal using ne_top_of_lt hr'

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

Tactic:
rw [← EMetric.mem_ball', Metric.emetric_ball_nnreal] at hzr'

Result:
case intro.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r : ENNReal
hf : DifferentiableOn ℂ f (EMetric.ball c r)
z : ℂ
hz : z ∈ EMetric.ball c r
r' : NNReal
hzr' : z ∈ Metric.ball c ↑r'
hr' : ↑r' < 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 : ENNReal
hf : DifferentiableOn ℂ f (EMetric.ball c r)
z : ℂ
hz : z ∈ EMetric.ball c r
r' : NNReal
hzr' : z ∈ Metric.ball c ↑r'
hr' : ↑r' < r
⊢ DifferentiableOn ℂ f (Metric.ball c ↑r')

Tactic:
rw [← Metric.emetric_ball_nnreal]

Result:
case intro.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r : ENNReal
hf : DifferentiableOn ℂ f (EMetric.ball c r)
z : ℂ
hz : z ∈ EMetric.ball c r
r' : NNReal
hzr' : z ∈ Metric.ball c ↑r'
hr' : ↑r' < r
⊢ DifferentiableOn ℂ f (EMetric.ball c ↑r')

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

Tactic:
obtain ⟨r', hzr', hr'⟩ := exists_between (EMetric.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 : ENNReal
hf : DifferentiableOn ℂ f (EMetric.ball c r)
z : ℂ
hz : z ∈ EMetric.ball c r
r' : ENNReal
hzr' : edist c z < r'
hr' : r' < 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 : ENNReal
hf : DifferentiableOn ℂ f (EMetric.ball c r)
z : ℂ
hz : z ∈ EMetric.ball c r
r' : NNReal
hzr' : z ∈ Metric.ball c ↑r'
hr' : ↑r' < r
⊢ HasSum (fun n => (↑n !)⁻¹ • (z - c) ^ n • iteratedDeriv n f c) (f z)

Tactic:
refine hasSum_taylorSeries_on_ball ?_ hzr'

Result:
case intro.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r : ENNReal
hf : DifferentiableOn ℂ f (EMetric.ball c r)
z : ℂ
hz : z ∈ EMetric.ball c r
r' : NNReal
hzr' : z ∈ Metric.ball c ↑r'
hr' : ↑r' < r
⊢ DifferentiableOn ℂ f (Metric.ball c ↑r')

Proof state:
case intro.intro.intro
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r : ENNReal
hf : DifferentiableOn ℂ f (EMetric.ball c r)
z : ℂ
hz : z ∈ EMetric.ball c r
r' : NNReal
hzr' : z ∈ Metric.ball c ↑r'
hr' : ↑r' < r
⊢ DifferentiableOn ℂ f (EMetric.ball c ↑r')

Tactic:
exact hf.mono <| EMetric.ball_subset_ball hr'.le

Result:
no goals