awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Analytic.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
⊢ insert x s ∩ Metric.eball x r ∈ 𝓝[insert x s] x

Tactic:
inter_mem_nhdsWithin _ (Metric.eball_mem_nhds x hf.r_pos)

Premises used: inter_mem_nhdsWithin, Metric.eball_mem_nhds, HasFPowerSeriesWithinOnBall.r_pos
-- Module: Mathlib.Analysis.Analytic.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
⊢ insert x s ∩ Metric.eball x r ∈ 𝓝[insert x s] x

Tactic:
exact inter_mem_nhdsWithin _ (Metric.eball_mem_nhds x hf.r_pos)

Premises used: inter_mem_nhdsWithin, Metric.eball_mem_nhds, HasFPowerSeriesWithinOnBall.r_pos
-- Module: Mathlib.Analysis.Analytic.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
⊢ ContinuousWithinAt f s x

Tactic:
hf.continuousWithinAt_insert.mono (subset_insert x s)

Premises used: ContinuousWithinAt.mono, HasFPowerSeriesWithinOnBall.continuousWithinAt_insert, Set.subset_insert
-- Module: Mathlib.Analysis.Analytic.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
hf : HasFPowerSeriesWithinAt f p s x
rcases : ∀ (r : ℝ≥0∞) (hr : HasFPowerSeriesWithinOnBall f p s x r), ContinuousWithinAt f (insert x s) x
⊢ ContinuousWithinAt f (insert x s) x

Tactic:
rcases hf with ⟨r, hr⟩
-- Module: Mathlib.Analysis.Analytic.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hr : HasFPowerSeriesWithinOnBall f p s x r
⊢ ContinuousWithinAt f (insert x s) x

Tactic:
apply hr.continuousWithinAt_insert

Premises used: HasFPowerSeriesWithinOnBall.continuousWithinAt_insert
-- Module: Mathlib.Analysis.Analytic.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
hf : HasFPowerSeriesWithinAt f p s x
⊢ ContinuousWithinAt f s x

Tactic:
hf.continuousWithinAt_insert.mono (subset_insert x s)

Premises used: HasFPowerSeriesWithinAt.continuousWithinAt_insert, ContinuousWithinAt.mono, Set.subset_insert
-- Module: Mathlib.Analysis.Analytic.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
hf : HasFPowerSeriesAt f p x
⊢ ContinuousAt f x

Tactic:
let ⟨_, hr⟩ := hf
  hr.continuousOn.continuousAt (Metric.eball_mem_nhds x hr.r_pos)

Premises used: ContinuousAt, Metric.eball_mem_nhds, _private.0.HasFPowerSeriesAt.radius_pos.match_1, HasFPowerSeriesOnBall.continuousOn, ContinuousOn.continuousAt, HasFPowerSeriesOnBall.r_pos
-- Module: Mathlib.Analysis.Analytic.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
x : E
hf : AnalyticWithinAt 𝕜 f s x
⊢ ContinuousWithinAt f (insert x s) x

Tactic:
let ⟨_, hp⟩ := hf
  hp.continuousWithinAt_insert

Premises used: ContinuousWithinAt, Insert.insert, HasFPowerSeriesWithinAt.continuousWithinAt_insert, _private.0.AnalyticWithinAt.continuousWithinAt_insert.match_1
-- Module: Mathlib.Analysis.Analytic.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
x : E
hf : AnalyticWithinAt 𝕜 f s x
⊢ ContinuousWithinAt f s x

Tactic:
hf.continuousWithinAt_insert.mono (subset_insert x s)

Premises used: AnalyticWithinAt.continuousWithinAt_insert, ContinuousWithinAt.mono, Set.subset_insert
-- Module: Mathlib.Analysis.Analytic.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
hf : AnalyticAt 𝕜 f x
⊢ ContinuousAt f x

Tactic:
let ⟨_, hp⟩ := hf
  hp.continuousAt

Premises used: ContinuousAt, _private.0.AnalyticAt.congr.match_1, HasFPowerSeriesAt.continuousAt
-- Module: Mathlib.Analysis.Analytic.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
hf : AnalyticAt 𝕜 f x
rcases :
  ∀ (g : FormalMultilinearSeries 𝕜 E F) (r : ℝ≥0∞) (hg : HasFPowerSeriesOnBall f g x r),
    ∀ᶠ (y : E) in 𝓝 x, ContinuousAt f y
⊢ ∀ᶠ (y : E) in 𝓝 x, ContinuousAt f y

Tactic:
rcases hf with ⟨g, r, hg⟩
-- Module: Mathlib.Analysis.Analytic.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
g : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
hg : HasFPowerSeriesOnBall f g x r
⊢ Metric.eball x r ∈ 𝓝 x

Tactic:
have : Metric.eball x r ∈ 𝓝 x := Metric.eball_mem_nhds _ hg.r_pos
-- Module: Mathlib.Analysis.Analytic.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
g : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
hg : HasFPowerSeriesOnBall f g x r
this : Metric.eball x r ∈ 𝓝 x
h : ∀ (y : E) (hy : y ∈ Metric.eball x r), ContinuousAt f y
⊢ ∀ᶠ (y : E) in 𝓝 x, ContinuousAt f y

Tactic:
filter_upwards [this] with y hy
-- Module: Mathlib.Analysis.Analytic.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
g : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
hg : HasFPowerSeriesOnBall f g x r
this : Metric.eball x r ∈ 𝓝 x
y : E
hy : y ∈ Metric.eball x r
h : Metric.eball x r ∈ 𝓝 y
⊢ ContinuousAt f y

Tactic:
apply hg.continuousOn.continuousAt

Premises used: HasFPowerSeriesOnBall.continuousOn, ContinuousOn.continuousAt
-- Module: Mathlib.Analysis.Analytic.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
g : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
hg : HasFPowerSeriesOnBall f g x r
this : Metric.eball x r ∈ 𝓝 x
y : E
hy : y ∈ Metric.eball x r
⊢ Metric.eball x r ∈ 𝓝 y

Tactic:
Metric.isOpen_eball.mem_nhds hy

Premises used: Metric.isOpen_eball, Set.Mem, IsOpen.mem_nhds
-- Module: Mathlib.Analysis.Analytic.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
g : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
hg : HasFPowerSeriesOnBall f g x r
this : Metric.eball x r ∈ 𝓝 x
y : E
hy : y ∈ Metric.eball x r
⊢ Metric.eball x r ∈ 𝓝 y

Tactic:
exact Metric.isOpen_eball.mem_nhds hy

Premises used: Metric.isOpen_eball, IsOpen.mem_nhds
-- Module: Mathlib.Analysis.Analytic.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
hf : AnalyticOnNhd 𝕜 f s
⊢ ContinuousOn f s

Tactic:
fun x hx => (hf x hx).continuousAt.continuousWithinAt

Premises used: ContinuousAt.continuousWithinAt, ContinuousOn, AnalyticAt.continuousAt
-- Module: Mathlib.Analysis.Analytic.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
h : AnalyticOn 𝕜 f s
⊢ ContinuousOn f s

Tactic:
fun x m ↦ (h x m).continuousWithinAt

Premises used: AnalyticWithinAt.continuousWithinAt, ContinuousOn
-- Module: Mathlib.Analysis.Analytic.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
fa : AnalyticOnNhd 𝕜 f univ
rw : ContinuousOn f univ
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f

Tactic:
rw [← continuousOn_univ]

Premises used: continuousOn_univ
-- Module: Mathlib.Analysis.Analytic.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
fa : AnalyticOnNhd 𝕜 f univ
⊢ ContinuousOn f univ

Tactic:
fa.continuousOn

Premises used: AnalyticOnNhd.continuousOn
-- Module: Mathlib.Analysis.Analytic.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
fa : AnalyticOnNhd 𝕜 f univ
⊢ ContinuousOn f univ

Tactic:
exact fa.continuousOn

Premises used: AnalyticOnNhd.continuousOn
-- Module: Mathlib.Analysis.Analytic.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
p : FormalMultilinearSeries 𝕜 E F
h : 0 < p.radius
y : E
hy : Membership.mem (γ := Set E) (Metric.eball 0 p.radius) y
rw : HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y) (p.sum y)
⊢ HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y) (p.sum (0 + y))

Tactic:
rw [zero_add]

Premises used: zero_add
-- Module: Mathlib.Analysis.Analytic.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
p : FormalMultilinearSeries 𝕜 E F
h : 0 < p.radius
y : E
hy : Membership.mem (γ := Set E) (Metric.eball 0 p.radius) y
⊢ HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y) (p.sum y)

Tactic:
p.hasSum hy

Premises used: FormalMultilinearSeries.hasSum
-- Module: Mathlib.Analysis.Analytic.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
p : FormalMultilinearSeries 𝕜 E F
h : 0 < p.radius
y : E
hy : Membership.mem (γ := Set E) (Metric.eball 0 p.radius) y
⊢ HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y) (p.sum y)

Tactic:
exact p.hasSum hy

Premises used: FormalMultilinearSeries.hasSum
-- Module: Mathlib.Analysis.Analytic.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
h'y : x + y ∈ insert x s
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
⊢ f (x + y) = p.sum y

Tactic:
(h.hasSum h'y hy).tsum_eq.symm

Premises used: HasSum.tsum_eq, HasFPowerSeriesWithinOnBall.hasSum, Eq.symm, FormalMultilinearSeries.sum
-- Module: Mathlib.Analysis.Analytic.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
h : HasFPowerSeriesOnBall f p x r
y : E
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
⊢ f (x + y) = p.sum y

Tactic:
(h.hasSum hy).tsum_eq.symm

Premises used: HasFPowerSeriesOnBall.hasSum, HasSum.tsum_eq, Eq.symm, FormalMultilinearSeries.sum
-- Module: Mathlib.Analysis.Analytic.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
inst_5 : CompleteSpace F
inl : ∀ (h : p.radius = 0), ContinuousOn p.sum (Metric.eball 0 p.radius)
inr : ∀ (h : 0 < p.radius), ContinuousOn p.sum (Metric.eball 0 p.radius)
⊢ ContinuousOn p.sum (Metric.eball 0 p.radius)

Tactic:
rcases eq_zero_or_pos p.radius with h | h

Premises used: FormalMultilinearSeries.radius, eq_zero_or_pos
-- Module: Mathlib.Analysis.Analytic.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
inst_5 : CompleteSpace F
h : p.radius = 0
⊢ ContinuousOn p.sum (Metric.eball 0 p.radius)

Tactic:
simp [h, continuousOn_empty]

Premises used: continuousOn_empty
-- Module: Mathlib.Analysis.Analytic.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
inst_5 : CompleteSpace F
h : 0 < p.radius
⊢ ContinuousOn p.sum (Metric.eball 0 p.radius)

Tactic:
(p.hasFPowerSeriesOnBall h).continuousOn

Premises used: HasFPowerSeriesOnBall.continuousOn, FormalMultilinearSeries.hasFPowerSeriesOnBall
-- Module: Mathlib.Analysis.Analytic.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
inst_5 : CompleteSpace F
h : 0 < p.radius
⊢ ContinuousOn p.sum (Metric.eball 0 p.radius)

Tactic:
exact (p.hasFPowerSeriesOnBall h).continuousOn

Premises used: HasFPowerSeriesOnBall.continuousOn, FormalMultilinearSeries.hasFPowerSeriesOnBall
-- Module: Mathlib.Analysis.Analytic.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
h_1 : HasFPowerSeriesAt (𝕜 := 𝕜) f p z₀
r : ℝ≥0∞
r_le : r ≤ radius.{u_1, u_1, u_2} (𝕜 := 𝕜) (E := 𝕜) (F := E) p
r_pos : 0 < r
h :
  ∀ {y : 𝕜},
    Membership.mem (γ := Set 𝕜) (Metric.eball 0 r) y →
      HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → 𝕜) → E) fun (x : Fin n) ↦ y) (f (z₀ + y))
x : 𝕜
⊢ Membership.mem (γ := Set 𝕜) (Metric.eball 0 r) x → HasSum (fun (n : ℕ) ↦ x ^ n • p.coeff n) (f (z₀ + x))

Tactic:
simpa using h
-- Module: Mathlib.Analysis.Analytic.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
refine : (∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun (n : ℕ) ↦ z ^ n • p.coeff n) (f (z₀ + z))) → HasFPowerSeriesAt (𝕜 := 𝕜) f p z₀
⊢ HasFPowerSeriesAt (𝕜 := 𝕜) f p z₀ ↔ ∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun (n : ℕ) ↦ z ^ n • p.coeff n) (f (z₀ + z))

Tactic:
refine ⟨fun ⟨r, _, r_pos, h⟩ =>
    eventually_of_mem (Metric.eball_mem_nhds 0 r_pos) fun _ => by simpa using h, ?_⟩
-- Module: Mathlib.Analysis.Analytic.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
simp :
  (∃ ε > 0, ∀ ⦃y : 𝕜⦄, dist y 0 < ε → HasSum (fun (n : ℕ) ↦ y ^ n • p.coeff n) (f (z₀ + y))) →
    HasFPowerSeriesAt (𝕜 := 𝕜) f p z₀
⊢ (∀ᶠ (z : 𝕜) in 𝓝 0, HasSum (fun (n : ℕ) ↦ z ^ n • p.coeff n) (f (z₀ + z))) → HasFPowerSeriesAt (𝕜 := 𝕜) f p z₀

Tactic:
simp only [Metric.eventually_nhds_iff]

Premises used: Metric.eventually_nhds_iff
-- Module: Mathlib.Analysis.Analytic.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
r : ℝ
r_pos : r > 0
h : ∀ ⦃y : 𝕜⦄, dist y 0 < r → HasSum (fun (n : ℕ) ↦ y ^ n • p.coeff n) (f (z₀ + y))
⊢ min (radius.{u_1, u_1, u_2} (𝕜 := 𝕜) (E := 𝕜) (F := E) p) (↑r.toNNReal : ℝ≥0∞) ≤
    radius.{u_1, u_1, u_2} (𝕜 := 𝕜) (E := 𝕜) (F := E) p

Tactic:
simp
-- Module: Mathlib.Analysis.Analytic.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
r : ℝ
r_pos : r > 0
h : ∀ ⦃y : 𝕜⦄, dist y 0 < r → HasSum (fun (n : ℕ) ↦ y ^ n • p.coeff n) (f (z₀ + y))
refine_1 : 0 < min (radius.{u_1, u_1, u_2} (𝕜 := 𝕜) (E := 𝕜) (F := E) p) (↑r.toNNReal : ℝ≥0∞)
refine_2 :
  ∀ {y : 𝕜},
    Membership.mem (γ := Set 𝕜)
        (Metric.eball 0 (min (radius.{u_1, u_1, u_2} (𝕜 := 𝕜) (E := 𝕜) (F := E) p) (↑r.toNNReal : ℝ≥0∞))) y →
      HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → 𝕜) → E) fun (x : Fin n) ↦ y) (f (z₀ + y))
⊢ HasFPowerSeriesAt (𝕜 := 𝕜) f p z₀

Tactic:
refine ⟨p.radius ⊓ r.toNNReal, by simp, ?_, ?_⟩
-- Module: Mathlib.Analysis.Analytic.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
r : ℝ
r_pos : r > 0
h : ∀ ⦃y : 𝕜⦄, dist y 0 < r → HasSum (fun (n : ℕ) ↦ y ^ n • p.coeff n) (f (z₀ + y))
refine_1 : 0 < radius.{u_1, u_1, u_2} (𝕜 := 𝕜) (E := 𝕜) (F := E) p
⊢ 0 < min (radius.{u_1, u_1, u_2} (𝕜 := 𝕜) (E := 𝕜) (F := E) p) (↑r.toNNReal : ℝ≥0∞)

Tactic:
simp only [r_pos.lt, lt_inf_iff, ENNReal.coe_pos, Real.toNNReal_pos, and_true]

Premises used: and_true, lt_inf_iff, GT.gt.lt, Real.toNNReal_pos, ENNReal.coe_pos
-- Module: Mathlib.Analysis.Analytic.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
r : ℝ
r_pos : r > 0
h : ∀ ⦃y : 𝕜⦄, dist y 0 < r → HasSum (fun (n : ℕ) ↦ y ^ n • p.coeff n) (f (z₀ + y))
refine_1 : ∀ (z : 𝕜) (z_pos : 0 < ‖z‖) (le_z : ‖z‖ < r), 0 < radius.{u_1, u_1, u_2} (𝕜 := 𝕜) (E := 𝕜) (F := E) p
⊢ 0 < radius.{u_1, u_1, u_2} (𝕜 := 𝕜) (E := 𝕜) (F := E) p

Tactic:
obtain ⟨z, z_pos, le_z⟩ := NormedField.exists_norm_lt 𝕜 r_pos.lt

Premises used: GT.gt.lt, NormedField.exists_norm_lt
-- Module: Mathlib.Analysis.Analytic.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
r : ℝ
r_pos : r > 0
h : ∀ ⦃y : 𝕜⦄, dist y 0 < r → HasSum (fun (n : ℕ) ↦ y ^ n • p.coeff n) (f (z₀ + y))
z : 𝕜
z_pos : 0 < ‖z‖
le_z : ‖z‖ < r
⊢ ∀ ⦃y : 𝕜⦄, ‖y‖ < r → HasSum (fun (n : ℕ) ↦ y ^ n • p.coeff n) (f (z₀ + y))

Tactic:
simp only [dist_zero_right] at h

Premises used: dist_zero_right
-- Module: Mathlib.Analysis.Analytic.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
r : ℝ
r_pos : r > 0
z : 𝕜
z_pos : 0 < ‖z‖
le_z : ‖z‖ < r
h : ∀ ⦃y : 𝕜⦄, ‖y‖ < r → HasSum (fun (n : ℕ) ↦ y ^ n • p.coeff n) (f (z₀ + y))
h₁ : Tendsto (fun (n : ℕ) ↦ ‖p n‖ * (↑‖z‖₊ : ℝ) ^ n) atTop (𝓝 (norm.{u_2} (E := E) 0))
l : ℝ
⊢ (↑‖z‖₊ : ℝ≥0∞) ≤ radius.{u_1, u_1, u_2} (𝕜 := 𝕜) (E := 𝕜) (F := E) p

Tactic:
apply FormalMultilinearSeries.le_radius_of_tendsto

Premises used: FormalMultilinearSeries.le_radius_of_tendsto
-- Module: Mathlib.Analysis.Analytic.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
r : ℝ
r_pos : r > 0
z : 𝕜
z_pos : 0 < ‖z‖
le_z : ‖z‖ < r
h : ∀ ⦃y : 𝕜⦄, ‖y‖ < r → HasSum (fun (n : ℕ) ↦ y ^ n • p.coeff n) (f (z₀ + y))
⊢ Tendsto (α := ℕ) ((fun (a : E) ↦ ‖a‖) ∘ fun (n : ℕ) ↦ z ^ n • p.coeff n) atTop (𝓝 (norm.{u_2} (E := E) 0))

Tactic:
tendsto_norm.comp (h le_z).summable.tendsto_atTop_zero

Premises used: Summable.tendsto_atTop_zero, HasSum.summable, tendsto_norm, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.Analytic.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
r : ℝ
r_pos : r > 0
z : 𝕜
z_pos : 0 < ‖z‖
le_z : ‖z‖ < r
h : ∀ ⦃y : 𝕜⦄, ‖y‖ < r → HasSum (fun (n : ℕ) ↦ y ^ n • p.coeff n) (f (z₀ + y))
x : ℕ
⊢ ‖p x‖ * (↑‖z‖₊ : ℝ) ^ x = ((fun (a : E) ↦ ‖a‖) ∘ fun (n : ℕ) ↦ z ^ n • p.coeff n) x

Tactic:
simp [norm_smul, mul_comm]

Premises used: norm_smul, mul_comm
-- Module: Mathlib.Analysis.Analytic.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
r : ℝ
r_pos : r > 0
h : ∀ ⦃y : 𝕜⦄, dist y 0 < r → HasSum (fun (n : ℕ) ↦ y ^ n • p.coeff n) (f (z₀ + y))
z : 𝕜
z_pos : 0 < ‖z‖
le_z : ‖z‖ < r
⊢ (↑‖z‖₊ : ℝ≥0∞) ≤ radius.{u_1, u_1, u_2} (𝕜 := 𝕜) (E := 𝕜) (F := E) p

Tactic:
have : (‖z‖₊ : ENNReal) ≤ p.radius := by
      simp only [dist_zero_right] at h
      apply FormalMultilinearSeries.le_radius_of_tendsto
      convert! tendsto_norm.comp (h le_z).summable.tendsto_atTop_zero
      simp [norm_smul, mul_comm]
-- Module: Mathlib.Analysis.Analytic.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
r : ℝ
r_pos : r > 0
h : ∀ ⦃y : 𝕜⦄, dist y 0 < r → HasSum (fun (n : ℕ) ↦ y ^ n • p.coeff n) (f (z₀ + y))
z : 𝕜
z_pos : 0 < ‖z‖
le_z : ‖z‖ < r
this : (↑‖z‖₊ : ℝ≥0∞) ≤ radius.{u_1, u_1, u_2} (𝕜 := 𝕜) (E := 𝕜) (F := E) p
⊢ 0 < radius.{u_1, u_1, u_2} (𝕜 := 𝕜) (E := 𝕜) (F := E) p

Tactic:
lt_of_lt_of_le ?_ this

Premises used: lt_of_lt_of_le
-- Module: Mathlib.Analysis.Analytic.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
r : ℝ
r_pos : r > 0
h : ∀ ⦃y : 𝕜⦄, dist y 0 < r → HasSum (fun (n : ℕ) ↦ y ^ n • p.coeff n) (f (z₀ + y))
z : 𝕜
z_pos : 0 < ‖z‖
le_z : ‖z‖ < r
this : (↑‖z‖₊ : ℝ≥0∞) ≤ radius.{u_1, u_1, u_2} (𝕜 := 𝕜) (E := 𝕜) (F := E) p
refine_1 : 0 < (↑‖z‖₊ : ℝ≥0∞)
⊢ 0 < radius.{u_1, u_1, u_2} (𝕜 := 𝕜) (E := 𝕜) (F := E) p

Tactic:
refine lt_of_lt_of_le ?_ this

Premises used: lt_of_lt_of_le
-- Module: Mathlib.Analysis.Analytic.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
p : FormalMultilinearSeries 𝕜 𝕜 E
f : 𝕜 → E
z₀ : 𝕜
r : ℝ
r_pos : r > 0
h : ∀ ⦃y : 𝕜⦄, dist y 0 < r → HasSum (fun (n : ℕ) ↦ y ^ n • p.coeff n) (f (z₀ + y))
z : 𝕜
z_pos : 0 < ‖z‖
le_z : ‖z‖ < r
this : (↑‖z‖₊ : ℝ≥0∞) ≤ radius.{u_1, u_1, u_2} (𝕜 := 𝕜) (E := 𝕜) (F := E) p
refine_1 : 0 < ‖z‖₊
⊢ 0 < (↑‖z‖₊ : ℝ≥0∞)

Tactic:
simp only [ENNReal.coe_pos]

Premises used: ENNReal.coe_pos