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
x : E
r r' : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p univ x r
hr : r' < r
⊢ IsBigO.{u_2, u_3, 0} (E := F) (F := ℝ) (𝓟 (Metric.eball (x, x) r'))
    (fun (y : E × E) ↦
      HSub.hSub (β := F) (f y.1 - f y.2) ((p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ y.1 - y.2 : F))
    fun (y : E × E) ↦ ‖y - (x, x)‖ * ‖y.1 - y.2‖

Tactic:
simpa using hf.isBigO_image_sub_image_sub_deriv_principal hr

Premises used: HasFPowerSeriesWithinOnBall.isBigO_image_sub_image_sub_deriv_principal
-- 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 r' : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
hr : r' < r
⊢ IsBigO.{u_2, u_3, 0} (E := F) (F := ℝ) (𝓟 (Metric.eball (x, x) r' ∩ insert x s ×ˢ insert x s))
    (fun (y : E × E) ↦
      HSub.hSub (β := F) (f y.1 - f y.2) ((p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ y.1 - y.2 : F))
    fun (y : E × E) ↦ ‖y - (x, x)‖ * ‖y.1 - y.2‖

Tactic:
have := hf.isBigO_image_sub_image_sub_deriv_principal 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 r' : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
hr : r' < r
this :
  IsBigO.{u_2, u_3, 0} (E := F) (F := ℝ) (𝓟 (Metric.eball (x, x) r' ∩ insert x s ×ˢ insert x s))
    (fun (y : E × E) ↦
      HSub.hSub (β := F) (f y.1 - f y.2) ((p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ y.1 - y.2 : F))
    fun (y : E × E) ↦ ‖y - (x, x)‖ * ‖y.1 - y.2‖
simp :
  ∀
    (this :
      ∃ (c : ℝ),
        ∀ (a b : E),
          edist a x < r' →
            edist b x < r' →
              a ∈ insert x s →
                b ∈ insert x s →
                  ‖HSub.hSub (β := F) (f a - f b) ((p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ a - b : F)‖ ≤
                    c * (‖(a, b) - (x, x)‖ * ‖a - b‖)),
    ∃ (C : ℝ),
      ∀ y ∈ insert x s,
        edist y x < r' →
          ∀ z ∈ insert x s,
            edist z x < r' →
              ‖HSub.hSub (β := F) (f y - f z) ((p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ y - z : F)‖ ≤
                C * (max ‖y - x‖ ‖z - x‖ * ‖y - z‖)
⊢ ∃ (C : ℝ),
    ∀ y ∈ insert x s ∩ Metric.eball x r',
      ∀ z ∈ insert x s ∩ Metric.eball x r',
        ‖HSub.hSub (β := F) (f y - f z) ((p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ y - z : F)‖ ≤
          C * max ‖y - x‖ ‖z - x‖ * ‖y - z‖

Tactic:
simp only [isBigO_principal, mem_inter_iff, Metric.mem_eball, Prod.edist_eq, max_lt_iff, mem_prod,
    norm_mul, Real.norm_eq_abs, abs_norm, and_imp, Prod.forall, mul_assoc] at this ⊢

Premises used: Prod.edist_eq, and_imp, Set.mem_inter_iff, mul_assoc, max_lt_iff, norm_mul, Set.mem_prod, Asymptotics.isBigO_principal, Prod.forall, abs_norm, Real.norm_eq_abs, Metric.mem_eball
-- 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 r' : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
hr : r' < r
this :
  ∃ (c : ℝ),
    ∀ (a b : E),
      edist a x < r' →
        edist b x < r' →
          a ∈ insert x s →
            b ∈ insert x s →
              ‖HSub.hSub (β := F) (f a - f b) ((p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ a - b : F)‖ ≤
                c * (‖(a, b) - (x, x)‖ * ‖a - b‖)
rcases :
  ∀ (C : ℝ)
    (hC :
      ∀ (a b : E),
        edist a x < r' →
          edist b x < r' →
            a ∈ insert x s →
              b ∈ insert x s →
                ‖HSub.hSub (β := F) (f a - f b) ((p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ a - b : F)‖ ≤
                  C * (‖(a, b) - (x, x)‖ * ‖a - b‖)),
    ∃ (C : ℝ),
      ∀ y ∈ insert x s,
        edist y x < r' →
          ∀ z ∈ insert x s,
            edist z x < r' →
              ‖HSub.hSub (β := F) (f y - f z) ((p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ y - z : F)‖ ≤
                C * (max ‖y - x‖ ‖z - x‖ * ‖y - z‖)
⊢ ∃ (C : ℝ),
    ∀ y ∈ insert x s,
      edist y x < r' →
        ∀ z ∈ insert x s,
          edist z x < r' →
            ‖HSub.hSub (β := F) (f y - f z) ((p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ y - z : F)‖ ≤
              C * (max ‖y - x‖ ‖z - x‖ * ‖y - z‖)

Tactic:
rcases this with ⟨C, hC⟩
-- 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 r' : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
hr : r' < r
C : ℝ
hC :
  ∀ (a b : E),
    edist a x < r' →
      edist b x < r' →
        a ∈ insert x s →
          b ∈ insert x s →
            ‖HSub.hSub (β := F) (f a - f b) ((p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ a - b : F)‖ ≤
              C * (‖(a, b) - (x, x)‖ * ‖a - b‖)
⊢ ∃ (C : ℝ),
    ∀ y ∈ insert x s,
      edist y x < r' →
        ∀ z ∈ insert x s,
          edist z x < r' →
            ‖HSub.hSub (β := F) (f y - f z) ((p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ y - z : F)‖ ≤
              C * (max ‖y - x‖ ‖z - x‖ * ‖y - z‖)

Tactic:
⟨C, fun y ys hy z zs hz ↦ hC y z hy hz ys zs⟩

Premises used: Exists.intro
-- 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 r' : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
hr : r' < r
C : ℝ
hC :
  ∀ (a b : E),
    edist a x < r' →
      edist b x < r' →
        a ∈ insert x s →
          b ∈ insert x s →
            ‖HSub.hSub (β := F) (f a - f b) ((p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ a - b : F)‖ ≤
              C * (‖(a, b) - (x, x)‖ * ‖a - b‖)
⊢ ∃ (C : ℝ),
    ∀ y ∈ insert x s,
      edist y x < r' →
        ∀ z ∈ insert x s,
          edist z x < r' →
            ‖HSub.hSub (β := F) (f y - f z) ((p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ y - z : F)‖ ≤
              C * (max ‖y - x‖ ‖z - x‖ * ‖y - z‖)

Tactic:
exact ⟨C, fun y ys hy z zs hz ↦ hC y z hy hz ys zs⟩
-- 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 r' : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p univ x r
hr : r' < r
⊢ ∃ (C : ℝ),
    ∀ y ∈ Metric.eball x r',
      ∀ z ∈ Metric.eball x r',
        ‖HSub.hSub (β := F) (f y - f z) ((p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ y - z : F)‖ ≤
          C * max ‖y - x‖ ‖z - x‖ * ‖y - z‖

Tactic:
simpa only [mem_univ, insert_eq_of_mem, univ_inter] using hf.image_sub_sub_deriv_le hr

Premises used: Set.insert_eq_of_mem, HasFPowerSeriesWithinOnBall.image_sub_sub_deriv_le, Set.univ_inter, Set.mem_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
s : Set E
x : E
hf : HasFPowerSeriesWithinAt f p s x
rcases :
  ∀ (r : ℝ≥0∞) (hf : HasFPowerSeriesWithinOnBall f p s x r),
    IsBigO.{u_2, u_3, 0} (E := F) (F := ℝ) (𝓝[insert x s ×ˢ insert x s] (x, x))
      (fun (y : E × E) ↦
        HSub.hSub (β := F) (f y.1 - f y.2) ((p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ y.1 - y.2 : F))
      fun (y : E × E) ↦ ‖y - (x, x)‖ * ‖y.1 - y.2‖
⊢ IsBigO.{u_2, u_3, 0} (E := F) (F := ℝ) (𝓝[insert x s ×ˢ insert x s] (x, x))
    (fun (y : E × E) ↦
      HSub.hSub (β := F) (f y.1 - f y.2) ((p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ y.1 - y.2 : F))
    fun (y : E × E) ↦ ‖y - (x, x)‖ * ‖y.1 - y.2‖

Tactic:
rcases hf with ⟨r, hf⟩
-- 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
rcases :
  ∀ (r' : ℝ≥0) (r'0 : 0 < (↑r' : ℝ≥0∞)) (h : (↑r' : ℝ≥0∞) < r),
    IsBigO.{u_2, u_3, 0} (E := F) (F := ℝ) (𝓝[insert x s ×ˢ insert x s] (x, x))
      (fun (y : E × E) ↦
        HSub.hSub (β := F) (f y.1 - f y.2) ((p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ y.1 - y.2 : F))
      fun (y : E × E) ↦ ‖y - (x, x)‖ * ‖y.1 - y.2‖
⊢ IsBigO.{u_2, u_3, 0} (E := F) (F := ℝ) (𝓝[insert x s ×ˢ insert x s] (x, x))
    (fun (y : E × E) ↦
      HSub.hSub (β := F) (f y.1 - f y.2) ((p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ y.1 - y.2 : F))
    fun (y : E × E) ↦ ‖y - (x, x)‖ * ‖y.1 - y.2‖

Tactic:
rcases ENNReal.lt_iff_exists_nnreal_btwn.1 hf.r_pos with ⟨r', r'0, h⟩

Premises used: ENNReal.lt_iff_exists_nnreal_btwn, Iff.mp, 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
r' : ℝ≥0
r'0 : 0 < (↑r' : ℝ≥0∞)
h : (↑r' : ℝ≥0∞) < r
⊢ IsBigO.{u_2, u_3, 0} (E := F) (F := ℝ) (𝓝[insert x s ×ˢ insert x s] (x, x))
    (fun (y : E × E) ↦
      HSub.hSub (β := F) (f y.1 - f y.2) ((p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ y.1 - y.2 : F))
    fun (y : E × E) ↦ ‖y - (x, x)‖ * ‖y.1 - y.2‖

Tactic:
(hf.isBigO_image_sub_image_sub_deriv_principal h).mono ?_

Premises used: HasFPowerSeriesWithinOnBall.isBigO_image_sub_image_sub_deriv_principal, Asymptotics.IsBigO.mono
-- 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
r' : ℝ≥0
r'0 : 0 < (↑r' : ℝ≥0∞)
h : (↑r' : ℝ≥0∞) < r
refine : 𝓝[insert x s ×ˢ insert x s] (x, x) ≤ 𝓟 (Metric.eball (x, x) (↑r' : ℝ≥0∞) ∩ insert x s ×ˢ insert x s)
⊢ IsBigO.{u_2, u_3, 0} (E := F) (F := ℝ) (𝓝[insert x s ×ˢ insert x s] (x, x))
    (fun (y : E × E) ↦
      HSub.hSub (β := F) (f y.1 - f y.2) ((p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ y.1 - y.2 : F))
    fun (y : E × E) ↦ ‖y - (x, x)‖ * ‖y.1 - y.2‖

Tactic:
refine (hf.isBigO_image_sub_image_sub_deriv_principal h).mono ?_

Premises used: HasFPowerSeriesWithinOnBall.isBigO_image_sub_image_sub_deriv_principal, Asymptotics.IsBigO.mono
-- 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
r' : ℝ≥0
r'0 : 0 < (↑r' : ℝ≥0∞)
h : (↑r' : ℝ≥0∞) < r
rw : 𝓝[insert x s ×ˢ insert x s] (x, x) ≤ 𝓟 (insert x s ×ˢ insert x s ∩ Metric.eball (x, x) (↑r' : ℝ≥0∞))
⊢ 𝓝[insert x s ×ˢ insert x s] (x, x) ≤ 𝓟 (Metric.eball (x, x) (↑r' : ℝ≥0∞) ∩ insert x s ×ˢ insert x s)

Tactic:
rw [inter_comm]

Premises used: Set.inter_comm
-- 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
r' : ℝ≥0
r'0 : 0 < (↑r' : ℝ≥0∞)
h : (↑r' : ℝ≥0∞) < r
⊢ 𝓝[insert x s ×ˢ insert x s] (x, x) ≤ 𝓟 (insert x s ×ˢ insert x s ∩ Metric.eball (x, x) (↑r' : ℝ≥0∞))

Tactic:
le_principal_iff.2 (inter_mem_nhdsWithin _ (Metric.eball_mem_nhds _ r'0))

Premises used: Iff.mpr, inter_mem_nhdsWithin, Filter.le_principal_iff, Metric.eball_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
r' : ℝ≥0
r'0 : 0 < (↑r' : ℝ≥0∞)
h : (↑r' : ℝ≥0∞) < r
⊢ 𝓝[insert x s ×ˢ insert x s] (x, x) ≤ 𝓟 (insert x s ×ˢ insert x s ∩ Metric.eball (x, x) (↑r' : ℝ≥0∞))

Tactic:
exact le_principal_iff.2 (inter_mem_nhdsWithin _ (Metric.eball_mem_nhds _ r'0))

Premises used: Iff.mpr, inter_mem_nhdsWithin, Filter.le_principal_iff, Metric.eball_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
x : E
hf : HasFPowerSeriesAt f p x
⊢ HasFPowerSeriesWithinAt f p univ x

Tactic:
rw [← hasFPowerSeriesWithinAt_univ] at hf

Premises used: hasFPowerSeriesWithinAt_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
hf : HasFPowerSeriesWithinAt f p univ x
⊢ IsBigO.{u_2, u_3, 0} (E := F) (F := ℝ) (𝓝 (x, x))
    (fun (y : E × E) ↦
      HSub.hSub (β := F) (f y.1 - f y.2) ((p 1 : (a : (i : Fin 1) → E) → F) fun (x : Fin 1) ↦ y.1 - y.2 : F))
    fun (y : E × E) ↦ ‖y - (x, x)‖ * ‖y.1 - y.2‖

Tactic:
simpa using hf.isBigO_image_sub_norm_mul_norm_sub

Premises used: HasFPowerSeriesWithinAt.isBigO_image_sub_norm_mul_norm_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
s : Set E
x : E
r : ℝ≥0∞
r' : ℝ≥0
hf : HasFPowerSeriesWithinOnBall f p s x r
h : (↑r' : ℝ≥0∞) < r
⊢ ∃ (a : ℝ),
    Membership.mem (γ := Set ℝ) (Ioo 0 1) a ∧
      ∃ C > 0,
        ∀ (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

Tactic:
hf.uniform_geometric_approx h

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

Tactic:
obtain ⟨a, ha, C, -, hp⟩ : ∃ a ∈ Ioo (0 : ℝ) 1, ∃ C > 0, ∀ y ∈ Metric.ball (0 : E) r', ∀ n,
    x + y ∈ insert x s → ‖f (x + y) - p.partialSum n y‖ ≤ C * a ^ n := hf.uniform_geometric_approx h

Premises used: HasFPowerSeriesWithinOnBall.uniform_geometric_approx, Metric.ball, OfNat.ofNat, NNReal.toReal, Set.Ioo
-- 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
⊢ TendstoUniformlyOn.{u_2, u_3, 0} (β := F) (fun (n : ℕ) (y : E) ↦ p.partialSum n y) (fun (y : E) ↦ f (x + y)) atTop
    ((fun (x_1 : E) ↦ x + x_1) ⁻¹' insert x s ∩ Metric.ball 0 (↑r' : ℝ))

Tactic:
Metric.tendstoUniformlyOn_iff.2 fun ε εpos => ?_

Premises used: Iff.mpr, Metric.tendstoUniformlyOn_iff
-- 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
refine :
  ∀ (ε : ℝ) (εpos : ε > 0),
    ∀ᶠ (n : ℕ) in atTop,
      ∀ (x_1 : E),
        Membership.mem (γ := Set E) ((fun (x_2 : E) ↦ x + x_2) ⁻¹' insert x s ∩ Metric.ball 0 (↑r' : ℝ)) x_1 →
          dist (f (x + x_1)) (p.partialSum n x_1) < ε
⊢ TendstoUniformlyOn.{u_2, u_3, 0} (β := F) (fun (n : ℕ) (y : E) ↦ p.partialSum n y) (fun (y : E) ↦ f (x + y)) atTop
    ((fun (x_1 : E) ↦ x + x_1) ⁻¹' insert x s ∩ Metric.ball 0 (↑r' : ℝ))

Tactic:
refine Metric.tendstoUniformlyOn_iff.2 fun ε εpos => ?_

Premises used: Iff.mpr, Metric.tendstoUniformlyOn_iff
-- 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
⊢ Tendsto (fun (n : ℕ) ↦ C * a ^ n) atTop (𝓝 (C * 0))

Tactic:
have L : Tendsto (fun n => (C : ℝ) * a ^ n) atTop (𝓝 ((C : ℝ) * 0)) :=
    tendsto_const_nhds.mul (tendsto_pow_atTop_nhds_zero_of_lt_one ha.1.le ha.2)
-- 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 (𝓝 (C * 0))
⊢ Tendsto (β := ℝ) (fun (n : ℕ) ↦ C * a ^ n) atTop (𝓝 0)

Tactic:
rw [mul_zero] at L

Premises used: MulZeroClass.mul_zero
-- 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 : ℕ) in atTop,
    ∀ (x_1 : E),
      Membership.mem (γ := Set E) ((fun (x_2 : E) ↦ x + x_2) ⁻¹' insert x s ∩ Metric.ball 0 (↑r' : ℝ)) x_1 →
        dist (f (x + x_1)) (p.partialSum n x_1) < ε

Tactic:
(L.eventually (gt_mem_nhds εpos)).mono fun n hn y hy => ?_

Premises used: gt_mem_nhds, Filter.Eventually.mono, Filter.Tendsto.eventually
-- 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)
refine :
  ∀ (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),
    dist (f (x + y)) (p.partialSum n y) < ε
⊢ ∀ᶠ (n : ℕ) in atTop,
    ∀ (x_1 : E),
      Membership.mem (γ := Set E) ((fun (x_2 : E) ↦ x + x_2) ⁻¹' insert x s ∩ Metric.ball 0 (↑r' : ℝ)) x_1 →
        dist (f (x + x_1)) (p.partialSum n x_1) < ε

Tactic:
refine (L.eventually (gt_mem_nhds εpos)).mono fun n hn y hy => ?_

Premises used: gt_mem_nhds, Filter.Eventually.mono, Filter.Tendsto.eventually
-- 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
rw : ‖f (x + y) - p.partialSum n y‖ < ε
⊢ dist (f (x + y)) (p.partialSum n y) < ε

Tactic:
rw [dist_eq_norm]

Premises used: dist_eq_norm