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

State before:
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
o : IsOpen s
h : ∀ (n : I), AnalyticOn ℂ (f n) s
u : TendstoUniformlyOn f g atTop s
⊢ AnalyticOn ℂ g s
Tactic:
intro c hc
State after:
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
o : IsOpen s
h : ∀ (n : I), AnalyticOn ℂ (f n) s
u : TendstoUniformlyOn f g atTop s
c : ℂ
hc : c ∈ s
⊢ AnalyticAt ℂ g c

State before:
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
o : IsOpen s
h : ∀ (n : I), AnalyticOn ℂ (f n) s
u : TendstoUniformlyOn f g atTop s
c : ℂ
hc : c ∈ s
⊢ AnalyticAt ℂ g c
Tactic:
rcases Metric.nhds_basis_closedBall.mem_iff.mp (o.mem_nhds hc) with ⟨r, rp, cb⟩
State after:
case intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
o : IsOpen s
h : ∀ (n : I), AnalyticOn ℂ (f n) s
u : TendstoUniformlyOn f g atTop s
c : ℂ
hc : c ∈ s
r : ℝ
rp : 0 < r
cb : closedBall c r ⊆ s
⊢ AnalyticAt ℂ g c

State before:
case intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
o : IsOpen s
h : ∀ (n : I), AnalyticOn ℂ (f n) s
u : TendstoUniformlyOn f g atTop s
c : ℂ
hc : c ∈ s
r : ℝ
rp : 0 < r
cb : closedBall c r ⊆ s
⊢ AnalyticAt ℂ g c
Tactic:
lift r to ℝ≥0 using rp.le
State after:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
o : IsOpen s
h : ∀ (n : I), AnalyticOn ℂ (f n) s
u : TendstoUniformlyOn f g atTop s
c : ℂ
hc : c ∈ s
r : ℝ≥0
rp : 0 < ↑r
cb : closedBall c ↑r ⊆ s
⊢ AnalyticAt ℂ g c

State before:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
o : IsOpen s
h : ∀ (n : I), AnalyticOn ℂ (f n) s
u : TendstoUniformlyOn f g atTop s
c : ℂ
hc : c ∈ s
r : ℝ≥0
rp : 0 < ↑r
cb : closedBall c ↑r ⊆ s
⊢ AnalyticAt ℂ g c
Tactic:
simp only [NNReal.coe_pos] at rp
State after:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
o : IsOpen s
h : ∀ (n : I), AnalyticOn ℂ (f n) s
u : TendstoUniformlyOn f g atTop s
c : ℂ
hc : c ∈ s
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
⊢ AnalyticAt ℂ g c

State before:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
o : IsOpen s
h : ∀ (n : I), AnalyticOn ℂ (f n) s
u : TendstoUniformlyOn f g atTop s
c : ℂ
hc : c ∈ s
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
⊢ AnalyticAt ℂ g c
Tactic:
have hb : ∀ n, AnalyticOn ℂ (f n) (closedBall c r) := fun n ↦ (h n).mono cb
State after:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
o : IsOpen s
h : ∀ (n : I), AnalyticOn ℂ (f n) s
u : TendstoUniformlyOn f g atTop s
c : ℂ
hc : c ∈ s
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
hb : ∀ (n : I), AnalyticOn ℂ (f n) (closedBall c ↑r)
⊢ AnalyticAt ℂ g c

State before:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
o : IsOpen s
h : ∀ (n : I), AnalyticOn ℂ (f n) s
u : TendstoUniformlyOn f g atTop s
c : ℂ
hc : c ∈ s
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
hb : ∀ (n : I), AnalyticOn ℂ (f n) (closedBall c ↑r)
⊢ AnalyticAt ℂ g c
Tactic:
set pr := fun n ↦ cauchyPowerSeries (f n) c r
State after:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
o : IsOpen s
h : ∀ (n : I), AnalyticOn ℂ (f n) s
u : TendstoUniformlyOn f g atTop s
c : ℂ
hc : c ∈ s
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
hb : ∀ (n : I), AnalyticOn ℂ (f n) (closedBall c ↑r)
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
⊢ AnalyticAt ℂ g c

State before:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
o : IsOpen s
h : ∀ (n : I), AnalyticOn ℂ (f n) s
u : TendstoUniformlyOn f g atTop s
c : ℂ
hc : c ∈ s
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
hb : ∀ (n : I), AnalyticOn ℂ (f n) (closedBall c ↑r)
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
⊢ AnalyticAt ℂ g c
Tactic:
have hpf : ∀ n, HasFPowerSeriesOnBall (f n) (pr n) c r := by
  intro n
  have cs := cauchy_on_cball_radius rp (hb n)
  have pn : pr n = cauchyPowerSeries (f n) c r := rfl
  rw [← pn] at cs; exact cs
State after:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
o : IsOpen s
h : ∀ (n : I), AnalyticOn ℂ (f n) s
u : TendstoUniformlyOn f g atTop s
c : ℂ
hc : c ∈ s
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
hb : ∀ (n : I), AnalyticOn ℂ (f n) (closedBall c ↑r)
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
⊢ AnalyticAt ℂ g c

State before:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
o : IsOpen s
h : ∀ (n : I), AnalyticOn ℂ (f n) s
u : TendstoUniformlyOn f g atTop s
c : ℂ
hc : c ∈ s
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
hb : ∀ (n : I), AnalyticOn ℂ (f n) (closedBall c ↑r)
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
⊢ AnalyticAt ℂ g c
Tactic:
have cfs : ∀ n, ContinuousOn (f n) s := fun n ↦ AnalyticOn.continuousOn (h n)
State after:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
o : IsOpen s
h : ∀ (n : I), AnalyticOn ℂ (f n) s
u : TendstoUniformlyOn f g atTop s
c : ℂ
hc : c ∈ s
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
hb : ∀ (n : I), AnalyticOn ℂ (f n) (closedBall c ↑r)
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cfs : ∀ (n : I), ContinuousOn (f n) s
⊢ AnalyticAt ℂ g c

State before:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
o : IsOpen s
h : ∀ (n : I), AnalyticOn ℂ (f n) s
u : TendstoUniformlyOn f g atTop s
c : ℂ
hc : c ∈ s
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
hb : ∀ (n : I), AnalyticOn ℂ (f n) (closedBall c ↑r)
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cfs : ∀ (n : I), ContinuousOn (f n) s
⊢ AnalyticAt ℂ g c
Tactic:
have cf : ∀ n, ContinuousOn (f n) (closedBall c r) := fun n ↦ ContinuousOn.mono (cfs n) cb
State after:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
o : IsOpen s
h : ∀ (n : I), AnalyticOn ℂ (f n) s
u : TendstoUniformlyOn f g atTop s
c : ℂ
hc : c ∈ s
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
hb : ∀ (n : I), AnalyticOn ℂ (f n) (closedBall c ↑r)
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cfs : ∀ (n : I), ContinuousOn (f n) s
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
⊢ AnalyticAt ℂ g c

State before:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
o : IsOpen s
h : ∀ (n : I), AnalyticOn ℂ (f n) s
u : TendstoUniformlyOn f g atTop s
c : ℂ
hc : c ∈ s
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
hb : ∀ (n : I), AnalyticOn ℂ (f n) (closedBall c ↑r)
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cfs : ∀ (n : I), ContinuousOn (f n) s
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
⊢ AnalyticAt ℂ g c
Tactic:
have cg : ContinuousOn g (closedBall c r) :=
  ContinuousOn.mono (TendstoUniformlyOn.continuousOn u (Filter.eventually_of_forall cfs)) cb
State after:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
o : IsOpen s
h : ∀ (n : I), AnalyticOn ℂ (f n) s
u : TendstoUniformlyOn f g atTop s
c : ℂ
hc : c ∈ s
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
hb : ∀ (n : I), AnalyticOn ℂ (f n) (closedBall c ↑r)
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cfs : ∀ (n : I), ContinuousOn (f n) s
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
⊢ AnalyticAt ℂ g c

State before:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
o : IsOpen s
h : ∀ (n : I), AnalyticOn ℂ (f n) s
u : TendstoUniformlyOn f g atTop s
c : ℂ
hc : c ∈ s
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
hb : ∀ (n : I), AnalyticOn ℂ (f n) (closedBall c ↑r)
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cfs : ∀ (n : I), ContinuousOn (f n) s
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
⊢ AnalyticAt ℂ g c
Tactic:
clear h hb hc o cfs
State after:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
⊢ AnalyticAt ℂ g c

State before:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
⊢ AnalyticAt ℂ g c
Tactic:
set p := cauchyPowerSeries g c r
State after:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
⊢ AnalyticAt ℂ g c

State before:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
⊢ AnalyticAt ℂ g c
Tactic:
refine
  HasFPowerSeriesOnBall.analyticAt
    { r_le := le_radius_cauchyPowerSeries g c r
      r_pos := ENNReal.coe_pos.mpr rp
      hasSum := ?_ }
State after:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
⊢ ∀ {y : ℂ}, y ∈ EMetric.ball 0 ↑r → HasSum (fun n => (cauchyPowerSeries g c (↑r) n) fun x => y) (g (c + y))

State before:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
⊢ ∀ {y : ℂ}, y ∈ EMetric.ball 0 ↑r → HasSum (fun n => (cauchyPowerSeries g c (↑r) n) fun x => y) (g (c + y))
Tactic:
intro y yb
State after:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
⊢ HasSum (fun n => (cauchyPowerSeries g c (↑r) n) fun x => y) (g (c + y))

State before:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
⊢ HasSum (fun n => (cauchyPowerSeries g c (↑r) n) fun x => y) (g (c + y))
Tactic:
have yr := yb
State after:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb yr : y ∈ EMetric.ball 0 ↑r
⊢ HasSum (fun n => (cauchyPowerSeries g c (↑r) n) fun x => y) (g (c + y))

State before:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb yr : y ∈ EMetric.ball 0 ↑r
⊢ HasSum (fun n => (cauchyPowerSeries g c (↑r) n) fun x => y) (g (c + y))
Tactic:
simp at yr
State after:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
⊢ HasSum (fun n => (cauchyPowerSeries g c (↑r) n) fun x => y) (g (c + y))

State before:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
⊢ HasSum (fun n => (cauchyPowerSeries g c (↑r) n) fun x => y) (g (c + y))
Tactic:
set a := abs y / r
State after:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
⊢ HasSum (fun n => (cauchyPowerSeries g c (↑r) n) fun x => y) (g (c + y))

State before:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
⊢ HasSum (fun n => (cauchyPowerSeries g c (↑r) n) fun x => y) (g (c + y))
Tactic:
have a0 : a ≥ 0 := by bound
State after:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
⊢ HasSum (fun n => (cauchyPowerSeries g c (↑r) n) fun x => y) (g (c + y))

State before:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
⊢ HasSum (fun n => (cauchyPowerSeries g c (↑r) n) fun x => y) (g (c + y))
Tactic:
have a1 : a < 1 := (div_lt_one (NNReal.coe_pos.mpr rp)).mpr yr
State after:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
⊢ HasSum (fun n => (cauchyPowerSeries g c (↑r) n) fun x => y) (g (c + y))

State before:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
⊢ HasSum (fun n => (cauchyPowerSeries g c (↑r) n) fun x => y) (g (c + y))
Tactic:
have a1p : 1 - a > 0 := by bound
State after:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
⊢ HasSum (fun n => (cauchyPowerSeries g c (↑r) n) fun x => y) (g (c + y))

State before:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
⊢ HasSum (fun n => (cauchyPowerSeries g c (↑r) n) fun x => y) (g (c + y))
Tactic:
rw [HasSum, Metric.tendsto_atTop]
State after:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
⊢ ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (n.sum fun b => (cauchyPowerSeries g c (↑r) b) fun x => y) (g (c + y)) < ε

State before:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
⊢ ∀ ε > 0, ∃ N, ∀ n ≥ N, dist (n.sum fun b => (cauchyPowerSeries g c (↑r) b) fun x => y) (g (c + y)) < ε
Tactic:
intro e ep
State after:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
⊢ ∃ N, ∀ n ≥ N, dist (n.sum fun b => (cauchyPowerSeries g c (↑r) b) fun x => y) (g (c + y)) < e

State before:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
⊢ ∃ N, ∀ n ≥ N, dist (n.sum fun b => (cauchyPowerSeries g c (↑r) b) fun x => y) (g (c + y)) < e
Tactic:
generalize d4 : (1 - a) * (e / 4) = d
State after:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
⊢ ∃ N, ∀ n ≥ N, dist (n.sum fun b => (cauchyPowerSeries g c (↑r) b) fun x => y) (g (c + y)) < e

State before:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
⊢ ∃ N, ∀ n ≥ N, dist (n.sum fun b => (cauchyPowerSeries g c (↑r) b) fun x => y) (g (c + y)) < e
Tactic:
have dp : d > 0 := by rw [← d4]; bound
State after:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
⊢ ∃ N, ∀ n ≥ N, dist (n.sum fun b => (cauchyPowerSeries g c (↑r) b) fun x => y) (g (c + y)) < e

State before:
case intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
⊢ ∃ N, ∀ n ≥ N, dist (n.sum fun b => (cauchyPowerSeries g c (↑r) b) fun x => y) (g (c + y)) < e
Tactic:
rcases Filter.eventually_atTop.mp (Metric.tendstoUniformlyOn_iff.mp u d dp) with ⟨n, hn'⟩
State after:
case intro.intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn' : ∀ b ≥ n, ∀ x ∈ s, dist (g x) (f b x) < d
⊢ ∃ N, ∀ n ≥ N, dist (n.sum fun b => (cauchyPowerSeries g c (↑r) b) fun x => y) (g (c + y)) < e

State before:
case intro.intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn' : ∀ b ≥ n, ∀ x ∈ s, dist (g x) (f b x) < d
⊢ ∃ N, ∀ n ≥ N, dist (n.sum fun b => (cauchyPowerSeries g c (↑r) b) fun x => y) (g (c + y)) < e
Tactic:
set hn := hn' n
State after:
case intro.intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn' : ∀ b ≥ n, ∀ x ∈ s, dist (g x) (f b x) < d
hn : n ≥ n → ∀ x ∈ s, dist (g x) (f n x) < d := hn' n
⊢ ∃ N, ∀ n ≥ N, dist (n.sum fun b => (cauchyPowerSeries g c (↑r) b) fun x => y) (g (c + y)) < e

State before:
case intro.intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn' : ∀ b ≥ n, ∀ x ∈ s, dist (g x) (f b x) < d
hn : n ≥ n → ∀ x ∈ s, dist (g x) (f n x) < d := hn' n
⊢ ∃ N, ∀ n ≥ N, dist (n.sum fun b => (cauchyPowerSeries g c (↑r) b) fun x => y) (g (c + y)) < e
Tactic:
simp at hn
State after:
case intro.intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn' : ∀ b ≥ n, ∀ x ∈ s, dist (g x) (f b x) < d
hn : ∀ x ∈ s, dist (g x) (f n x) < d
⊢ ∃ N, ∀ n ≥ N, dist (n.sum fun b => (cauchyPowerSeries g c (↑r) b) fun x => y) (g (c + y)) < e

State before:
case intro.intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn' : ∀ b ≥ n, ∀ x ∈ s, dist (g x) (f b x) < d
hn : ∀ x ∈ s, dist (g x) (f n x) < d
⊢ ∃ N, ∀ n ≥ N, dist (n.sum fun b => (cauchyPowerSeries g c (↑r) b) fun x => y) (g (c + y)) < e
Tactic:
clear hn' u
State after:
case intro.intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
⊢ ∃ N, ∀ n ≥ N, dist (n.sum fun b => (cauchyPowerSeries g c (↑r) b) fun x => y) (g (c + y)) < e

State before:
case intro.intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
⊢ ∃ N, ∀ n ≥ N, dist (n.sum fun b => (cauchyPowerSeries g c (↑r) b) fun x => y) (g (c + y)) < e
Tactic:
have dfg : dist (f n (c + y)) (g (c + y)) ≤ d := by
  apply le_of_lt; rw [dist_comm]
  refine hn (c + y) ?_
  apply cb
  simp; exact yr.le
State after:
case intro.intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
⊢ ∃ N, ∀ n ≥ N, dist (n.sum fun b => (cauchyPowerSeries g c (↑r) b) fun x => y) (g (c + y)) < e

State before:
case intro.intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
⊢ ∃ N, ∀ n ≥ N, dist (n.sum fun b => (cauchyPowerSeries g c (↑r) b) fun x => y) (g (c + y)) < e
Tactic:
set hs := (hpf n).hasSum yb
State after:
case intro.intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
hs : HasSum (fun n_1 => (pr n n_1) fun x => y) (f n (c + y)) := (hpf n).hasSum yb
⊢ ∃ N, ∀ n ≥ N, dist (n.sum fun b => (cauchyPowerSeries g c (↑r) b) fun x => y) (g (c + y)) < e

State before:
case intro.intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
hs : HasSum (fun n_1 => (pr n n_1) fun x => y) (f n (c + y)) := (hpf n).hasSum yb
⊢ ∃ N, ∀ n ≥ N, dist (n.sum fun b => (cauchyPowerSeries g c (↑r) b) fun x => y) (g (c + y)) < e
Tactic:
rw [HasSum, Metric.tendsto_atTop] at hs
State after:
case intro.intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
hs : ∀ ε > 0, ∃ N, ∀ n_1 ≥ N, dist (n_1.sum fun b => (pr n b) fun x => y) (f n (c + y)) < ε
⊢ ∃ N, ∀ n ≥ N, dist (n.sum fun b => (cauchyPowerSeries g c (↑r) b) fun x => y) (g (c + y)) < e

State before:
case intro.intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
hs : ∀ ε > 0, ∃ N, ∀ n_1 ≥ N, dist (n_1.sum fun b => (pr n b) fun x => y) (f n (c + y)) < ε
⊢ ∃ N, ∀ n ≥ N, dist (n.sum fun b => (cauchyPowerSeries g c (↑r) b) fun x => y) (g (c + y)) < e
Tactic:
rcases hs d dp with ⟨N, NM⟩
State after:
case intro.intro.intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
hs : ∀ ε > 0, ∃ N, ∀ n_1 ≥ N, dist (n_1.sum fun b => (pr n b) fun x => y) (f n (c + y)) < ε
N : Finset ℕ
NM : ∀ n_1 ≥ N, dist (n_1.sum fun b => (pr n b) fun x => y) (f n (c + y)) < d
⊢ ∃ N, ∀ n ≥ N, dist (n.sum fun b => (cauchyPowerSeries g c (↑r) b) fun x => y) (g (c + y)) < e

State before:
case intro.intro.intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
hs : ∀ ε > 0, ∃ N, ∀ n_1 ≥ N, dist (n_1.sum fun b => (pr n b) fun x => y) (f n (c + y)) < ε
N : Finset ℕ
NM : ∀ n_1 ≥ N, dist (n_1.sum fun b => (pr n b) fun x => y) (f n (c + y)) < d
⊢ ∃ N, ∀ n ≥ N, dist (n.sum fun b => (cauchyPowerSeries g c (↑r) b) fun x => y) (g (c + y)) < e
Tactic:
clear hs
State after:
case intro.intro.intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
N : Finset ℕ
NM : ∀ n_1 ≥ N, dist (n_1.sum fun b => (pr n b) fun x => y) (f n (c + y)) < d
⊢ ∃ N, ∀ n ≥ N, dist (n.sum fun b => (cauchyPowerSeries g c (↑r) b) fun x => y) (g (c + y)) < e

State before:
case intro.intro.intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
N : Finset ℕ
NM : ∀ n_1 ≥ N, dist (n_1.sum fun b => (pr n b) fun x => y) (f n (c + y)) < d
⊢ ∃ N, ∀ n ≥ N, dist (n.sum fun b => (cauchyPowerSeries g c (↑r) b) fun x => y) (g (c + y)) < e
Tactic:
exists N
State after:
case intro.intro.intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
N : Finset ℕ
NM : ∀ n_1 ≥ N, dist (n_1.sum fun b => (pr n b) fun x => y) (f n (c + y)) < d
⊢ ∀ n ≥ N, dist (n.sum fun b => (cauchyPowerSeries g c (↑r) b) fun x => y) (g (c + y)) < e

State before:
case intro.intro.intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
N : Finset ℕ
NM : ∀ n_1 ≥ N, dist (n_1.sum fun b => (pr n b) fun x => y) (f n (c + y)) < d
⊢ ∀ n ≥ N, dist (n.sum fun b => (cauchyPowerSeries g c (↑r) b) fun x => y) (g (c + y)) < e
Tactic:
intro M NlM
State after:
case intro.intro.intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
N : Finset ℕ
NM : ∀ n_1 ≥ N, dist (n_1.sum fun b => (pr n b) fun x => y) (f n (c + y)) < d
M : Finset ℕ
NlM : M ≥ N
⊢ dist (M.sum fun b => (cauchyPowerSeries g c (↑r) b) fun x => y) (g (c + y)) < e

State before:
case intro.intro.intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
N : Finset ℕ
NM : ∀ n_1 ≥ N, dist (n_1.sum fun b => (pr n b) fun x => y) (f n (c + y)) < d
M : Finset ℕ
NlM : M ≥ N
⊢ dist (M.sum fun b => (cauchyPowerSeries g c (↑r) b) fun x => y) (g (c + y)) < e
Tactic:
have dpf := (NM M NlM).le
State after:
case intro.intro.intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
N : Finset ℕ
NM : ∀ n_1 ≥ N, dist (n_1.sum fun b => (pr n b) fun x => y) (f n (c + y)) < d
M : Finset ℕ
NlM : M ≥ N
dpf : dist (M.sum fun b => (pr n b) fun x => y) (f n (c + y)) ≤ d
⊢ dist (M.sum fun b => (cauchyPowerSeries g c (↑r) b) fun x => y) (g (c + y)) < e

State before:
case intro.intro.intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
N : Finset ℕ
NM : ∀ n_1 ≥ N, dist (n_1.sum fun b => (pr n b) fun x => y) (f n (c + y)) < d
M : Finset ℕ
NlM : M ≥ N
dpf : dist (M.sum fun b => (pr n b) fun x => y) (f n (c + y)) ≤ d
⊢ dist (M.sum fun b => (cauchyPowerSeries g c (↑r) b) fun x => y) (g (c + y)) < e
Tactic:
clear NM NlM N yb
State after:
case intro.intro.intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
M : Finset ℕ
dpf : dist (M.sum fun b => (pr n b) fun x => y) (f n (c + y)) ≤ d
⊢ dist (M.sum fun b => (cauchyPowerSeries g c (↑r) b) fun x => y) (g (c + y)) < e

State before:
case intro.intro.intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
M : Finset ℕ
dpf : dist (M.sum fun b => (pr n b) fun x => y) (f n (c + y)) ≤ d
dppr : dist (M.sum fun k => (p k) fun x => y) (M.sum fun k => (pr n k) fun x => y) ≤ e / 4
⊢ dist (M.sum fun b => (cauchyPowerSeries g c (↑r) b) fun x => y) (g (c + y)) < e
Tactic:
generalize hMp : M.sum (fun k : ℕ ↦ p k fun _ ↦ y) = Mp
State after:
case intro.intro.intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
M : Finset ℕ
dpf : dist (M.sum fun b => (pr n b) fun x => y) (f n (c + y)) ≤ d
dppr : dist (M.sum fun k => (p k) fun x => y) (M.sum fun k => (pr n k) fun x => y) ≤ e / 4
Mp : ℂ
hMp : (M.sum fun k => (p k) fun x => y) = Mp
⊢ dist Mp (g (c + y)) < e

State before:
case intro.intro.intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
M : Finset ℕ
dpf : dist (M.sum fun b => (pr n b) fun x => y) (f n (c + y)) ≤ d
dppr : dist (M.sum fun k => (p k) fun x => y) (M.sum fun k => (pr n k) fun x => y) ≤ e / 4
Mp : ℂ
hMp : (M.sum fun k => (p k) fun x => y) = Mp
⊢ dist Mp (g (c + y)) < e
Tactic:
rw [hMp] at dppr
State after:
case intro.intro.intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
M : Finset ℕ
dpf : dist (M.sum fun b => (pr n b) fun x => y) (f n (c + y)) ≤ d
Mp : ℂ
dppr : dist Mp (M.sum fun k => (pr n k) fun x => y) ≤ e / 4
hMp : (M.sum fun k => (p k) fun x => y) = Mp
⊢ dist Mp (g (c + y)) < e

State before:
case intro.intro.intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
M : Finset ℕ
dpf : dist (M.sum fun b => (pr n b) fun x => y) (f n (c + y)) ≤ d
Mp : ℂ
dppr : dist Mp (M.sum fun k => (pr n k) fun x => y) ≤ e / 4
hMp : (M.sum fun k => (p k) fun x => y) = Mp
⊢ dist Mp (g (c + y)) < e
Tactic:
generalize hMpr : M.sum (fun k ↦ pr n k fun _ ↦ y) = Mpr
State after:
case intro.intro.intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
M : Finset ℕ
dpf : dist (M.sum fun b => (pr n b) fun x => y) (f n (c + y)) ≤ d
Mp : ℂ
dppr : dist Mp (M.sum fun k => (pr n k) fun x => y) ≤ e / 4
hMp : (M.sum fun k => (p k) fun x => y) = Mp
Mpr : ℂ
hMpr : (M.sum fun k => (pr n k) fun x => y) = Mpr
⊢ dist Mp (g (c + y)) < e

State before:
case intro.intro.intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
M : Finset ℕ
dpf : dist (M.sum fun b => (pr n b) fun x => y) (f n (c + y)) ≤ d
Mp : ℂ
dppr : dist Mp (M.sum fun k => (pr n k) fun x => y) ≤ e / 4
hMp : (M.sum fun k => (p k) fun x => y) = Mp
Mpr : ℂ
hMpr : (M.sum fun k => (pr n k) fun x => y) = Mpr
⊢ dist Mp (g (c + y)) < e
Tactic:
rw [hMpr] at dpf dppr
State after:
case intro.intro.intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
M : Finset ℕ
Mp : ℂ
hMp : (M.sum fun k => (p k) fun x => y) = Mp
Mpr : ℂ
dppr : dist Mp Mpr ≤ e / 4
dpf : dist Mpr (f n (c + y)) ≤ d
hMpr : (M.sum fun k => (pr n k) fun x => y) = Mpr
⊢ dist Mp (g (c + y)) < e

State before:
case intro.intro.intro.intro.intro
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
M : Finset ℕ
Mp : ℂ
hMp : (M.sum fun k => (p k) fun x => y) = Mp
Mpr : ℂ
dppr : dist Mp Mpr ≤ e / 4
dpf : dist Mpr (f n (c + y)) ≤ d
hMpr : (M.sum fun k => (pr n k) fun x => y) = Mpr
⊢ dist Mp (g (c + y)) < e
Tactic:
calc dist Mp (g (c + y))
  _ ≤ dist Mp (f n (c + y)) + dist (f n (c + y)) (g (c + y)) := dist_triangle _ _ _
  _ ≤ dist Mp Mpr + dist Mpr (f n (c + y)) + d := by bound
  _ ≤ e / 4 + d + d := by bound
  _ = e / 4 + 2 * (1 - a) * (e / 4) := by rw [← d4]; ring
  _ ≤ e / 4 + 2 * (1 - 0) * (e / 4) := by bound
  _ = 3 / 4 * e := by ring
  _ < 1 * e := (mul_lt_mul_of_pos_right (by norm_num) ep)
  _ = e := by simp
State after:
no goals

State before:
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
o : IsOpen s
h : ∀ (n : I), AnalyticOn ℂ (f n) s
u : TendstoUniformlyOn f g atTop s
c : ℂ
hc : c ∈ s
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
hb : ∀ (n : I), AnalyticOn ℂ (f n) (closedBall c ↑r)
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
⊢ ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
Tactic:
intro n
State after:
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
o : IsOpen s
h : ∀ (n : I), AnalyticOn ℂ (f n) s
u : TendstoUniformlyOn f g atTop s
c : ℂ
hc : c ∈ s
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
hb : ∀ (n : I), AnalyticOn ℂ (f n) (closedBall c ↑r)
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
n : I
⊢ HasFPowerSeriesOnBall (f n) (pr n) c ↑r

State before:
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
o : IsOpen s
h : ∀ (n : I), AnalyticOn ℂ (f n) s
u : TendstoUniformlyOn f g atTop s
c : ℂ
hc : c ∈ s
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
hb : ∀ (n : I), AnalyticOn ℂ (f n) (closedBall c ↑r)
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
n : I
⊢ HasFPowerSeriesOnBall (f n) (pr n) c ↑r
Tactic:
have cs := cauchy_on_cball_radius rp (hb n)
State after:
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
o : IsOpen s
h : ∀ (n : I), AnalyticOn ℂ (f n) s
u : TendstoUniformlyOn f g atTop s
c : ℂ
hc : c ∈ s
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
hb : ∀ (n : I), AnalyticOn ℂ (f n) (closedBall c ↑r)
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
n : I
cs : HasFPowerSeriesOnBall (f n) (cauchyPowerSeries (f n) c ↑r) c ↑r
⊢ HasFPowerSeriesOnBall (f n) (pr n) c ↑r

State before:
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
o : IsOpen s
h : ∀ (n : I), AnalyticOn ℂ (f n) s
u : TendstoUniformlyOn f g atTop s
c : ℂ
hc : c ∈ s
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
hb : ∀ (n : I), AnalyticOn ℂ (f n) (closedBall c ↑r)
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
n : I
cs : HasFPowerSeriesOnBall (f n) (cauchyPowerSeries (f n) c ↑r) c ↑r
⊢ HasFPowerSeriesOnBall (f n) (pr n) c ↑r
Tactic:
have pn : pr n = cauchyPowerSeries (f n) c r := rfl
State after:
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
o : IsOpen s
h : ∀ (n : I), AnalyticOn ℂ (f n) s
u : TendstoUniformlyOn f g atTop s
c : ℂ
hc : c ∈ s
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
hb : ∀ (n : I), AnalyticOn ℂ (f n) (closedBall c ↑r)
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
n : I
cs : HasFPowerSeriesOnBall (f n) (cauchyPowerSeries (f n) c ↑r) c ↑r
pn : pr n = cauchyPowerSeries (f n) c ↑r
⊢ HasFPowerSeriesOnBall (f n) (pr n) c ↑r

State before:
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
o : IsOpen s
h : ∀ (n : I), AnalyticOn ℂ (f n) s
u : TendstoUniformlyOn f g atTop s
c : ℂ
hc : c ∈ s
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
hb : ∀ (n : I), AnalyticOn ℂ (f n) (closedBall c ↑r)
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
n : I
cs : HasFPowerSeriesOnBall (f n) (cauchyPowerSeries (f n) c ↑r) c ↑r
pn : pr n = cauchyPowerSeries (f n) c ↑r
⊢ HasFPowerSeriesOnBall (f n) (pr n) c ↑r
Tactic:
rw [← pn] at cs
State after:
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
o : IsOpen s
h : ∀ (n : I), AnalyticOn ℂ (f n) s
u : TendstoUniformlyOn f g atTop s
c : ℂ
hc : c ∈ s
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
hb : ∀ (n : I), AnalyticOn ℂ (f n) (closedBall c ↑r)
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
n : I
cs : HasFPowerSeriesOnBall (f n) (pr n) c ↑r
pn : pr n = cauchyPowerSeries (f n) c ↑r
⊢ HasFPowerSeriesOnBall (f n) (pr n) c ↑r

State before:
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
o : IsOpen s
h : ∀ (n : I), AnalyticOn ℂ (f n) s
u : TendstoUniformlyOn f g atTop s
c : ℂ
hc : c ∈ s
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
hb : ∀ (n : I), AnalyticOn ℂ (f n) (closedBall c ↑r)
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
n : I
cs : HasFPowerSeriesOnBall (f n) (pr n) c ↑r
pn : pr n = cauchyPowerSeries (f n) c ↑r
⊢ HasFPowerSeriesOnBall (f n) (pr n) c ↑r
Tactic:
exact cs
State after:
no goals

State before:
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
⊢ a ≥ 0
Tactic:
bound
State after:
no goals

State before:
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
⊢ 1 - a > 0
Tactic:
bound
State after:
no goals

State before:
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
⊢ d > 0
Tactic:
rw [← d4]
State after:
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
⊢ (1 - a) * (e / 4) > 0

State before:
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
u : TendstoUniformlyOn f g atTop s
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
⊢ (1 - a) * (e / 4) > 0
Tactic:
bound
State after:
no goals

State before:
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
⊢ dist (f n (c + y)) (g (c + y)) ≤ d
Tactic:
apply le_of_lt
State after:
case a
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
⊢ dist (f n (c + y)) (g (c + y)) < d

State before:
case a
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
⊢ dist (f n (c + y)) (g (c + y)) < d
Tactic:
rw [dist_comm]
State after:
case a
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
⊢ dist (g (c + y)) (f n (c + y)) < d

State before:
case a
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
⊢ dist (g (c + y)) (f n (c + y)) < d
Tactic:
refine hn (c + y) ?_
State after:
case a
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
⊢ c + y ∈ s

State before:
case a
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
⊢ c + y ∈ s
Tactic:
apply cb
State after:
case a.a
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
⊢ c + y ∈ closedBall c ↑r

State before:
case a.a
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
⊢ c + y ∈ closedBall c ↑r
Tactic:
simp
State after:
case a.a
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
⊢ Complex.abs y ≤ ↑r

State before:
case a.a
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yb : y ∈ EMetric.ball 0 ↑r
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
⊢ Complex.abs y ≤ ↑r
Tactic:
exact yr.le
State after:
no goals

State before:
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
M : Finset ℕ
dpf : dist (M.sum fun b => (pr n b) fun x => y) (f n (c + y)) ≤ d
⊢ dist (M.sum fun k => (p k) fun x => y) (M.sum fun k => (pr n k) fun x => y) ≤ e / 4
Tactic:
trans M.sum fun k : ℕ ↦ dist (p k fun _ ↦ y) (pr n k fun _ ↦ y)
State after:
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
M : Finset ℕ
dpf : dist (M.sum fun b => (pr n b) fun x => y) (f n (c + y)) ≤ d
⊢ dist (M.sum fun k => (p k) fun x => y) (M.sum fun k => (pr n k) fun x => y) ≤
    M.sum fun k => dist ((p k) fun x => y) ((pr n k) fun x => y)

I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
M : Finset ℕ
dpf : dist (M.sum fun b => (pr n b) fun x => y) (f n (c + y)) ≤ d
⊢ (M.sum fun k => dist ((p k) fun x => y) ((pr n k) fun x => y)) ≤ e / 4

State before:
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
M : Finset ℕ
dpf : dist (M.sum fun b => (pr n b) fun x => y) (f n (c + y)) ≤ d
⊢ dist (M.sum fun k => (p k) fun x => y) (M.sum fun k => (pr n k) fun x => y) ≤
    M.sum fun k => dist ((p k) fun x => y) ((pr n k) fun x => y)

I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
M : Finset ℕ
dpf : dist (M.sum fun b => (pr n b) fun x => y) (f n (c + y)) ≤ d
⊢ (M.sum fun k => dist ((p k) fun x => y) ((pr n k) fun x => y)) ≤ e / 4
Tactic:
apply dist_sum_sum_le M (fun k : ℕ ↦ p k fun _ ↦ y) fun k : ℕ ↦ pr n k fun _ ↦ y
State after:
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
M : Finset ℕ
dpf : dist (M.sum fun b => (pr n b) fun x => y) (f n (c + y)) ≤ d
⊢ (M.sum fun k => dist ((p k) fun x => y) ((pr n k) fun x => y)) ≤ e / 4

State before:
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
M : Finset ℕ
dpf : dist (M.sum fun b => (pr n b) fun x => y) (f n (c + y)) ≤ d
⊢ (M.sum fun k => dist ((p k) fun x => y) ((pr n k) fun x => y)) ≤ e / 4
Tactic:
trans M.sum fun k ↦ a ^ k * d
State after:
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
M : Finset ℕ
dpf : dist (M.sum fun b => (pr n b) fun x => y) (f n (c + y)) ≤ d
⊢ (M.sum fun k => dist ((p k) fun x => y) ((pr n k) fun x => y)) ≤ M.sum fun k => a ^ k * d

I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
M : Finset ℕ
dpf : dist (M.sum fun b => (pr n b) fun x => y) (f n (c + y)) ≤ d
⊢ (M.sum fun k => a ^ k * d) ≤ e / 4

State before:
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
M : Finset ℕ
dpf : dist (M.sum fun b => (pr n b) fun x => y) (f n (c + y)) ≤ d
⊢ (M.sum fun k => dist ((p k) fun x => y) ((pr n k) fun x => y)) ≤ M.sum fun k => a ^ k * d
Tactic:
apply Finset.sum_le_sum
State after:
case h
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
M : Finset ℕ
dpf : dist (M.sum fun b => (pr n b) fun x => y) (f n (c + y)) ≤ d
⊢ ∀ i ∈ M, dist ((p i) fun x => y) ((pr n i) fun x => y) ≤ a ^ i * d

State before:
case h
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
M : Finset ℕ
dpf : dist (M.sum fun b => (pr n b) fun x => y) (f n (c + y)) ≤ d
⊢ ∀ i ∈ M, dist ((p i) fun x => y) ((pr n i) fun x => y) ≤ a ^ i * d
Tactic:
intro k _
State after:
case h
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
M : Finset ℕ
dpf : dist (M.sum fun b => (pr n b) fun x => y) (f n (c + y)) ≤ d
k : ℕ
a✝ : k ∈ M
⊢ dist ((p k) fun x => y) ((pr n k) fun x => y) ≤ a ^ k * d

State before:
case h
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
M : Finset ℕ
dpf : dist (M.sum fun b => (pr n b) fun x => y) (f n (c + y)) ≤ d
k : ℕ
a✝ : k ∈ M
⊢ dist ((p k) fun x => y) ((pr n k) fun x => y) ≤ a ^ k * d
Tactic:
have hak : a ^ k = abs y ^ k * r⁻¹ ^ k := by
  calc (abs y / r) ^ k
    _ = (abs y * r⁻¹) ^ k := by rw [div_eq_mul_inv, NNReal.coe_inv]
    _ = abs y ^ k * r⁻¹ ^ k := mul_pow _ _ _
State after:
case h
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
M : Finset ℕ
dpf : dist (M.sum fun b => (pr n b) fun x => y) (f n (c + y)) ≤ d
k : ℕ
a✝ : k ∈ M
hak : a ^ k = Complex.abs y ^ k * ↑r⁻¹ ^ k
⊢ dist ((p k) fun x => y) ((pr n k) fun x => y) ≤ a ^ k * d

State before:
case h
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
M : Finset ℕ
dpf : dist (M.sum fun b => (pr n b) fun x => y) (f n (c + y)) ≤ d
k : ℕ
a✝ : k ∈ M
hak : a ^ k = Complex.abs y ^ k * ↑r⁻¹ ^ k
⊢ dist ((p k) fun x => y) ((pr n k) fun x => y) ≤ a ^ k * d
Tactic:
rw [hak]
State after:
case h
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
M : Finset ℕ
dpf : dist (M.sum fun b => (pr n b) fun x => y) (f n (c + y)) ≤ d
k : ℕ
a✝ : k ∈ M
hak : a ^ k = Complex.abs y ^ k * ↑r⁻¹ ^ k
⊢ dist ((p k) fun x => y) ((pr n k) fun x => y) ≤ Complex.abs y ^ k * ↑r⁻¹ ^ k * d

State before:
case h
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
M : Finset ℕ
dpf : dist (M.sum fun b => (pr n b) fun x => y) (f n (c + y)) ≤ d
k : ℕ
a✝ : k ∈ M
hak : a ^ k = Complex.abs y ^ k * ↑r⁻¹ ^ k
⊢ dist ((p k) fun x => y) ((pr n k) fun x => y) ≤ Complex.abs y ^ k * ↑r⁻¹ ^ k * d
Tactic:
generalize hd' : d.toNNReal = d'
State after:
case h
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
M : Finset ℕ
dpf : dist (M.sum fun b => (pr n b) fun x => y) (f n (c + y)) ≤ d
k : ℕ
a✝ : k ∈ M
hak : a ^ k = Complex.abs y ^ k * ↑r⁻¹ ^ k
d' : ℝ≥0
hd' : d.toNNReal = d'
⊢ dist ((p k) fun x => y) ((pr n k) fun x => y) ≤ Complex.abs y ^ k * ↑r⁻¹ ^ k * d

State before:
case h
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
M : Finset ℕ
dpf : dist (M.sum fun b => (pr n b) fun x => y) (f n (c + y)) ≤ d
k : ℕ
a✝ : k ∈ M
hak : a ^ k = Complex.abs y ^ k * ↑r⁻¹ ^ k
d' : ℝ≥0
hd' : d.toNNReal = d'
⊢ dist ((p k) fun x => y) ((pr n k) fun x => y) ≤ Complex.abs y ^ k * ↑r⁻¹ ^ k * d
Tactic:
have dd : (d' : ℝ) = d := by rw [← hd']; exact Real.coe_toNNReal d dp.le
State after:
case h
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
M : Finset ℕ
dpf : dist (M.sum fun b => (pr n b) fun x => y) (f n (c + y)) ≤ d
k : ℕ
a✝ : k ∈ M
hak : a ^ k = Complex.abs y ^ k * ↑r⁻¹ ^ k
d' : ℝ≥0
hd' : d.toNNReal = d'
dd : ↑d' = d
⊢ dist ((p k) fun x => y) ((pr n k) fun x => y) ≤ Complex.abs y ^ k * ↑r⁻¹ ^ k * d

State before:
case h
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
M : Finset ℕ
dpf : dist (M.sum fun b => (pr n b) fun x => y) (f n (c + y)) ≤ d
k : ℕ
a✝ : k ∈ M
hak : a ^ k = Complex.abs y ^ k * ↑r⁻¹ ^ k
d' : ℝ≥0
hd' : d.toNNReal = d'
dd : ↑d' = d
⊢ dist ((p k) fun x => y) ((pr n k) fun x => y) ≤ Complex.abs y ^ k * ↑r⁻¹ ^ k * d
Tactic:
have hcb : ∀ z, z ∈ closedBall c r → abs (g z - f n z) ≤ d' := by
  intro z zb; exact _root_.trans (hn z (cb zb)).le (le_of_eq dd.symm)
State after:
case h
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
M : Finset ℕ
dpf : dist (M.sum fun b => (pr n b) fun x => y) (f n (c + y)) ≤ d
k : ℕ
a✝ : k ∈ M
hak : a ^ k = Complex.abs y ^ k * ↑r⁻¹ ^ k
d' : ℝ≥0
hd' : d.toNNReal = d'
dd : ↑d' = d
hcb : ∀ z ∈ closedBall c ↑r, Complex.abs (g z - f n z) ≤ ↑d'
⊢ dist ((p k) fun x => y) ((pr n k) fun x => y) ≤ Complex.abs y ^ k * ↑r⁻¹ ^ k * d

State before:
case h
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
M : Finset ℕ
dpf : dist (M.sum fun b => (pr n b) fun x => y) (f n (c + y)) ≤ d
k : ℕ
a✝ : k ∈ M
hak : a ^ k = Complex.abs y ^ k * ↑r⁻¹ ^ k
d' : ℝ≥0
hd' : d.toNNReal = d'
dd : ↑d' = d
hcb : ∀ z ∈ closedBall c ↑r, Complex.abs (g z - f n z) ≤ ↑d'
⊢ dist ((p k) fun x => y) ((pr n k) fun x => y) ≤ Complex.abs y ^ k * ↑r⁻¹ ^ k * d
Tactic:
exact _root_.trans (cauchy_dist k y rp cg (cf n) hcb)
  (mul_le_mul_of_nonneg_left (le_of_eq dd) (by bound))
State after:
no goals

State before:
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
M : Finset ℕ
dpf : dist (M.sum fun b => (pr n b) fun x => y) (f n (c + y)) ≤ d
k : ℕ
a✝ : k ∈ M
⊢ a ^ k = Complex.abs y ^ k * ↑r⁻¹ ^ k
Tactic:
calc (abs y / r) ^ k
  _ = (abs y * r⁻¹) ^ k := by rw [div_eq_mul_inv, NNReal.coe_inv]
  _ = abs y ^ k * r⁻¹ ^ k := mul_pow _ _ _
State after:
no goals

State before:
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
M : Finset ℕ
dpf : dist (M.sum fun b => (pr n b) fun x => y) (f n (c + y)) ≤ d
k : ℕ
a✝ : k ∈ M
⊢ (Complex.abs y / ↑r) ^ k = (Complex.abs y * ↑r⁻¹) ^ k
Tactic:
rw [div_eq_mul_inv, NNReal.coe_inv]
State after:
no goals

State before:
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
M : Finset ℕ
dpf : dist (M.sum fun b => (pr n b) fun x => y) (f n (c + y)) ≤ d
k : ℕ
a✝ : k ∈ M
hak : a ^ k = Complex.abs y ^ k * ↑r⁻¹ ^ k
d' : ℝ≥0
hd' : d.toNNReal = d'
⊢ ↑d' = d
Tactic:
rw [← hd']
State after:
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
M : Finset ℕ
dpf : dist (M.sum fun b => (pr n b) fun x => y) (f n (c + y)) ≤ d
k : ℕ
a✝ : k ∈ M
hak : a ^ k = Complex.abs y ^ k * ↑r⁻¹ ^ k
d' : ℝ≥0
hd' : d.toNNReal = d'
⊢ ↑d.toNNReal = d

State before:
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
M : Finset ℕ
dpf : dist (M.sum fun b => (pr n b) fun x => y) (f n (c + y)) ≤ d
k : ℕ
a✝ : k ∈ M
hak : a ^ k = Complex.abs y ^ k * ↑r⁻¹ ^ k
d' : ℝ≥0
hd' : d.toNNReal = d'
⊢ ↑d.toNNReal = d
Tactic:
exact Real.coe_toNNReal d dp.le
State after:
no goals

State before:
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
M : Finset ℕ
dpf : dist (M.sum fun b => (pr n b) fun x => y) (f n (c + y)) ≤ d
k : ℕ
a✝ : k ∈ M
hak : a ^ k = Complex.abs y ^ k * ↑r⁻¹ ^ k
d' : ℝ≥0
hd' : d.toNNReal = d'
dd : ↑d' = d
⊢ ∀ z ∈ closedBall c ↑r, Complex.abs (g z - f n z) ≤ ↑d'
Tactic:
intro z zb
State after:
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
M : Finset ℕ
dpf : dist (M.sum fun b => (pr n b) fun x => y) (f n (c + y)) ≤ d
k : ℕ
a✝ : k ∈ M
hak : a ^ k = Complex.abs y ^ k * ↑r⁻¹ ^ k
d' : ℝ≥0
hd' : d.toNNReal = d'
dd : ↑d' = d
z : ℂ
zb : z ∈ closedBall c ↑r
⊢ Complex.abs (g z - f n z) ≤ ↑d'

State before:
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
M : Finset ℕ
dpf : dist (M.sum fun b => (pr n b) fun x => y) (f n (c + y)) ≤ d
k : ℕ
a✝ : k ∈ M
hak : a ^ k = Complex.abs y ^ k * ↑r⁻¹ ^ k
d' : ℝ≥0
hd' : d.toNNReal = d'
dd : ↑d' = d
z : ℂ
zb : z ∈ closedBall c ↑r
⊢ Complex.abs (g z - f n z) ≤ ↑d'
Tactic:
exact _root_.trans (hn z (cb zb)).le (le_of_eq dd.symm)
State after:
no goals

State before:
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
M : Finset ℕ
dpf : dist (M.sum fun b => (pr n b) fun x => y) (f n (c + y)) ≤ d
k : ℕ
a✝ : k ∈ M
hak : a ^ k = Complex.abs y ^ k * ↑r⁻¹ ^ k
d' : ℝ≥0
hd' : d.toNNReal = d'
dd : ↑d' = d
hcb : ∀ z ∈ closedBall c ↑r, Complex.abs (g z - f n z) ≤ ↑d'
⊢ 0 ≤ Complex.abs y ^ k * ↑r⁻¹ ^ k
Tactic:
bound
State after:
no goals

State before:
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
M : Finset ℕ
dpf : dist (M.sum fun b => (pr n b) fun x => y) (f n (c + y)) ≤ d
⊢ (M.sum fun k => a ^ k * d) ≤ e / 4
Tactic:
have pgb : (M.sum fun k ↦ a ^ k) ≤ (1 - a)⁻¹ := partial_geometric_bound M a0 a1
State after:
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
M : Finset ℕ
dpf : dist (M.sum fun b => (pr n b) fun x => y) (f n (c + y)) ≤ d
pgb : (M.sum fun k => a ^ k) ≤ (1 - a)⁻¹
⊢ (M.sum fun k => a ^ k * d) ≤ e / 4

State before:
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
M : Finset ℕ
dpf : dist (M.sum fun b => (pr n b) fun x => y) (f n (c + y)) ≤ d
pgb : (M.sum fun k => a ^ k) ≤ (1 - a)⁻¹
⊢ (M.sum fun k => a ^ k * d) ≤ e / 4
Tactic:
calc
  (M.sum fun k ↦ a ^ k * d) = (M.sum fun k ↦ a ^ k) * d := by rw [← Finset.sum_mul]
  _ ≤ (1 - a)⁻¹ * d := by bound
  _ = (1 - a)⁻¹ * ((1 - a) * (e / 4)) := by rw [← d4]
  _ = (1 - a) * (1 - a)⁻¹ * (e / 4) := by ring
  _ = 1 * (e / 4) := by rw [mul_inv_cancel a1p.ne']
  _ = e / 4 := by ring
State after:
no goals

State before:
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
M : Finset ℕ
dpf : dist (M.sum fun b => (pr n b) fun x => y) (f n (c + y)) ≤ d
pgb : (M.sum fun k => a ^ k) ≤ (1 - a)⁻¹
⊢ (M.sum fun k => a ^ k * d) = (M.sum fun k => a ^ k) * d
Tactic:
rw [← Finset.sum_mul]
State after:
no goals

State before:
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
M : Finset ℕ
dpf : dist (M.sum fun b => (pr n b) fun x => y) (f n (c + y)) ≤ d
pgb : (M.sum fun k => a ^ k) ≤ (1 - a)⁻¹
⊢ (M.sum fun k => a ^ k) * d ≤ (1 - a)⁻¹ * d
Tactic:
bound
State after:
no goals

State before:
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
M : Finset ℕ
dpf : dist (M.sum fun b => (pr n b) fun x => y) (f n (c + y)) ≤ d
pgb : (M.sum fun k => a ^ k) ≤ (1 - a)⁻¹
⊢ (1 - a)⁻¹ * d = (1 - a)⁻¹ * ((1 - a) * (e / 4))
Tactic:
rw [← d4]
State after:
no goals

State before:
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
M : Finset ℕ
dpf : dist (M.sum fun b => (pr n b) fun x => y) (f n (c + y)) ≤ d
pgb : (M.sum fun k => a ^ k) ≤ (1 - a)⁻¹
⊢ (1 - a)⁻¹ * ((1 - a) * (e / 4)) = (1 - a) * (1 - a)⁻¹ * (e / 4)
Tactic:
ring
State after:
no goals

State before:
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
M : Finset ℕ
dpf : dist (M.sum fun b => (pr n b) fun x => y) (f n (c + y)) ≤ d
pgb : (M.sum fun k => a ^ k) ≤ (1 - a)⁻¹
⊢ (1 - a) * (1 - a)⁻¹ * (e / 4) = 1 * (e / 4)
Tactic:
rw [mul_inv_cancel a1p.ne']
State after:
no goals

State before:
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
M : Finset ℕ
dpf : dist (M.sum fun b => (pr n b) fun x => y) (f n (c + y)) ≤ d
pgb : (M.sum fun k => a ^ k) ≤ (1 - a)⁻¹
⊢ 1 * (e / 4) = e / 4
Tactic:
ring
State after:
no goals

State before:
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
M : Finset ℕ
Mp : ℂ
hMp : (M.sum fun k => (p k) fun x => y) = Mp
Mpr : ℂ
dppr : dist Mp Mpr ≤ e / 4
dpf : dist Mpr (f n (c + y)) ≤ d
hMpr : (M.sum fun k => (pr n k) fun x => y) = Mpr
⊢ dist Mp (f n (c + y)) + dist (f n (c + y)) (g (c + y)) ≤ dist Mp Mpr + dist Mpr (f n (c + y)) + d
Tactic:
bound
State after:
no goals

State before:
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
M : Finset ℕ
Mp : ℂ
hMp : (M.sum fun k => (p k) fun x => y) = Mp
Mpr : ℂ
dppr : dist Mp Mpr ≤ e / 4
dpf : dist Mpr (f n (c + y)) ≤ d
hMpr : (M.sum fun k => (pr n k) fun x => y) = Mpr
⊢ dist Mp Mpr + dist Mpr (f n (c + y)) + d ≤ e / 4 + d + d
Tactic:
bound
State after:
no goals

State before:
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
M : Finset ℕ
Mp : ℂ
hMp : (M.sum fun k => (p k) fun x => y) = Mp
Mpr : ℂ
dppr : dist Mp Mpr ≤ e / 4
dpf : dist Mpr (f n (c + y)) ≤ d
hMpr : (M.sum fun k => (pr n k) fun x => y) = Mpr
⊢ e / 4 + d + d = e / 4 + 2 * (1 - a) * (e / 4)
Tactic:
rw [← d4]
State after:
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
M : Finset ℕ
Mp : ℂ
hMp : (M.sum fun k => (p k) fun x => y) = Mp
Mpr : ℂ
dppr : dist Mp Mpr ≤ e / 4
dpf : dist Mpr (f n (c + y)) ≤ d
hMpr : (M.sum fun k => (pr n k) fun x => y) = Mpr
⊢ e / 4 + (1 - a) * (e / 4) + (1 - a) * (e / 4) = e / 4 + 2 * (1 - a) * (e / 4)

State before:
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
M : Finset ℕ
Mp : ℂ
hMp : (M.sum fun k => (p k) fun x => y) = Mp
Mpr : ℂ
dppr : dist Mp Mpr ≤ e / 4
dpf : dist Mpr (f n (c + y)) ≤ d
hMpr : (M.sum fun k => (pr n k) fun x => y) = Mpr
⊢ e / 4 + (1 - a) * (e / 4) + (1 - a) * (e / 4) = e / 4 + 2 * (1 - a) * (e / 4)
Tactic:
ring
State after:
no goals

State before:
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
M : Finset ℕ
Mp : ℂ
hMp : (M.sum fun k => (p k) fun x => y) = Mp
Mpr : ℂ
dppr : dist Mp Mpr ≤ e / 4
dpf : dist Mpr (f n (c + y)) ≤ d
hMpr : (M.sum fun k => (pr n k) fun x => y) = Mpr
⊢ e / 4 + 2 * (1 - a) * (e / 4) ≤ e / 4 + 2 * (1 - 0) * (e / 4)
Tactic:
bound
State after:
no goals

State before:
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
M : Finset ℕ
Mp : ℂ
hMp : (M.sum fun k => (p k) fun x => y) = Mp
Mpr : ℂ
dppr : dist Mp Mpr ≤ e / 4
dpf : dist Mpr (f n (c + y)) ≤ d
hMpr : (M.sum fun k => (pr n k) fun x => y) = Mpr
⊢ e / 4 + 2 * (1 - 0) * (e / 4) = 3 / 4 * e
Tactic:
ring
State after:
no goals

State before:
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
M : Finset ℕ
Mp : ℂ
hMp : (M.sum fun k => (p k) fun x => y) = Mp
Mpr : ℂ
dppr : dist Mp Mpr ≤ e / 4
dpf : dist Mpr (f n (c + y)) ≤ d
hMpr : (M.sum fun k => (pr n k) fun x => y) = Mpr
⊢ 3 / 4 < 1
Tactic:
norm_num
State after:
no goals

State before:
I : Type
inst✝¹ : Lattice I
inst✝ : Nonempty I
f : I → ℂ → ℂ
g : ℂ → ℂ
s : Set ℂ
c : ℂ
r : ℝ≥0
cb : closedBall c ↑r ⊆ s
rp : 0 < r
pr : I → FormalMultilinearSeries ℂ ℂ ℂ := fun n => cauchyPowerSeries (f n) c ↑r
hpf : ∀ (n : I), HasFPowerSeriesOnBall (f n) (pr n) c ↑r
cf : ∀ (n : I), ContinuousOn (f n) (closedBall c ↑r)
cg : ContinuousOn g (closedBall c ↑r)
p : FormalMultilinearSeries ℂ ℂ ℂ := cauchyPowerSeries g c ↑r
y : ℂ
yr : Complex.abs y < ↑r
a : ℝ := Complex.abs y / ↑r
a0 : a ≥ 0
a1 : a < 1
a1p : 1 - a > 0
e : ℝ
ep : e > 0
d : ℝ
d4 : (1 - a) * (e / 4) = d
dp : d > 0
n : I
hn : ∀ x ∈ s, dist (g x) (f n x) < d
dfg : dist (f n (c + y)) (g (c + y)) ≤ d
M : Finset ℕ
Mp : ℂ
hMp : (M.sum fun k => (p k) fun x => y) = Mp
Mpr : ℂ
dppr : dist Mp Mpr ≤ e / 4
dpf : dist Mpr (f n (c + y)) ≤ d
hMpr : (M.sum fun k => (pr n k) fun x => y) = Mpr
⊢ 1 * e = e
Tactic:
simp
State after:
no goals