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∞
r' : ℝ≥0
hf : HasFPowerSeriesWithinOnBall f p s x r
h : (↑r' : ℝ≥0∞) < r
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Ioo 0 1) a
C : ℝ
hp :
  ∀ (y : E),
    Membership.mem (γ := Set E) (Metric.ball 0 (↑r' : ℝ)) y →
      ∀ (n : ℕ), x + y ∈ insert x s → ‖f (x + y) - p.partialSum n y‖ ≤ C * a ^ n
ε : ℝ
εpos : ε > 0
L : Tendsto (β := ℝ) (fun (n : ℕ) ↦ C * a ^ n) atTop (𝓝 0)
n : ℕ
hn : C * a ^ n < ε
y : E
hy : Membership.mem (γ := Set E) ((fun (x_1 : E) ↦ x + x_1) ⁻¹' insert x s ∩ Metric.ball 0 (↑r' : ℝ)) y
⊢ ‖f (x + y) - p.partialSum n y‖ < ε

Tactic:
(hp y hy.2 n hy.1).trans_lt hn

Premises used: And.right, And.left, LE.le.trans_lt
-- 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∞
r' : ℝ≥0
hf : HasFPowerSeriesWithinOnBall f p s x r
h : (↑r' : ℝ≥0∞) < r
a : ℝ
ha : Membership.mem (γ := Set ℝ) (Ioo 0 1) a
C : ℝ
hp :
  ∀ (y : E),
    Membership.mem (γ := Set E) (Metric.ball 0 (↑r' : ℝ)) y →
      ∀ (n : ℕ), x + y ∈ insert x s → ‖f (x + y) - p.partialSum n y‖ ≤ C * a ^ n
ε : ℝ
εpos : ε > 0
L : Tendsto (β := ℝ) (fun (n : ℕ) ↦ C * a ^ n) atTop (𝓝 0)
n : ℕ
hn : C * a ^ n < ε
y : E
hy : Membership.mem (γ := Set E) ((fun (x_1 : E) ↦ x + x_1) ⁻¹' insert x s ∩ Metric.ball 0 (↑r' : ℝ)) y
⊢ ‖f (x + y) - p.partialSum n y‖ < ε

Tactic:
exact (hp y hy.2 n hy.1).trans_lt hn

Premises used: And.right, And.left, LE.le.trans_lt
-- 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∞
r' : ℝ≥0
hf : HasFPowerSeriesWithinOnBall f p univ x r
h : (↑r' : ℝ≥0∞) < r
⊢ TendstoUniformlyOn.{u_2, u_3, 0} (β := F) (fun (n : ℕ) (y : E) ↦ p.partialSum n y) (fun (y : E) ↦ f (x + y)) atTop
    (Metric.ball 0 (↑r' : ℝ))

Tactic:
simpa using hf.tendstoUniformlyOn h

Premises used: HasFPowerSeriesWithinOnBall.tendstoUniformlyOn
-- 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
u : Set (F × F)
hu : u ∈ uniformity F
y : E
hy : Membership.mem (γ := Set E) ((fun (x_1 : E) ↦ x + x_1) ⁻¹' insert x s ∩ Metric.eball 0 r) y
rcases :
  ∀ (r' : ℝ≥0) (yr' : edist y 0 < (↑r' : ℝ≥0∞)) (hr' : (↑r' : ℝ≥0∞) < r),
    ∃ t ∈ 𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' insert x s ∩ Metric.eball 0 r] y,
      ∀ᶠ (n : ℕ) in atTop, ∀ y ∈ t, ((fun (y : E) ↦ f (x + y)) y, (fun (n : ℕ) (y : E) ↦ p.partialSum n y) n y) ∈ u
⊢ ∃ t ∈ 𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' insert x s ∩ Metric.eball 0 r] y,
    ∀ᶠ (n : ℕ) in atTop, ∀ y ∈ t, ((fun (y : E) ↦ f (x + y)) y, (fun (n : ℕ) (y : E) ↦ p.partialSum n y) n y) ∈ u

Tactic:
rcases ENNReal.lt_iff_exists_nnreal_btwn.1 hy.2 with ⟨r', yr', hr'⟩

Premises used: ENNReal.lt_iff_exists_nnreal_btwn, 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∞
hf : HasFPowerSeriesWithinOnBall f p s x r
u : Set (F × F)
hu : u ∈ uniformity F
y : E
hy : Membership.mem (γ := Set E) ((fun (x_1 : E) ↦ x + x_1) ⁻¹' insert x s ∩ Metric.eball 0 r) y
r' : ℝ≥0
yr' : edist y 0 < (↑r' : ℝ≥0∞)
hr' : (↑r' : ℝ≥0∞) < r
⊢ Metric.eball 0 (↑r' : ℝ≥0∞) ∈ 𝓝 y

Tactic:
have : Metric.eball (0 : E) r' ∈ 𝓝 y := IsOpen.mem_nhds Metric.isOpen_eball 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∞
hf : HasFPowerSeriesWithinOnBall f p s x r
u : Set (F × F)
hu : u ∈ uniformity F
y : E
hy : Membership.mem (γ := Set E) ((fun (x_1 : E) ↦ x + x_1) ⁻¹' insert x s ∩ Metric.eball 0 r) y
r' : ℝ≥0
yr' : edist y 0 < (↑r' : ℝ≥0∞)
hr' : (↑r' : ℝ≥0∞) < r
this : Metric.eball 0 (↑r' : ℝ≥0∞) ∈ 𝓝 y
⊢ ∃ t ∈ 𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' insert x s ∩ Metric.eball 0 r] y,
    ∀ᶠ (n : ℕ) in atTop, ∀ y ∈ t, ((fun (y : E) ↦ f (x + y)) y, (fun (n : ℕ) (y : E) ↦ p.partialSum n y) n y) ∈ u

Tactic:
⟨(x + ·)⁻¹' (insert x s) ∩ Metric.eball (0 : E) r', ?_, ?_⟩

Premises used: ENNReal.ofNNReal, Insert.insert, Metric.eball, Inter.inter, Set.preimage, HAdd.hAdd, And.intro, Exists.intro, OfNat.ofNat
-- 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
u : Set (F × F)
hu : u ∈ uniformity F
y : E
hy : Membership.mem (γ := Set E) ((fun (x_1 : E) ↦ x + x_1) ⁻¹' insert x s ∩ Metric.eball 0 r) y
r' : ℝ≥0
yr' : edist y 0 < (↑r' : ℝ≥0∞)
hr' : (↑r' : ℝ≥0∞) < r
this : Metric.eball 0 (↑r' : ℝ≥0∞) ∈ 𝓝 y
refine_1 :
  (fun (x_1 : E) ↦ x + x_1) ⁻¹' insert x s ∩ Metric.eball 0 (↑r' : ℝ≥0∞) ∈
    𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' insert x s ∩ Metric.eball 0 r] y
refine_2 :
  ∀ᶠ (n : ℕ) in atTop,
    ∀ (y : E),
      Membership.mem (γ := Set E) ((fun (x_1 : E) ↦ x + x_1) ⁻¹' insert x s ∩ Metric.eball 0 (↑r' : ℝ≥0∞)) y →
        ((fun (y : E) ↦ f (x + y)) y, (fun (n : ℕ) (y : E) ↦ p.partialSum n y) n y) ∈ u
⊢ ∃ t ∈ 𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' insert x s ∩ Metric.eball 0 r] y,
    ∀ᶠ (n : ℕ) in atTop, ∀ y ∈ t, ((fun (y : E) ↦ f (x + y)) y, (fun (n : ℕ) (y : E) ↦ p.partialSum n y) n y) ∈ u

Tactic:
refine ⟨(x + ·)⁻¹' (insert x s) ∩ Metric.eball (0 : E) r', ?_, ?_⟩
-- 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
u : Set (F × F)
hu : u ∈ uniformity F
y : E
hy : Membership.mem (γ := Set E) ((fun (x_1 : E) ↦ x + x_1) ⁻¹' insert x s ∩ Metric.eball 0 r) y
r' : ℝ≥0
yr' : edist y 0 < (↑r' : ℝ≥0∞)
hr' : (↑r' : ℝ≥0∞) < r
this : Metric.eball 0 (↑r' : ℝ≥0∞) ∈ 𝓝 y
refine_1 :
  (fun (x_1 : E) ↦ x + x_1) ⁻¹' insert x s ∩ Metric.eball 0 (↑r' : ℝ≥0∞) ∈ 𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' insert x s] y
refine_1₁ : Metric.eball 0 r ∈ 𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' insert x s] y
⊢ (fun (x_1 : E) ↦ x + x_1) ⁻¹' insert x s ∩ Metric.eball 0 (↑r' : ℝ≥0∞) ∈
    𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' insert x s ∩ Metric.eball 0 r] y

Tactic:
rw [nhdsWithin_inter_of_mem']

Premises used: nhdsWithin_inter_of_mem'
-- 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
u : Set (F × F)
hu : u ∈ uniformity F
y : E
hy : Membership.mem (γ := Set E) ((fun (x_1 : E) ↦ x + x_1) ⁻¹' insert x s ∩ Metric.eball 0 r) y
r' : ℝ≥0
yr' : edist y 0 < (↑r' : ℝ≥0∞)
hr' : (↑r' : ℝ≥0∞) < r
this : Metric.eball 0 (↑r' : ℝ≥0∞) ∈ 𝓝 y
⊢ (fun (x_1 : E) ↦ x + x_1) ⁻¹' insert x s ∩ Metric.eball 0 (↑r' : ℝ≥0∞) ∈ 𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' insert x s] y

Tactic:
inter_mem_nhdsWithin _ this

Premises used: inter_mem_nhdsWithin
-- 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
u : Set (F × F)
hu : u ∈ uniformity F
y : E
hy : Membership.mem (γ := Set E) ((fun (x_1 : E) ↦ x + x_1) ⁻¹' insert x s ∩ Metric.eball 0 r) y
r' : ℝ≥0
yr' : edist y 0 < (↑r' : ℝ≥0∞)
hr' : (↑r' : ℝ≥0∞) < r
this : Metric.eball 0 (↑r' : ℝ≥0∞) ∈ 𝓝 y
⊢ (fun (x_1 : E) ↦ x + x_1) ⁻¹' insert x s ∩ Metric.eball 0 (↑r' : ℝ≥0∞) ∈ 𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' insert x s] y

Tactic:
exact inter_mem_nhdsWithin _ this

Premises used: inter_mem_nhdsWithin
-- 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
u : Set (F × F)
hu : u ∈ uniformity F
y : E
hy : Membership.mem (γ := Set E) ((fun (x_1 : E) ↦ x + x_1) ⁻¹' insert x s ∩ Metric.eball 0 r) y
r' : ℝ≥0
yr' : edist y 0 < (↑r' : ℝ≥0∞)
hr' : (↑r' : ℝ≥0∞) < r
this : Metric.eball 0 (↑r' : ℝ≥0∞) ∈ 𝓝 y
refine_1 : Metric.eball 0 r ∈ 𝓝 y
⊢ Metric.eball 0 r ∈ 𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' insert x s] y

Tactic:
apply mem_nhdsWithin_of_mem_nhds

Premises used: mem_nhdsWithin_of_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
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
u : Set (F × F)
hu : u ∈ uniformity F
y : E
hy : Membership.mem (γ := Set E) ((fun (x_1 : E) ↦ x + x_1) ⁻¹' insert x s ∩ Metric.eball 0 r) y
r' : ℝ≥0
yr' : edist y 0 < (↑r' : ℝ≥0∞)
hr' : (↑r' : ℝ≥0∞) < r
this : Metric.eball 0 (↑r' : ℝ≥0∞) ∈ 𝓝 y
⊢ Metric.eball 0 r ∈ 𝓝 y

Tactic:
apply Filter.mem_of_superset this (Metric.eball_subset_eball hr'.le)

Premises used: Metric.eball_subset_eball, LT.lt.le, Filter.mem_of_superset
-- 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
u : Set (F × F)
hu : u ∈ uniformity F
y : E
hy : Membership.mem (γ := Set E) ((fun (x_1 : E) ↦ x + x_1) ⁻¹' insert x s ∩ Metric.eball 0 r) y
r' : ℝ≥0
yr' : edist y 0 < (↑r' : ℝ≥0∞)
hr' : (↑r' : ℝ≥0∞) < r
this : Metric.eball 0 (↑r' : ℝ≥0∞) ∈ 𝓝 y
⊢ ∀ᶠ (n : ℕ) in atTop,
    ∀ (y : E),
      Membership.mem (γ := Set E) ((fun (x_1 : E) ↦ x + x_1) ⁻¹' insert x s ∩ Metric.eball 0 (↑r' : ℝ≥0∞)) y →
        ((fun (y : E) ↦ f (x + y)) y, (fun (n : ℕ) (y : E) ↦ p.partialSum n y) n y) ∈ u

Tactic:
simpa [Metric.eball_coe] using hf.tendstoUniformlyOn hr' u hu

Premises used: HasFPowerSeriesWithinOnBall.tendstoUniformlyOn, Metric.eball_coe
-- 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
⊢ HasFPowerSeriesWithinOnBall f p univ x r

Tactic:
rw [← hasFPowerSeriesWithinOnBall_univ] at hf

Premises used: hasFPowerSeriesWithinOnBall_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
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p univ x r
⊢ TendstoLocallyUniformlyOn.{u_2, u_3, 0} (β := F) (fun (n : ℕ) (y : E) ↦ p.partialSum n y) (fun (y : E) ↦ f (x + y))
    atTop (Metric.eball 0 r)

Tactic:
simpa using hf.tendstoLocallyUniformlyOn

Premises used: HasFPowerSeriesWithinOnBall.tendstoLocallyUniformlyOn
-- 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∞
r' : ℝ≥0
hf : HasFPowerSeriesWithinOnBall f p s x r
h : (↑r' : ℝ≥0∞) < r
⊢ TendstoUniformlyOn.{u_2, u_3, 0} (α := E) (β := F)
    (fun (n : ℕ) ↦ (fun (y : E) ↦ p.partialSum n y) ∘ fun (y : E) ↦ y - x)
    ((fun (y : E) ↦ f (x + y)) ∘ fun (y : E) ↦ y - x) atTop
    (preimage (β := E) (fun (y : E) ↦ y - x) ((fun (x_1 : E) ↦ x + x_1) ⁻¹' insert x s ∩ Metric.ball 0 (↑r' : ℝ)))

Tactic:
(hf.tendstoUniformlyOn h).comp fun y => y - x

Premises used: TendstoUniformlyOn.comp, HSub.hSub, HasFPowerSeriesWithinOnBall.tendstoUniformlyOn
-- 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∞
r' : ℝ≥0
hf : HasFPowerSeriesWithinOnBall f p s x r
h : (↑r' : ℝ≥0∞) < r
h₁ : f = (fun (y : E) ↦ f (x + y)) ∘ fun (y : E) ↦ y - x
h₂ :
  insert x s ∩ Metric.ball x (↑r' : ℝ) =
    preimage (β := E) (fun (y : E) ↦ y - x) ((fun (x_1 : E) ↦ x + x_1) ⁻¹' insert x s ∩ Metric.ball 0 (↑r' : ℝ))
⊢ TendstoUniformlyOn (fun (n : ℕ) (y : E) ↦ p.partialSum n (y - x)) f atTop (insert x s ∩ Metric.ball x (↑r' : ℝ))

Tactic:
convert! (hf.tendstoUniformlyOn h).comp fun y => y - x using 1

Premises used: TendstoUniformlyOn.comp, HSub.hSub, HasFPowerSeriesWithinOnBall.tendstoUniformlyOn
-- 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∞
r' : ℝ≥0
hf : HasFPowerSeriesWithinOnBall f p s x r
h : (↑r' : ℝ≥0∞) < r
⊢ f = (fun (y : E) ↦ f (x + y)) ∘ fun (y : E) ↦ y - x

Tactic:
simp [Function.comp_def]

Premises used: Function.comp_def
-- 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∞
r' : ℝ≥0
hf : HasFPowerSeriesWithinOnBall f p s x r
h : (↑r' : ℝ≥0∞) < r
h₁ :
  ∀ (z : E),
    z ∈ insert x s ∩ Metric.ball x (↑r' : ℝ) ↔
      Membership.mem (γ := Set E)
        (preimage (β := E) (fun (y : E) ↦ y - x) ((fun (x_1 : E) ↦ x + x_1) ⁻¹' insert x s ∩ Metric.ball 0 (↑r' : ℝ))) z
⊢ insert x s ∩ Metric.ball x (↑r' : ℝ) =
    preimage (β := E) (fun (y : E) ↦ y - x) ((fun (x_1 : E) ↦ x + x_1) ⁻¹' insert x s ∩ Metric.ball 0 (↑r' : ℝ))

Tactic:
ext z
-- 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∞
r' : ℝ≥0
hf : HasFPowerSeriesWithinOnBall f p s x r
h : (↑r' : ℝ≥0∞) < r
z : E
⊢ z ∈ insert x s ∩ Metric.ball x (↑r' : ℝ) ↔
    Membership.mem (γ := Set E)
      (preimage (β := E) (fun (y : E) ↦ y - x) ((fun (x_1 : E) ↦ x + x_1) ⁻¹' insert x s ∩ Metric.ball 0 (↑r' : ℝ))) z

Tactic:
simp [dist_eq_norm]

Premises used: dist_eq_norm
-- 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∞
r' : ℝ≥0
hf : HasFPowerSeriesWithinOnBall f p univ x r
h : (↑r' : ℝ≥0∞) < r
⊢ TendstoUniformlyOn (fun (n : ℕ) (y : E) ↦ p.partialSum n (y - x)) f atTop (Metric.ball x (↑r' : ℝ))

Tactic:
simpa using hf.tendstoUniformlyOn' h

Premises used: HasFPowerSeriesWithinOnBall.tendstoUniformlyOn'
-- 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
⊢ ContinuousOn (Y := E) (fun (y : E) ↦ y - x) (insert x s ∩ Metric.eball x r)

Tactic:
fun_prop
-- 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
⊢ ContinuousOn (Y := E) (fun (y : E) ↦ y - x) (insert x s ∩ Metric.eball x r)

Tactic:
have A : ContinuousOn (fun y : E => y - x) (insert x s ∩ Metric.eball (x : E) r) := by fun_prop
-- 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
A : ContinuousOn (Y := E) (fun (y : E) ↦ y - x) (insert x s ∩ Metric.eball x r)
⊢ TendstoLocallyUniformlyOn.{u_2, u_3, 0} (β := F)
    (fun (n : ℕ) ↦ (fun (y : E) ↦ p.partialSum n y) ∘ fun (y : E) ↦ y - x)
    ((fun (y : E) ↦ f (x + y)) ∘ fun (y : E) ↦ y - x) atTop (insert x s ∩ Metric.eball x r)

Tactic:
hf.tendstoLocallyUniformlyOn.comp (fun y : E => y - x) _ A

Premises used: HasFPowerSeriesWithinOnBall.tendstoLocallyUniformlyOn, HSub.hSub, TendstoLocallyUniformlyOn.comp
-- 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
A : ContinuousOn (Y := E) (fun (y : E) ↦ y - x) (insert x s ∩ Metric.eball x r)
h : f = (fun (y : E) ↦ f (x + y)) ∘ fun (y : E) ↦ y - x
convert! :
  MapsTo (β := E) (fun (y : E) ↦ y - x) (insert x s ∩ Metric.eball x r)
    ((fun (x_1 : E) ↦ x + x_1) ⁻¹' insert x s ∩ Metric.eball 0 r)
⊢ TendstoLocallyUniformlyOn (fun (n : ℕ) (y : E) ↦ p.partialSum n (y - x)) f atTop (insert x s ∩ Metric.eball x r)

Tactic:
convert! hf.tendstoLocallyUniformlyOn.comp (fun y : E => y - x) _ A using 1

Premises used: HasFPowerSeriesWithinOnBall.tendstoLocallyUniformlyOn, HSub.hSub, TendstoLocallyUniformlyOn.comp
-- 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
A : ContinuousOn (Y := E) (fun (y : E) ↦ y - x) (insert x s ∩ Metric.eball x r)
h : ∀ (z : E), f z = ((fun (y : E) ↦ f (x + y)) ∘ fun (y : E) ↦ y - x) z
⊢ f = (fun (y : E) ↦ f (x + y)) ∘ fun (y : E) ↦ y - x

Tactic:
ext z
-- 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
A : ContinuousOn (Y := E) (fun (y : E) ↦ y - x) (insert x s ∩ Metric.eball x r)
z : E
⊢ f z = ((fun (y : E) ↦ f (x + y)) ∘ fun (y : E) ↦ y - x) z

Tactic:
simp
-- 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
A : ContinuousOn (Y := E) (fun (y : E) ↦ y - x) (insert x s ∩ Metric.eball x r)
z : E
⊢ z ∈ insert x s ∩ Metric.eball x r →
    Membership.mem (γ := Set E) ((fun (x_1 : E) ↦ x + x_1) ⁻¹' insert x s ∩ Metric.eball 0 r) ((fun (y : E) ↦ y - x) z)

Tactic:
simp [edist_eq_enorm_sub]

Premises used: edist_eq_enorm_sub
-- 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 : HasFPowerSeriesWithinOnBall f p univ x r
⊢ TendstoLocallyUniformlyOn (fun (n : ℕ) (y : E) ↦ p.partialSum n (y - x)) f atTop (Metric.eball x r)

Tactic:
simpa using hf.tendstoLocallyUniformlyOn'

Premises used: HasFPowerSeriesWithinOnBall.tendstoLocallyUniformlyOn'
-- 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
⊢ ContinuousOn f (insert x s ∩ Metric.eball x r)

Tactic:
hf.tendstoLocallyUniformlyOn'.continuousOn <|
    Frequently.of_forall fun n =>
      ((p.partialSum_continuous n).comp (continuous_id.sub continuous_const)).continuousOn

Premises used: Continuous.continuousOn, Filter.Frequently.of_forall, Continuous.comp, continuous_const, FormalMultilinearSeries.partialSum_continuous, TendstoLocallyUniformlyOn.continuousOn, HasFPowerSeriesWithinOnBall.tendstoLocallyUniformlyOn', continuous_id, Continuous.sub
-- 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 : HasFPowerSeriesWithinOnBall f p univ x r
⊢ ContinuousOn f (Metric.eball x r)

Tactic:
simpa using hf.continuousOn

Premises used: HasFPowerSeriesWithinOnBall.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
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
⊢ x ∈ insert x s ∩ Metric.eball x r

Tactic:
simp [hf.r_pos]

Premises used: 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
apply : insert x s ∩ Metric.eball x r ∈ 𝓝[insert x s] x
⊢ ContinuousWithinAt f (insert x s) x

Tactic:
apply (hf.continuousOn.continuousWithinAt (x := x) (by simp [hf.r_pos])).mono_of_mem_nhdsWithin

Premises used: HasFPowerSeriesWithinOnBall.continuousOn, ContinuousWithinAt.mono_of_mem_nhdsWithin, ContinuousOn.continuousWithinAt