Theorem: analyticOn_ball_radius (Ray/Analytic/Uniform.lean)

State before:
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
⊢ ∃ p, HasFPowerSeriesOnBall f p z ↑r
Tactic:
have h0 := analyticOn_small_cball h (r / 2) (NNReal.half_lt_self <| rp.ne')
State after:
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
⊢ ∃ p, HasFPowerSeriesOnBall f p z ↑r

State before:
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
⊢ ∃ p, HasFPowerSeriesOnBall f p z ↑r
Tactic:
rcases analyticOn_cball_radius (half_pos rp) h0 with ⟨p, ph⟩
State after:
case intro
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
⊢ ∃ p, HasFPowerSeriesOnBall f p z ↑r

State before:
case intro
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
⊢ ∃ p, HasFPowerSeriesOnBall f p z ↑r
Tactic:
set R := FormalMultilinearSeries.radius p
State after:
case intro
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
⊢ ∃ p, HasFPowerSeriesOnBall f p z ↑r

State before:
case intro
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
⊢ ∃ p, HasFPowerSeriesOnBall f p z ↑r
Tactic:
refine
  ⟨p, {
      r_le := ?_
      r_pos := ENNReal.coe_pos.mpr rp
      hasSum := ?_ }⟩
State after:
case intro.refine_1
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
⊢ ↑r ≤ p.radius

case intro.refine_2
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
⊢ ∀ {y : ℂ}, y ∈ EMetric.ball 0 ↑r → HasSum (fun n => (p n) fun x => y) (f (z + y))

State before:
case intro.refine_1
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
⊢ ↑r ≤ p.radius
Tactic:
apply ENNReal.le_of_forall_pos_nnreal_lt
State after:
case intro.refine_1.h
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
⊢ ∀ (r_1 : ℝ≥0), 0 < r_1 → ↑r_1 < ↑r → ↑r_1 ≤ p.radius

State before:
case intro.refine_1.h
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
⊢ ∀ (r_1 : ℝ≥0), 0 < r_1 → ↑r_1 < ↑r → ↑r_1 ≤ p.radius
Tactic:
intro t tp tr
State after:
case intro.refine_1.h
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
t : ℝ≥0
tp : 0 < t
tr : ↑t < ↑r
⊢ ↑t ≤ p.radius

State before:
case intro.refine_1.h
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
t : ℝ≥0
tp : 0 < t
tr : ↑t < ↑r
⊢ ↑t ≤ p.radius
Tactic:
have ht := analyticOn_small_cball h t (ENNReal.coe_lt_coe.mp tr)
State after:
case intro.refine_1.h
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
t : ℝ≥0
tp : 0 < t
tr : ↑t < ↑r
ht : AnalyticOn ℂ f (closedBall z ↑t)
⊢ ↑t ≤ p.radius

State before:
case intro.refine_1.h
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
t : ℝ≥0
tp : 0 < t
tr : ↑t < ↑r
ht : AnalyticOn ℂ f (closedBall z ↑t)
⊢ ↑t ≤ p.radius
Tactic:
rcases analyticOn_cball_radius tp ht with ⟨p', hp'⟩
State after:
case intro.refine_1.h.intro
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
t : ℝ≥0
tp : 0 < t
tr : ↑t < ↑r
ht : AnalyticOn ℂ f (closedBall z ↑t)
p' : FormalMultilinearSeries ℂ ℂ ℂ
hp' : HasFPowerSeriesOnBall f p' z ↑t
⊢ ↑t ≤ p.radius

State before:
case intro.refine_1.h.intro
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
t : ℝ≥0
tp : 0 < t
tr : ↑t < ↑r
ht : AnalyticOn ℂ f (closedBall z ↑t)
p' : FormalMultilinearSeries ℂ ℂ ℂ
hp' : HasFPowerSeriesOnBall f p' z ↑t
⊢ ↑t ≤ p.radius
Tactic:
have pp : p = p' := HasFPowerSeriesAt.eq_formalMultilinearSeries ⟨↑(r / 2), ph⟩ ⟨t, hp'⟩
State after:
case intro.refine_1.h.intro
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
t : ℝ≥0
tp : 0 < t
tr : ↑t < ↑r
ht : AnalyticOn ℂ f (closedBall z ↑t)
p' : FormalMultilinearSeries ℂ ℂ ℂ
hp' : HasFPowerSeriesOnBall f p' z ↑t
pp : p = p'
⊢ ↑t ≤ p.radius

State before:
case intro.refine_1.h.intro
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
t : ℝ≥0
tp : 0 < t
tr : ↑t < ↑r
ht : AnalyticOn ℂ f (closedBall z ↑t)
p' : FormalMultilinearSeries ℂ ℂ ℂ
hp' : HasFPowerSeriesOnBall f p' z ↑t
pp : p = p'
⊢ ↑t ≤ p.radius
Tactic:
rw [← pp] at hp'
State after:
case intro.refine_1.h.intro
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
t : ℝ≥0
tp : 0 < t
tr : ↑t < ↑r
ht : AnalyticOn ℂ f (closedBall z ↑t)
p' : FormalMultilinearSeries ℂ ℂ ℂ
hp' : HasFPowerSeriesOnBall f p z ↑t
pp : p = p'
⊢ ↑t ≤ p.radius

State before:
case intro.refine_1.h.intro
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
t : ℝ≥0
tp : 0 < t
tr : ↑t < ↑r
ht : AnalyticOn ℂ f (closedBall z ↑t)
p' : FormalMultilinearSeries ℂ ℂ ℂ
hp' : HasFPowerSeriesOnBall f p z ↑t
pp : p = p'
⊢ ↑t ≤ p.radius
Tactic:
refine hp'.r_le
State after:
no goals

State before:
case intro.refine_2
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
⊢ ∀ {y : ℂ}, y ∈ EMetric.ball 0 ↑r → HasSum (fun n => (p n) fun x => y) (f (z + y))
Tactic:
intro y yr
State after:
case intro.refine_2
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
y : ℂ
yr : y ∈ EMetric.ball 0 ↑r
⊢ HasSum (fun n => (p n) fun x => y) (f (z + y))

State before:
case intro.refine_2
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
y : ℂ
yr : y ∈ EMetric.ball 0 ↑r
⊢ HasSum (fun n => (p n) fun x => y) (f (z + y))
Tactic:
rw [EMetric.ball, Set.mem_setOf] at yr
State after:
case intro.refine_2
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
y : ℂ
yr : edist y 0 < ↑r
⊢ HasSum (fun n => (p n) fun x => y) (f (z + y))

State before:
case intro.refine_2
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
y : ℂ
yr : edist y 0 < ↑r
⊢ HasSum (fun n => (p n) fun x => y) (f (z + y))
Tactic:
rcases exists_between yr with ⟨t, t0, t1⟩
State after:
case intro.refine_2.intro.intro
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
y : ℂ
yr : edist y 0 < ↑r
t : ENNReal
t0 : edist y 0 < t
t1 : t < ↑r
⊢ HasSum (fun n => (p n) fun x => y) (f (z + y))

State before:
case intro.refine_2.intro.intro
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
y : ℂ
yr : edist y 0 < ↑r
t : ENNReal
t0 : edist y 0 < t
t1 : t < ↑r
⊢ HasSum (fun n => (p n) fun x => y) (f (z + y))
Tactic:
have t1' : t.toNNReal < r := by
  rw [← WithTop.coe_lt_coe]; exact lt_of_le_of_lt ENNReal.coe_toNNReal_le_self t1
State after:
case intro.refine_2.intro.intro
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
y : ℂ
yr : edist y 0 < ↑r
t : ENNReal
t0 : edist y 0 < t
t1 : t < ↑r
t1' : t.toNNReal < r
⊢ HasSum (fun n => (p n) fun x => y) (f (z + y))

State before:
case intro.refine_2.intro.intro
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
y : ℂ
yr : edist y 0 < ↑r
t : ENNReal
t0 : edist y 0 < t
t1 : t < ↑r
t1' : t.toNNReal < r
⊢ HasSum (fun n => (p n) fun x => y) (f (z + y))
Tactic:
have ht := analyticOn_small_cball h t.toNNReal t1'
State after:
case intro.refine_2.intro.intro
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
y : ℂ
yr : edist y 0 < ↑r
t : ENNReal
t0 : edist y 0 < t
t1 : t < ↑r
t1' : t.toNNReal < r
ht : AnalyticOn ℂ f (closedBall z ↑t.toNNReal)
⊢ HasSum (fun n => (p n) fun x => y) (f (z + y))

State before:
case intro.refine_2.intro.intro
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
y : ℂ
yr : edist y 0 < ↑r
t : ENNReal
t0 : edist y 0 < t
t1 : t < ↑r
t1' : t.toNNReal < r
ht : AnalyticOn ℂ f (closedBall z ↑t.toNNReal)
⊢ HasSum (fun n => (p n) fun x => y) (f (z + y))
Tactic:
have tp : 0 < ENNReal.toNNReal t :=
  ENNReal.toNNReal_pos (ne_of_gt <| pos_of_gt t0) (ne_top_of_lt t1)
State after:
case intro.refine_2.intro.intro
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
y : ℂ
yr : edist y 0 < ↑r
t : ENNReal
t0 : edist y 0 < t
t1 : t < ↑r
t1' : t.toNNReal < r
ht : AnalyticOn ℂ f (closedBall z ↑t.toNNReal)
tp : 0 < t.toNNReal
⊢ HasSum (fun n => (p n) fun x => y) (f (z + y))

State before:
case intro.refine_2.intro.intro
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
y : ℂ
yr : edist y 0 < ↑r
t : ENNReal
t0 : edist y 0 < t
t1 : t < ↑r
t1' : t.toNNReal < r
ht : AnalyticOn ℂ f (closedBall z ↑t.toNNReal)
tp : 0 < t.toNNReal
⊢ HasSum (fun n => (p n) fun x => y) (f (z + y))
Tactic:
rcases analyticOn_cball_radius tp ht with ⟨p', hp'⟩
State after:
case intro.refine_2.intro.intro.intro
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
y : ℂ
yr : edist y 0 < ↑r
t : ENNReal
t0 : edist y 0 < t
t1 : t < ↑r
t1' : t.toNNReal < r
ht : AnalyticOn ℂ f (closedBall z ↑t.toNNReal)
tp : 0 < t.toNNReal
p' : FormalMultilinearSeries ℂ ℂ ℂ
hp' : HasFPowerSeriesOnBall f p' z ↑t.toNNReal
⊢ HasSum (fun n => (p n) fun x => y) (f (z + y))

State before:
case intro.refine_2.intro.intro.intro
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
y : ℂ
yr : edist y 0 < ↑r
t : ENNReal
t0 : edist y 0 < t
t1 : t < ↑r
t1' : t.toNNReal < r
ht : AnalyticOn ℂ f (closedBall z ↑t.toNNReal)
tp : 0 < t.toNNReal
p' : FormalMultilinearSeries ℂ ℂ ℂ
hp' : HasFPowerSeriesOnBall f p' z ↑t.toNNReal
⊢ HasSum (fun n => (p n) fun x => y) (f (z + y))
Tactic:
have pp : p = p' :=
  HasFPowerSeriesAt.eq_formalMultilinearSeries ⟨↑(r / 2), ph⟩ ⟨t.toNNReal, hp'⟩
State after:
case intro.refine_2.intro.intro.intro
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
y : ℂ
yr : edist y 0 < ↑r
t : ENNReal
t0 : edist y 0 < t
t1 : t < ↑r
t1' : t.toNNReal < r
ht : AnalyticOn ℂ f (closedBall z ↑t.toNNReal)
tp : 0 < t.toNNReal
p' : FormalMultilinearSeries ℂ ℂ ℂ
hp' : HasFPowerSeriesOnBall f p' z ↑t.toNNReal
pp : p = p'
⊢ HasSum (fun n => (p n) fun x => y) (f (z + y))

State before:
case intro.refine_2.intro.intro.intro
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
y : ℂ
yr : edist y 0 < ↑r
t : ENNReal
t0 : edist y 0 < t
t1 : t < ↑r
t1' : t.toNNReal < r
ht : AnalyticOn ℂ f (closedBall z ↑t.toNNReal)
tp : 0 < t.toNNReal
p' : FormalMultilinearSeries ℂ ℂ ℂ
hp' : HasFPowerSeriesOnBall f p' z ↑t.toNNReal
pp : p = p'
⊢ HasSum (fun n => (p n) fun x => y) (f (z + y))
Tactic:
rw [← pp] at hp'
State after:
case intro.refine_2.intro.intro.intro
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
y : ℂ
yr : edist y 0 < ↑r
t : ENNReal
t0 : edist y 0 < t
t1 : t < ↑r
t1' : t.toNNReal < r
ht : AnalyticOn ℂ f (closedBall z ↑t.toNNReal)
tp : 0 < t.toNNReal
p' : FormalMultilinearSeries ℂ ℂ ℂ
hp' : HasFPowerSeriesOnBall f p z ↑t.toNNReal
pp : p = p'
⊢ HasSum (fun n => (p n) fun x => y) (f (z + y))

State before:
case intro.refine_2.intro.intro.intro
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
y : ℂ
yr : edist y 0 < ↑r
t : ENNReal
t0 : edist y 0 < t
t1 : t < ↑r
t1' : t.toNNReal < r
ht : AnalyticOn ℂ f (closedBall z ↑t.toNNReal)
tp : 0 < t.toNNReal
p' : FormalMultilinearSeries ℂ ℂ ℂ
hp' : HasFPowerSeriesOnBall f p z ↑t.toNNReal
pp : p = p'
⊢ HasSum (fun n => (p n) fun x => y) (f (z + y))
Tactic:
refine hp'.hasSum ?_
State after:
case intro.refine_2.intro.intro.intro
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
y : ℂ
yr : edist y 0 < ↑r
t : ENNReal
t0 : edist y 0 < t
t1 : t < ↑r
t1' : t.toNNReal < r
ht : AnalyticOn ℂ f (closedBall z ↑t.toNNReal)
tp : 0 < t.toNNReal
p' : FormalMultilinearSeries ℂ ℂ ℂ
hp' : HasFPowerSeriesOnBall f p z ↑t.toNNReal
pp : p = p'
⊢ y ∈ EMetric.ball 0 ↑t.toNNReal

State before:
case intro.refine_2.intro.intro.intro
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
y : ℂ
yr : edist y 0 < ↑r
t : ENNReal
t0 : edist y 0 < t
t1 : t < ↑r
t1' : t.toNNReal < r
ht : AnalyticOn ℂ f (closedBall z ↑t.toNNReal)
tp : 0 < t.toNNReal
p' : FormalMultilinearSeries ℂ ℂ ℂ
hp' : HasFPowerSeriesOnBall f p z ↑t.toNNReal
pp : p = p'
⊢ y ∈ EMetric.ball 0 ↑t.toNNReal
Tactic:
rw [EMetric.ball, Set.mem_setOf]
State after:
case intro.refine_2.intro.intro.intro
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
y : ℂ
yr : edist y 0 < ↑r
t : ENNReal
t0 : edist y 0 < t
t1 : t < ↑r
t1' : t.toNNReal < r
ht : AnalyticOn ℂ f (closedBall z ↑t.toNNReal)
tp : 0 < t.toNNReal
p' : FormalMultilinearSeries ℂ ℂ ℂ
hp' : HasFPowerSeriesOnBall f p z ↑t.toNNReal
pp : p = p'
⊢ edist y 0 < ↑t.toNNReal

State before:
case intro.refine_2.intro.intro.intro
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
y : ℂ
yr : edist y 0 < ↑r
t : ENNReal
t0 : edist y 0 < t
t1 : t < ↑r
t1' : t.toNNReal < r
ht : AnalyticOn ℂ f (closedBall z ↑t.toNNReal)
tp : 0 < t.toNNReal
p' : FormalMultilinearSeries ℂ ℂ ℂ
hp' : HasFPowerSeriesOnBall f p z ↑t.toNNReal
pp : p = p'
⊢ edist y 0 < ↑t.toNNReal
Tactic:
calc edist y 0
  _ < t := t0
  _ = ↑t.toNNReal := (ENNReal.coe_toNNReal <| ne_top_of_lt t1).symm
State after:
no goals

State before:
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
y : ℂ
yr : edist y 0 < ↑r
t : ENNReal
t0 : edist y 0 < t
t1 : t < ↑r
⊢ t.toNNReal < r
Tactic:
rw [← WithTop.coe_lt_coe]
State after:
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
y : ℂ
yr : edist y 0 < ↑r
t : ENNReal
t0 : edist y 0 < t
t1 : t < ↑r
⊢ ↑t.toNNReal < ↑r

State before:
f : ℂ → ℂ
z : ℂ
r : ℝ≥0
rp : r > 0
h : AnalyticOn ℂ f (ball z ↑r)
h0 : AnalyticOn ℂ f (closedBall z ↑(r / 2))
p : FormalMultilinearSeries ℂ ℂ ℂ
ph : HasFPowerSeriesOnBall f p z ↑(r / 2)
R : ENNReal := p.radius
y : ℂ
yr : edist y 0 < ↑r
t : ENNReal
t0 : edist y 0 < t
t1 : t < ↑r
⊢ ↑t.toNNReal < ↑r
Tactic:
exact lt_of_le_of_lt ENNReal.coe_toNNReal_le_self t1
State after:
no goals