awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
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} (β := 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' : ℝ))
have 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' : ℝ))
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
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
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' : ℝ))
have 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) < ε
Tactic: refine Metric.tendstoUniformlyOn_iff.2 fun ε εpos => ?_
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (hypothesis)
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
⊢ ∀ᶠ (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) < ε
have L : 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)
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (hypothesis)
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))
⊢ ∀ᶠ (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) < ε
have L₁ : Tendsto (β := ℝ) (fun (n : ℕ) ↦ C * a ^ n) atTop (𝓝 0)
Tactic: rw [mul_zero] at L
Cleared hypotheses: L
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
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) < ε
have 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) < ε
Tactic: refine (L.eventually (gt_mem_nhds εpos)).mono fun n hn y hy => ?_
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
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
⊢ dist (f (x + y)) (p.partialSum n y) < ε
have rw : ‖f (x + y) - p.partialSum n y‖ < ε
Tactic: rw [dist_eq_norm]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (hypothesis)
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 : HasFPowerSeriesOnBall f p 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' : ℝ))
have hf₁ : HasFPowerSeriesWithinOnBall f p univ x r
Tactic: rw [← hasFPowerSeriesWithinOnBall_univ] at hf
Cleared hypotheses: hf, h
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
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
⊢ ∃ 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
have 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
Tactic: rcases ENNReal.lt_iff_exists_nnreal_btwn.1 hy.2 with ⟨r', yr', hr'⟩
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (hypothesis)
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
⊢ ∃ 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
have this : Metric.eball 0 (↑r' : ℝ≥0∞) ∈ 𝓝 y
Tactic: have : Metric.eball (0 : E) r' ∈ 𝓝 y := IsOpen.mem_nhds Metric.isOpen_eball yr'
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
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
have 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
Tactic: refine ⟨(x + ·)⁻¹' (insert x s) ∩ Metric.eball (0 : E) r', ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
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
⊢ ∃ 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
have 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
Tactic: refine ⟨(x + ·)⁻¹' (insert x s) ∩ Metric.eball (0 : E) r', ?_, ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
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 ∩ Metric.eball 0 r] y
have 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
Tactic: rw [nhdsWithin_inter_of_mem']
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
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
⊢ (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
have refine_1₁ : Metric.eball 0 r ∈ 𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' insert x s] y
Tactic: rw [nhdsWithin_inter_of_mem']
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
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 ∈ 𝓝[(fun (x_1 : E) ↦ x + x_1) ⁻¹' insert x s] y
have refine_1 : Metric.eball 0 r ∈ 𝓝 y
Tactic: apply mem_nhdsWithin_of_mem_nhds
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (hypothesis)
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
⊢ 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)
have hf₁ : HasFPowerSeriesWithinOnBall f p univ x r
Tactic: rw [← hasFPowerSeriesWithinOnBall_univ] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
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 (fun (n : ℕ) (y : E) ↦ p.partialSum n (y - x)) f atTop (insert x s ∩ Metric.ball x (↑r' : ℝ))
have h₁ : f = (fun (y : E) ↦ f (x + y)) ∘ fun (y : E) ↦ y - x
Tactic: convert! (hf.tendstoUniformlyOn h).comp fun y => y - x using 1
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
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
⊢ TendstoUniformlyOn (fun (n : ℕ) (y : E) ↦ p.partialSum n (y - x)) f atTop (insert x s ∩ Metric.ball x (↑r' : ℝ))
have 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' : ℝ))
Tactic: convert! (hf.tendstoUniformlyOn h).comp fun y => y - x using 1
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
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
⊢ 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' : ℝ))
have 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
Tactic: ext z
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (hypothesis)
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 : HasFPowerSeriesOnBall f p x r
h : (↑r' : ℝ≥0∞) < r
⊢ TendstoUniformlyOn (fun (n : ℕ) (y : E) ↦ p.partialSum n (y - x)) f atTop (Metric.ball x (↑r' : ℝ))
have hf₁ : HasFPowerSeriesWithinOnBall f p univ x r
Tactic: rw [← hasFPowerSeriesWithinOnBall_univ] at hf
Cleared hypotheses: hf, h
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (hypothesis)
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
⊢ TendstoLocallyUniformlyOn (fun (n : ℕ) (y : E) ↦ p.partialSum n (y - x)) f atTop (insert x s ∩ Metric.eball x r)
have A : 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
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
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 (fun (n : ℕ) (y : E) ↦ p.partialSum n (y - x)) f atTop (insert x s ∩ Metric.eball x r)
have h : f = (fun (y : E) ↦ f (x + y)) ∘ fun (y : E) ↦ y - x
Tactic: convert! hf.tendstoLocallyUniformlyOn.comp (fun y : E => y - x) _ A using 1
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
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
⊢ TendstoLocallyUniformlyOn (fun (n : ℕ) (y : E) ↦ p.partialSum n (y - x)) f atTop (insert x s ∩ Metric.eball x r)
have 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)
Tactic: convert! hf.tendstoLocallyUniformlyOn.comp (fun y : E => y - x) _ A using 1
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
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)
⊢ f = (fun (y : E) ↦ f (x + y)) ∘ fun (y : E) ↦ y - x
have h : ∀ (z : E), f z = ((fun (y : E) ↦ f (x + y)) ∘ fun (y : E) ↦ y - x) z
Tactic: ext z
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (hypothesis)
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
⊢ TendstoLocallyUniformlyOn (fun (n : ℕ) (y : E) ↦ p.partialSum n (y - x)) f atTop (Metric.eball x r)
have hf₁ : HasFPowerSeriesWithinOnBall f p univ x r
Tactic: rw [← hasFPowerSeriesWithinOnBall_univ] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (hypothesis)
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
⊢ ContinuousOn f (Metric.eball x r)
have hf₁ : HasFPowerSeriesWithinOnBall f p univ x r
Tactic: rw [← hasFPowerSeriesWithinOnBall_univ] at hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
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 (insert x s) x
have apply : insert x s ∩ Metric.eball x r ∈ 𝓝[insert x s] x
Tactic: apply (hf.continuousOn.continuousWithinAt (x := x) (by simp [hf.r_pos])).mono_of_mem_nhdsWithin
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
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 (insert x s) x
have rcases : ∀ (r : ℝ≥0∞) (hr : HasFPowerSeriesWithinOnBall f p s x r), ContinuousWithinAt f (insert x s) x
Tactic: rcases hf with ⟨r, hr⟩
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
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
⊢ ∀ᶠ (y : E) in 𝓝 x, ContinuousAt f y
have rcases : ∀ (g : FormalMultilinearSeries 𝕜 E F) (r : ℝ≥0∞) (hg : HasFPowerSeriesOnBall f g x r),
  ∀ᶠ (y : E) in 𝓝 x, ContinuousAt f y
Tactic: rcases hf with ⟨g, r, hg⟩
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (hypothesis)
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
⊢ ∀ᶠ (y : E) in 𝓝 x, ContinuousAt f y
have this : Metric.eball x r ∈ 𝓝 x
Tactic: have : Metric.eball x r ∈ 𝓝 x := Metric.eball_mem_nhds _ hg.r_pos
-- Lean 4 proof step from Mathlib.Analysis.Analytic.Basic (goal)
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) in 𝓝 x, ContinuousAt f y
have h : ∀ (y : E) (hy : y ∈ Metric.eball x r), ContinuousAt f y
Tactic: filter_upwards [this] with y hy