awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Analytic.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F
s : Set E
g : F →L[𝕜] G
h : AnalyticOn 𝕜 f s
x : E
hx : x ∈ s
rcases :
  ∀ (p : FormalMultilinearSeries 𝕜 E F) (r : ℝ≥0∞) (hp : HasFPowerSeriesWithinOnBall f p s x r),
    AnalyticWithinAt.{u_1, u_2, u_4} 𝕜 (F := G) ((⇑g : (a : F) → G) ∘ f) s x
⊢ AnalyticWithinAt.{u_1, u_2, u_4} 𝕜 (F := G) ((⇑g : (a : F) → G) ∘ f) s x

Tactic:
rcases h x hx with ⟨p, r, hp⟩
-- Module: Mathlib.Analysis.Analytic.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F
s : Set E
g : F →L[𝕜] G
h : AnalyticOn 𝕜 f s
x : E
hx : x ∈ s
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
hp : HasFPowerSeriesWithinOnBall f p s x r
⊢ AnalyticWithinAt.{u_1, u_2, u_4} 𝕜 (F := G) ((⇑g : (a : F) → G) ∘ f) s x

Tactic:
⟨g.compFormalMultilinearSeries p, r, g.comp_hasFPowerSeriesWithinOnBall hp⟩

Premises used: AnalyticWithinAt, ContinuousLinearMap.comp_hasFPowerSeriesWithinOnBall, Exists.intro, ContinuousLinearMap.compFormalMultilinearSeries
-- Module: Mathlib.Analysis.Analytic.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F
s : Set E
g : F →L[𝕜] G
h : AnalyticOn 𝕜 f s
x : E
hx : x ∈ s
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
hp : HasFPowerSeriesWithinOnBall f p s x r
⊢ AnalyticWithinAt.{u_1, u_2, u_4} 𝕜 (F := G) ((⇑g : (a : F) → G) ∘ f) s x

Tactic:
exact ⟨g.compFormalMultilinearSeries p, r, g.comp_hasFPowerSeriesWithinOnBall hp⟩
-- Module: Mathlib.Analysis.Analytic.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F
s : Set E
g : F →L[𝕜] G
h : AnalyticOnNhd 𝕜 f s
x : E
hx : x ∈ s
rcases :
  ∀ (p : FormalMultilinearSeries 𝕜 E F) (r : ℝ≥0∞) (hp : HasFPowerSeriesOnBall f p x r),
    AnalyticAt.{u_1, u_2, u_4} 𝕜 (F := G) ((⇑g : (a : F) → G) ∘ f) x
⊢ AnalyticAt.{u_1, u_2, u_4} 𝕜 (F := G) ((⇑g : (a : F) → G) ∘ f) x

Tactic:
rcases h x hx with ⟨p, r, hp⟩
-- Module: Mathlib.Analysis.Analytic.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F
s : Set E
g : F →L[𝕜] G
h : AnalyticOnNhd 𝕜 f s
x : E
hx : x ∈ s
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p x r
⊢ AnalyticAt.{u_1, u_2, u_4} 𝕜 (F := G) ((⇑g : (a : F) → G) ∘ f) x

Tactic:
⟨g.compFormalMultilinearSeries p, r, g.comp_hasFPowerSeriesOnBall hp⟩

Premises used: AnalyticAt, Exists.intro, ContinuousLinearMap.comp_hasFPowerSeriesOnBall, ContinuousLinearMap.compFormalMultilinearSeries
-- Module: Mathlib.Analysis.Analytic.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F
s : Set E
g : F →L[𝕜] G
h : AnalyticOnNhd 𝕜 f s
x : E
hx : x ∈ s
p : FormalMultilinearSeries 𝕜 E F
r : ℝ≥0∞
hp : HasFPowerSeriesOnBall f p x r
⊢ AnalyticAt.{u_1, u_2, u_4} 𝕜 (F := G) ((⇑g : (a : F) → G) ∘ f) x

Tactic:
exact ⟨g.compFormalMultilinearSeries p, r, g.comp_hasFPowerSeriesOnBall hp⟩
-- 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
y : E
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
h'y : x + y ∈ insert x s
⊢ Tendsto (fun (n : ℕ) ↦ p.partialSum n y) atTop (𝓝 (f (x + y)))

Tactic:
(hf.hasSum h'y hy).tendsto_sum_nat

Premises used: HasSum.tendsto_sum_nat, FormalMultilinearSeries.partialSum, HasFPowerSeriesWithinOnBall.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
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
y : E
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
⊢ Tendsto (fun (n : ℕ) ↦ p.partialSum n y) atTop (𝓝 (f (x + y)))

Tactic:
(hf.hasSum hy).tendsto_sum_nat

Premises used: HasSum.tendsto_sum_nat, FormalMultilinearSeries.partialSum, HasFPowerSeriesOnBall.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
x : E
hf : HasFPowerSeriesAt f p x
rcases :
  ∀ (r : ℝ≥0∞) (hr : HasFPowerSeriesOnBall f p x r),
    ∀ᶠ (y : E) in 𝓝 0, Tendsto (fun (n : ℕ) ↦ p.partialSum n y) atTop (𝓝 (f (x + y)))
⊢ ∀ᶠ (y : E) in 𝓝 0, Tendsto (fun (n : ℕ) ↦ p.partialSum n y) atTop (𝓝 (f (x + y)))

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
x : E
r : ℝ≥0∞
hr : HasFPowerSeriesOnBall f p x r
h :
  ∀ (y : E) (hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y),
    Tendsto (fun (n : ℕ) ↦ p.partialSum n y) atTop (𝓝 (f (x + y)))
⊢ ∀ᶠ (y : E) in 𝓝 0, Tendsto (fun (n : ℕ) ↦ p.partialSum n y) atTop (𝓝 (f (x + y)))

Tactic:
filter_upwards [Metric.eball_mem_nhds (0 : E) hr.r_pos] with y hy

Premises used: Metric.eball_mem_nhds, OfNat.ofNat, 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
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hr : HasFPowerSeriesOnBall f p x r
y : E
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
⊢ Tendsto (fun (n : ℕ) ↦ p.partialSum n y) atTop (𝓝 (f (x + y)))

Tactic:
hr.tendsto_partialSum hy

Premises used: HasFPowerSeriesOnBall.tendsto_partialSum
-- 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∞
hr : HasFPowerSeriesOnBall f p x r
y : E
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
⊢ Tendsto (fun (n : ℕ) ↦ p.partialSum n y) atTop (𝓝 (f (x + y)))

Tactic:
exact hr.tendsto_partialSum hy

Premises used: HasFPowerSeriesOnBall.tendsto_partialSum
-- 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∞
y : E
hf : HasFPowerSeriesWithinOnBall f p s x r
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
h'y : x + y ∈ insert x s
⊢ Tendsto (fun (z : ℕ × E) ↦ p.partialSum z.1 y) (SProd.sprod (α := Filter ℕ) atTop (𝓝 y)) (𝓝 (f (x + y)))

Tactic:
apply (hf.tendsto_partialSum hy h'y).comp tendsto_fst

Premises used: Filter.Tendsto.comp, HasFPowerSeriesWithinOnBall.tendsto_partialSum, Filter.tendsto_fst
-- 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∞
y : E
hf : HasFPowerSeriesWithinOnBall f p s x r
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
h'y : x + y ∈ insert x s
⊢ Tendsto (fun (z : ℕ × E) ↦ p.partialSum z.1 y) (SProd.sprod (α := Filter ℕ) atTop (𝓝 y)) (𝓝 (f (x + y)))

Tactic:
have A : Tendsto (fun (z : ℕ × E) ↦ p.partialSum z.1 y) (atTop ×ˢ 𝓝 y) (𝓝 (f (x + y))) := by
    apply (hf.tendsto_partialSum hy h'y).comp tendsto_fst
-- 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∞
y : E
hf : HasFPowerSeriesWithinOnBall f p s x r
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
h'y : x + y ∈ insert x s
A : Tendsto (fun (z : ℕ × E) ↦ p.partialSum z.1 y) (SProd.sprod (α := Filter ℕ) atTop (𝓝 y)) (𝓝 (f (x + y)))
this :
  Tendsto.{u_2, u_3} (β := F) (fun (z : ℕ × E) ↦ p.partialSum z.1 z.2 - p.partialSum z.1 y)
    (SProd.sprod (α := Filter ℕ) atTop (𝓝 y)) (𝓝 0)
⊢ Tendsto (fun (z : ℕ × E) ↦ p.partialSum z.1 z.2) (SProd.sprod (α := Filter ℕ) atTop (𝓝 y)) (𝓝 (f (x + y)))

Tactic:
simpa using A.add this

Premises used: Filter.Tendsto.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
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
y : E
hf : HasFPowerSeriesWithinOnBall f p s x r
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
h'y : x + y ∈ insert x s
A : Tendsto (fun (z : ℕ × E) ↦ p.partialSum z.1 y) (SProd.sprod (α := Filter ℕ) atTop (𝓝 y)) (𝓝 (f (x + y)))
suffices :
  Tendsto.{u_2, u_3} (β := F) (fun (z : ℕ × E) ↦ p.partialSum z.1 z.2 - p.partialSum z.1 y)
    (SProd.sprod (α := Filter ℕ) atTop (𝓝 y)) (𝓝 0)
⊢ Tendsto (fun (z : ℕ × E) ↦ p.partialSum z.1 z.2) (SProd.sprod (α := Filter ℕ) atTop (𝓝 y)) (𝓝 (f (x + y)))

Tactic:
suffices Tendsto (fun (z : ℕ × E) ↦ p.partialSum z.1 z.2 - p.partialSum z.1 y)
    (atTop ×ˢ 𝓝 y) (𝓝 0) by simpa using A.add this
-- 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∞
y : E
hf : HasFPowerSeriesWithinOnBall f p s x r
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
h'y : x + y ∈ insert x s
A : Tendsto (fun (z : ℕ × E) ↦ p.partialSum z.1 y) (SProd.sprod (α := Filter ℕ) atTop (𝓝 y)) (𝓝 (f (x + y)))
apply :
  ∀ (ε : ℝ) (εpos : ε > 0),
    ∀ᶠ (x : ℕ × E) in SProd.sprod (α := Filter ℕ) atTop (𝓝 y), dist (p.partialSum x.1 x.2 - p.partialSum x.1 y) 0 < ε
⊢ Tendsto.{u_2, u_3} (β := F) (fun (z : ℕ × E) ↦ p.partialSum z.1 z.2 - p.partialSum z.1 y)
    (SProd.sprod (α := Filter ℕ) atTop (𝓝 y)) (𝓝 0)

Tactic:
apply Metric.tendsto_nhds.2 (fun ε εpos ↦ ?_)

Premises used: Iff.mpr, Metric.tendsto_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
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
y : E
hf : HasFPowerSeriesWithinOnBall f p s x r
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
h'y : x + y ∈ insert x s
A : Tendsto (fun (z : ℕ × E) ↦ p.partialSum z.1 y) (SProd.sprod (α := Filter ℕ) atTop (𝓝 y)) (𝓝 (f (x + y)))
ε : ℝ
εpos : ε > 0
⊢ ‖y‖ₑ < r

Tactic:
simp at 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
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
y : E
hf : HasFPowerSeriesWithinOnBall f p s x r
h'y : x + y ∈ insert x s
A : Tendsto (fun (z : ℕ × E) ↦ p.partialSum z.1 y) (SProd.sprod (α := Filter ℕ) atTop (𝓝 y)) (𝓝 (f (x + y)))
ε : ℝ
εpos : ε > 0
hy : ‖y‖ₑ < r
⊢ ∃ (r' : ℝ≥0), ‖y‖₊ < r' ∧ (↑r' : ℝ≥0∞) < r

Tactic:
simpa using ENNReal.lt_iff_exists_nnreal_btwn.1 hy

Premises used: ENNReal.lt_iff_exists_nnreal_btwn, Iff.mp
-- 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∞
y : E
hf : HasFPowerSeriesWithinOnBall f p s x r
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
h'y : x + y ∈ insert x s
A : Tendsto (fun (z : ℕ × E) ↦ p.partialSum z.1 y) (SProd.sprod (α := Filter ℕ) atTop (𝓝 y)) (𝓝 (f (x + y)))
ε : ℝ
εpos : ε > 0
obtain :
  ∀ (r' : ℝ≥0) (yr' : ‖y‖₊ < r') (r'r : (↑r' : ℝ≥0∞) < r),
    ∀ᶠ (x : ℕ × E) in SProd.sprod (α := Filter ℕ) atTop (𝓝 y), dist (p.partialSum x.1 x.2 - p.partialSum x.1 y) 0 < ε
⊢ ∀ᶠ (x : ℕ × E) in SProd.sprod (α := Filter ℕ) atTop (𝓝 y), dist (p.partialSum x.1 x.2 - p.partialSum x.1 y) 0 < ε

Tactic:
obtain ⟨r', yr', r'r⟩ : ∃ (r' : ℝ≥0), ‖y‖₊ < r' ∧ r' < r := by
    simp at hy
    simpa using ENNReal.lt_iff_exists_nnreal_btwn.1 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
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
y : E
hf : HasFPowerSeriesWithinOnBall f p s x r
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
h'y : x + y ∈ insert x s
A : Tendsto (fun (z : ℕ × E) ↦ p.partialSum z.1 y) (SProd.sprod (α := Filter ℕ) atTop (𝓝 y)) (𝓝 (f (x + y)))
ε : ℝ
εpos : ε > 0
r' : ℝ≥0
yr' : ‖y‖₊ < r'
r'r : (↑r' : ℝ≥0∞) < r
⊢ ‖y‖ < (↑r' : ℝ)

Tactic:
simpa [← coe_nnnorm] using yr'

Premises used: coe_nnnorm
-- 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∞
y : E
hf : HasFPowerSeriesWithinOnBall f p s x r
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
h'y : x + y ∈ insert x s
A : Tendsto (fun (z : ℕ × E) ↦ p.partialSum z.1 y) (SProd.sprod (α := Filter ℕ) atTop (𝓝 y)) (𝓝 (f (x + y)))
ε : ℝ
εpos : ε > 0
r' : ℝ≥0
yr' : ‖y‖₊ < r'
r'r : (↑r' : ℝ≥0∞) < r
⊢ ‖y‖ < (↑r' : ℝ)

Tactic:
have yr'_2 : ‖y‖ < r' := by simpa [← coe_nnnorm] using yr'
-- 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∞
y : E
hf : HasFPowerSeriesWithinOnBall f p s x r
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
h'y : x + y ∈ insert x s
A : Tendsto (fun (z : ℕ × E) ↦ p.partialSum z.1 y) (SProd.sprod (α := Filter ℕ) atTop (𝓝 y)) (𝓝 (f (x + y)))
ε : ℝ
εpos : ε > 0
r' : ℝ≥0
yr' : ‖y‖₊ < r'
r'r : (↑r' : ℝ≥0∞) < r
yr'_2 : ‖y‖ < (↑r' : ℝ)
S : Summable (α := ℝ) fun (n : ℕ) ↦ ‖p n‖ * (↑r' : ℝ) ^ n
⊢ Tendsto (β := ℝ)
    (fun (k : ℕ) ↦
      ∑' (n : ℕ),
        norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + k)) ↦ E) F) (p (n + k)) *
          (↑r' : ℝ) ^ (n + k))
    atTop (𝓝 0)

Tactic:
apply _root_.tendsto_sum_nat_add (f := fun n ↦ ‖p n‖ * ↑r' ^ n)

Premises used: Norm.norm, HMul.hMul, HPow.hPow, tendsto_sum_nat_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
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
y : E
hf : HasFPowerSeriesWithinOnBall f p s x r
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
h'y : x + y ∈ insert x s
A : Tendsto (fun (z : ℕ × E) ↦ p.partialSum z.1 y) (SProd.sprod (α := Filter ℕ) atTop (𝓝 y)) (𝓝 (f (x + y)))
ε : ℝ
εpos : ε > 0
r' : ℝ≥0
yr' : ‖y‖₊ < r'
r'r : (↑r' : ℝ≥0∞) < r
yr'_2 : ‖y‖ < (↑r' : ℝ)
S : Summable (α := ℝ) fun (n : ℕ) ↦ ‖p n‖ * (↑r' : ℝ) ^ n
⊢ Tendsto (β := ℝ)
    (fun (k : ℕ) ↦
      ∑' (n : ℕ),
        norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + k)) ↦ E) F) (p (n + k)) *
          (↑r' : ℝ) ^ (n + k))
    atTop (𝓝 0)

Tactic:
have : Tendsto (fun k ↦ ∑' n, ‖p (n + k)‖ * ↑r' ^ (n + k)) atTop (𝓝 0) := by
      apply _root_.tendsto_sum_nat_add (f := fun n ↦ ‖p n‖ * ↑r' ^ n)
-- 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∞
y : E
hf : HasFPowerSeriesWithinOnBall f p s x r
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
h'y : x + y ∈ insert x s
A : Tendsto (fun (z : ℕ × E) ↦ p.partialSum z.1 y) (SProd.sprod (α := Filter ℕ) atTop (𝓝 y)) (𝓝 (f (x + y)))
ε : ℝ
εpos : ε > 0
r' : ℝ≥0
yr' : ‖y‖₊ < r'
r'r : (↑r' : ℝ≥0∞) < r
yr'_2 : ‖y‖ < (↑r' : ℝ)
S : Summable (α := ℝ) fun (n : ℕ) ↦ ‖p n‖ * (↑r' : ℝ) ^ n
this :
  Tendsto (β := ℝ)
    (fun (k : ℕ) ↦
      ∑' (n : ℕ),
        norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + k)) ↦ E) F) (p (n + k)) *
          (↑r' : ℝ) ^ (n + k))
    atTop (𝓝 0)
linarith : ε / 4 ≤ 0 → 4 / 4 = 1
linarith₁ : ε / 4 ≤ 0 → HMul.hMul (α := ℝ) 1 4 = 4
linarith₂ : ε / 4 ≤ 0 → GT.gt (α := ℝ) 4 0
linarith₃ : ε / 4 ≤ 0 → 0 - ε + (1 * ε - HMul.hMul (α := ℝ) 4 0) = 0
⊢ ε / 4 > 0

Tactic:
linarith
-- 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∞
y : E
hf : HasFPowerSeriesWithinOnBall f p s x r
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
h'y : x + y ∈ insert x s
A : Tendsto (fun (z : ℕ × E) ↦ p.partialSum z.1 y) (SProd.sprod (α := Filter ℕ) atTop (𝓝 y)) (𝓝 (f (x + y)))
ε : ℝ
εpos : ε > 0
r' : ℝ≥0
yr' : ‖y‖₊ < r'
r'r : (↑r' : ℝ≥0∞) < r
yr'_2 : ‖y‖ < (↑r' : ℝ)
S : Summable (α := ℝ) fun (n : ℕ) ↦ ‖p n‖ * (↑r' : ℝ) ^ n
this :
  Tendsto (β := ℝ)
    (fun (k : ℕ) ↦
      ∑' (n : ℕ),
        norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + k)) ↦ E) F) (p (n + k)) *
          (↑r' : ℝ) ^ (n + k))
    atTop (𝓝 0)
⊢ ∃ (k : ℕ),
    ∑' (n : ℕ),
        norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + k)) ↦ E) F) (p (n + k)) *
          (↑r' : ℝ) ^ (n + k) <
      ε / 4

Tactic:
exact ((tendsto_order.1 this).2 _ (by linarith)).exists

Premises used: tendsto_order, Filter.Eventually.exists, And.right, Iff.mp
-- 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∞
y : E
hf : HasFPowerSeriesWithinOnBall f p s x r
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
h'y : x + y ∈ insert x s
A : Tendsto (fun (z : ℕ × E) ↦ p.partialSum z.1 y) (SProd.sprod (α := Filter ℕ) atTop (𝓝 y)) (𝓝 (f (x + y)))
ε : ℝ
εpos : ε > 0
r' : ℝ≥0
yr' : ‖y‖₊ < r'
r'r : (↑r' : ℝ≥0∞) < r
yr'_2 : ‖y‖ < (↑r' : ℝ)
S : Summable (α := ℝ) fun (n : ℕ) ↦ ‖p n‖ * (↑r' : ℝ) ^ n
obtain :
  ∀ (k : ℕ)
    (hk :
      ∑' (n : ℕ),
          norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + k)) ↦ E) F) (p (n + k)) *
            (↑r' : ℝ) ^ (n + k) <
        ε / 4),
    ∀ᶠ (x : ℕ × E) in SProd.sprod (α := Filter ℕ) atTop (𝓝 y), dist (p.partialSum x.1 x.2 - p.partialSum x.1 y) 0 < ε
⊢ ∀ᶠ (x : ℕ × E) in SProd.sprod (α := Filter ℕ) atTop (𝓝 y), dist (p.partialSum x.1 x.2 - p.partialSum x.1 y) 0 < ε

Tactic:
obtain ⟨k, hk⟩ : ∃ k, ∑' (n : ℕ), ‖p (n + k)‖ * ↑r' ^ (n + k) < ε / 4 := by
    have : Tendsto (fun k ↦ ∑' n, ‖p (n + k)‖ * ↑r' ^ (n + k)) atTop (𝓝 0) := by
      apply _root_.tendsto_sum_nat_add (f := fun n ↦ ‖p n‖ * ↑r' ^ n)
    exact ((tendsto_order.1 this).2 _ (by linarith)).exists
-- 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∞
y : E
hf : HasFPowerSeriesWithinOnBall f p s x r
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
h'y : x + y ∈ insert x s
A : Tendsto (fun (z : ℕ × E) ↦ p.partialSum z.1 y) (SProd.sprod (α := Filter ℕ) atTop (𝓝 y)) (𝓝 (f (x + y)))
ε : ℝ
εpos : ε > 0
r' : ℝ≥0
yr' : ‖y‖₊ < r'
r'r : (↑r' : ℝ≥0∞) < r
yr'_2 : ‖y‖ < (↑r' : ℝ)
S : Summable (α := ℝ) fun (n : ℕ) ↦ ‖p n‖ * (↑r' : ℝ) ^ n
k : ℕ
hk :
  ∑' (n : ℕ),
      norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + k)) ↦ E) F) (p (n + k)) *
        (↑r' : ℝ) ^ (n + k) <
    ε / 4
⊢ ContinuousAt.{u_2, u_3} (Y := F) (fun (z : E) ↦ p.partialSum k z) y

Tactic:
have : ContinuousAt (fun z ↦ p.partialSum k z) y := (p.partialSum_continuous k).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
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
y : E
hf : HasFPowerSeriesWithinOnBall f p s x r
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
h'y : x + y ∈ insert x s
A : Tendsto (fun (z : ℕ × E) ↦ p.partialSum z.1 y) (SProd.sprod (α := Filter ℕ) atTop (𝓝 y)) (𝓝 (f (x + y)))
ε : ℝ
εpos : ε > 0
r' : ℝ≥0
yr' : ‖y‖₊ < r'
r'r : (↑r' : ℝ≥0∞) < r
yr'_2 : ‖y‖ < (↑r' : ℝ)
S : Summable (α := ℝ) fun (n : ℕ) ↦ ‖p n‖ * (↑r' : ℝ) ^ n
k : ℕ
hk :
  ∑' (n : ℕ),
      norm (E := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + k)) ↦ E) F) (p (n + k)) *
        (↑r' : ℝ) ^ (n + k) <
    ε / 4
this : ContinuousAt.{u_2, u_3} (Y := F) (fun (z : E) ↦ p.partialSum k z) y
linarith : ε / 4 ≤ 0 → 4 / 4 = 1
linarith₁ : ε / 4 ≤ 0 → HMul.hMul (α := ℝ) 1 4 = 4
linarith₂ : ε / 4 ≤ 0 → GT.gt (α := ℝ) 4 0
linarith₃ : ε / 4 ≤ 0 → 4 / 4 = 1
linarith₄ : ε / 4 ≤ 0 → HMul.hMul (α := ℝ) 1 4 = 4
linarith₅ : ε / 4 ≤ 0 → GT.gt (α := ℝ) 4 0
linarith₆ : ε / 4 ≤ 0 → 0 - ε + (1 * ε - HMul.hMul (α := ℝ) 4 0) = 0
⊢ ε / 4 > 0

Tactic:
linarith