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
s : Set E
hf : AnalyticOnNhd 𝕜 f s
y x : E
hx : x + -y ∈ s
⊢ AnalyticAt.{u_1, u_2, u_3} 𝕜 (F := F) (fun (z : E) ↦ f (z - y)) (x - y + y)

Tactic:
apply (hf (x - y) (by convert! hx using 1; abel)).comp_sub

Premises used: HSub.hSub, AnalyticAt.comp_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
s : Set E
x : E
hf : AnalyticWithinAt 𝕜 f s x
y : E
obtain :
  ∀ (p : FormalMultilinearSeries 𝕜 E F) (hf : HasFPowerSeriesWithinAt f p s x),
    AnalyticWithinAt.{u_1, u_2, u_3} 𝕜 (F := F) (fun (z : E) ↦ f (z - y)) (s + {y}) (x + y)
⊢ AnalyticWithinAt.{u_1, u_2, u_3} 𝕜 (F := F) (fun (z : E) ↦ f (z - y)) (s + {y}) (x + y)

Tactic:
obtain ⟨p, hf⟩ := 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
s : Set E
x y : E
p : FormalMultilinearSeries 𝕜 E F
hf : HasFPowerSeriesWithinAt f p s x
⊢ AnalyticWithinAt.{u_1, u_2, u_3} 𝕜 (F := F) (fun (z : E) ↦ f (z - y)) (s + {y}) (x + y)

Tactic:
⟨p, hf.comp_sub _⟩

Premises used: HasFPowerSeriesWithinAt.comp_sub, AnalyticWithinAt, 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
s : Set E
x y : E
p : FormalMultilinearSeries 𝕜 E F
hf : HasFPowerSeriesWithinAt f p s x
⊢ AnalyticWithinAt.{u_1, u_2, u_3} 𝕜 (F := F) (fun (z : E) ↦ f (z - y)) (s + {y}) (x + y)

Tactic:
exact ⟨p, hf.comp_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
s : Set E
hf : AnalyticOn 𝕜 f s
y x : E
hx : x ∈ s + {y}
⊢ x + -y ∈ s

Tactic:
simp only [add_singleton, image_add_right, mem_preimage] at hx

Premises used: Set.image_add_right, Set.add_singleton, Set.mem_preimage
-- Module: Mathlib.Analysis.Analytic.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
hf : AnalyticOn 𝕜 f s
y x : E
hx : x + -y ∈ s
⊢ x = x - y + y

Tactic:
abel
-- Module: Mathlib.Analysis.Analytic.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
hf : AnalyticOn 𝕜 f s
y x : E
hx : x + -y ∈ s
rw : AnalyticWithinAt.{u_1, u_2, u_3} 𝕜 (F := F) (fun (z : E) ↦ f (z - y)) (s + {y}) (x - y + y)
⊢ AnalyticWithinAt.{u_1, u_2, u_3} 𝕜 (F := F) (fun (z : E) ↦ f (z - y)) (s + {y}) x

Tactic:
rw [show x = (x - y) + y by abel]
-- Module: Mathlib.Analysis.Analytic.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
hf : AnalyticOn 𝕜 f s
y x : E
hx : x + -y ∈ s
⊢ x + -y ∈ s

Tactic:
hx
-- Module: Mathlib.Analysis.Analytic.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
hf : AnalyticOn 𝕜 f s
y x : E
hx : x + -y ∈ s
h : x - y = x + -y
⊢ x - y ∈ s

Tactic:
convert! hx using 1
-- Module: Mathlib.Analysis.Analytic.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
hf : AnalyticOn 𝕜 f s
y x : E
hx : x + -y ∈ s
⊢ x - y = x + -y

Tactic:
abel
-- Module: Mathlib.Analysis.Analytic.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
hf : AnalyticOn 𝕜 f s
y x : E
hx : x + -y ∈ s
⊢ AnalyticWithinAt.{u_1, u_2, u_3} 𝕜 (F := F) (fun (z : E) ↦ f (z - y)) (s + {y}) (x - y + y)

Tactic:
apply (hf (x - y) (by convert! hx using 1; abel)).comp_sub

Premises used: HSub.hSub, AnalyticWithinAt.comp_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∞
hf : HasFPowerSeriesWithinOnBall f p s x r
y : E
hy : y ∈ insert x s ∩ Metric.eball x r
⊢ Membership.mem (γ := Set E) (Metric.eball 0 r) (y - x)

Tactic:
simpa [edist_eq_enorm_sub] using hy.2

Premises used: edist_eq_enorm_sub, And.right
-- 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 : y ∈ insert x s ∩ Metric.eball x r
⊢ Membership.mem (γ := Set E) (Metric.eball 0 r) (y - x)

Tactic:
have : y - x ∈ Metric.eball 0 r := by simpa [edist_eq_enorm_sub] using hy.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∞
hf : HasFPowerSeriesWithinOnBall f p s x r
y : E
hy : y ∈ insert x s ∩ Metric.eball x r
this : Membership.mem (γ := Set E) (Metric.eball 0 r) (y - x)
⊢ x + (y - x) ∈ insert x s

Tactic:
simpa only [add_sub_cancel] using hy.1

Premises used: add_sub_cancel, And.left
-- 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 : y ∈ insert x s ∩ Metric.eball x r
this : Membership.mem (γ := Set E) (Metric.eball 0 r) (y - x)
⊢ HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ y - x) (f y)

Tactic:
simpa only [add_sub_cancel] using hf.hasSum (by simpa only [add_sub_cancel] using hy.1) this

Premises used: add_sub_cancel, 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 : y ∈ Metric.eball x r
⊢ Membership.mem (γ := Set E) (Metric.eball 0 r) (y - x)

Tactic:
simpa [edist_eq_enorm_sub] using hy

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 : HasFPowerSeriesOnBall f p x r
y : E
hy : y ∈ Metric.eball x r
⊢ Membership.mem (γ := Set E) (Metric.eball 0 r) (y - x)

Tactic:
have : y - x ∈ Metric.eball 0 r := by simpa [edist_eq_enorm_sub] using 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
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
y : E
hy : y ∈ Metric.eball x r
this : Membership.mem (γ := Set E) (Metric.eball 0 r) (y - x)
⊢ HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ y - x) (f y)

Tactic:
simpa only [add_sub_cancel] using hf.hasSum this

Premises used: HasFPowerSeriesOnBall.hasSum, add_sub_cancel
-- 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
⊢ 0 < p.radius

Tactic:
lt_of_lt_of_le hf.r_pos hf.r_le

Premises used: HasFPowerSeriesOnBall.r_le, HasFPowerSeriesOnBall.r_pos, lt_of_lt_of_le
-- 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
⊢ 0 < p.radius

Tactic:
lt_of_lt_of_le hf.r_pos hf.r_le

Premises used: HasFPowerSeriesWithinOnBall.r_le, HasFPowerSeriesWithinOnBall.r_pos, lt_of_lt_of_le
-- 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
⊢ 0 < p.radius

Tactic:
let ⟨_, hr⟩ := hf
  hr.radius_pos

Premises used: FormalMultilinearSeries.radius, HasFPowerSeriesOnBall.radius_pos, LT.lt, _private.0.HasFPowerSeriesAt.radius_pos.match_1, 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 r' : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p s x r
r'_pos : 0 < r'
hr : r' ≤ r
⊢ HasFPowerSeriesWithinOnBall f p s x r'

Tactic:
⟨le_trans hr hf.1, r'_pos, fun hy h'y => hf.hasSum hy (Metric.eball_subset_eball hr h'y)⟩

Premises used: Metric.eball_subset_eball, HasFPowerSeriesWithinOnBall.mk, HasFPowerSeriesWithinOnBall.r_le, HasFPowerSeriesWithinOnBall.hasSum, le_trans
-- 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 : HasFPowerSeriesOnBall f p x r
r'_pos : 0 < r'
hr : r' ≤ r
⊢ HasFPowerSeriesOnBall f p x r'

Tactic:
⟨le_trans hr hf.1, r'_pos, fun hy => hf.hasSum (Metric.eball_subset_eball hr hy)⟩

Premises used: Metric.eball_subset_eball, HasFPowerSeriesOnBall.r_le, HasFPowerSeriesOnBall.hasSum, HasFPowerSeriesOnBall.mk, le_trans
-- 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 g : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : EqOn g f (s ∩ Metric.eball x r)
h'' : g x = f x
⊢ HasFPowerSeriesWithinOnBall g p s x r

Tactic:
⟨h.r_le, h.r_pos, ?_⟩

Premises used: HasFPowerSeriesWithinOnBall.mk, HasFPowerSeriesWithinOnBall.r_le, 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 g : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : EqOn g f (s ∩ Metric.eball x r)
h'' : g x = f x
refine :
  ∀ {y : E},
    x + y ∈ insert x s →
      Membership.mem (γ := Set E) (Metric.eball 0 r) y →
        HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y) (g (x + y))
⊢ HasFPowerSeriesWithinOnBall g p s x r

Tactic:
refine ⟨h.r_le, h.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 g : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : EqOn g f (s ∩ Metric.eball x r)
h'' : g x = f x
y : E
hy : x + y ∈ insert x s
h'y : Membership.mem (γ := Set E) (Metric.eball 0 r) y
⊢ HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y) (f (x + y))

Tactic:
h.hasSum hy h'y

Premises used: 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 g : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : EqOn g f (s ∩ Metric.eball x r)
h'' : g x = f x
y : E
hy : x + y ∈ insert x s
h'y : Membership.mem (γ := Set E) (Metric.eball 0 r) y
h₁ : g (x + y) = f (x + y)
⊢ HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y) (g (x + y))

Tactic:
convert! h.hasSum hy h'y using 1

Premises used: 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 g : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : EqOn g f (s ∩ Metric.eball x r)
h'' : g x = f x
y : E
hy : x + y ∈ insert x s
h'y : Membership.mem (γ := Set E) (Metric.eball 0 r) y
⊢ y = 0 ∨ x + y ∈ s

Tactic:
simp only [mem_insert_iff, add_eq_left] at hy

Premises used: add_eq_left, Set.mem_insert_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 g : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : EqOn g f (s ∩ Metric.eball x r)
h'' : g x = f x
y : E
h'y : Membership.mem (γ := Set E) (Metric.eball 0 r) y
hy : y = 0 ∨ x + y ∈ s
h₁ : ∀ (h'y : Membership.mem (γ := Set E) (Metric.eball 0 r) 0), g (x + 0) = f (x + 0)
h₂ : ∀ (hy : x + y ∈ s), g (x + y) = f (x + y)
⊢ g (x + y) = f (x + y)

Tactic:
rcases hy with rfl | hy

Premises used: rfl
-- 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 g : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : EqOn g f (s ∩ Metric.eball x r)
h'' : g x = f x
h'y : Membership.mem (γ := Set E) (Metric.eball 0 r) 0
⊢ g (x + 0) = f (x + 0)

Tactic:
simpa using h''
-- 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 g : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : EqOn g f (s ∩ Metric.eball x r)
h'' : g x = f x
y : E
h'y : Membership.mem (γ := Set E) (Metric.eball 0 r) y
hy : x + y ∈ s
h₁ : x + y ∈ s ∩ Metric.eball x r
⊢ g (x + y) = f (x + y)

Tactic:
apply h'
-- 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 g : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : EqOn g f (s ∩ Metric.eball x r)
h'' : g x = f x
y : E
h'y : Membership.mem (γ := Set E) (Metric.eball 0 r) y
hy : x + y ∈ s
⊢ x + y ∈ s ∩ Metric.eball x r

Tactic:
⟨hy, ?_⟩

Premises used: Set.Mem, setOf, Set.inter, And.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 g : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : EqOn g f (s ∩ Metric.eball x r)
h'' : g x = f x
y : E
h'y : Membership.mem (γ := Set E) (Metric.eball 0 r) y
hy : x + y ∈ s
h₁ : x + y ∈ Metric.eball x r
⊢ x + y ∈ s ∩ Metric.eball x r

Tactic:
refine ⟨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 g : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : EqOn g f (s ∩ Metric.eball x r)
h'' : g x = f x
y : E
h'y : Membership.mem (γ := Set E) (Metric.eball 0 r) y
hy : x + y ∈ s
⊢ x + y ∈ Metric.eball x r

Tactic:
simpa [edist_eq_enorm_sub] using h'y

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 g : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : EqOn g f (insert x s ∩ Metric.eball x r)
⊢ HasFPowerSeriesWithinOnBall g p s x r

Tactic:
⟨h.r_le, h.r_pos, fun {y} hy h'y ↦ ?_⟩

Premises used: HasFPowerSeriesWithinOnBall.mk, HasFPowerSeriesWithinOnBall.r_le, 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 g : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : EqOn g f (insert x s ∩ Metric.eball x r)
refine :
  ∀ {y : E} (hy : x + y ∈ insert x s) (h'y : Membership.mem (γ := Set E) (Metric.eball 0 r) y),
    HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y) (g (x + y))
⊢ HasFPowerSeriesWithinOnBall g p s x r

Tactic:
refine ⟨h.r_le, h.r_pos, fun {y} hy h'y ↦ ?_⟩
-- 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 g : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : EqOn g f (insert x s ∩ Metric.eball x r)
y : E
hy : x + y ∈ insert x s
h'y : Membership.mem (γ := Set E) (Metric.eball 0 r) y
⊢ HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y) (f (x + y))

Tactic:
h.hasSum hy h'y

Premises used: 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 g : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : EqOn g f (insert x s ∩ Metric.eball x r)
y : E
hy : x + y ∈ insert x s
h'y : Membership.mem (γ := Set E) (Metric.eball 0 r) y
h₁ : g (x + y) = f (x + y)
⊢ HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y) (g (x + y))

Tactic:
convert! h.hasSum hy h'y using 1

Premises used: 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 g : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : EqOn g f (insert x s ∩ Metric.eball x r)
y : E
hy : x + y ∈ insert x s
h'y : Membership.mem (γ := Set E) (Metric.eball 0 r) y
⊢ x + y ∈ Metric.eball x r

Tactic:
simpa [edist_eq_enorm_sub] using h'y

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 g : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
h' : EqOn g f (insert x s ∩ Metric.eball x r)
y : E
hy : x + y ∈ insert x s
h'y : Membership.mem (γ := Set E) (Metric.eball 0 r) y
⊢ g (x + y) = f (x + y)

Tactic:
exact h' ⟨hy, by simpa [edist_eq_enorm_sub] using h'y⟩

Premises used: And.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 g : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
h : HasFPowerSeriesWithinAt f p s x
h' : g =ᶠ[𝓝[s] x] f
h'' : g x = f x
rcases : ∀ (r : ℝ≥0∞) (hr : HasFPowerSeriesWithinOnBall f p s x r), HasFPowerSeriesWithinAt g p s x
⊢ HasFPowerSeriesWithinAt g p s x

Tactic:
rcases h 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 g : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
h' : g =ᶠ[𝓝[s] x] f
h'' : g x = f x
r : ℝ≥0∞
hr : HasFPowerSeriesWithinOnBall f p s x r
⊢ ∃ ε > 0, Metric.eball x ε ∩ s ⊆ {y : E | g y = f y}

Tactic:
EMetric.mem_nhdsWithin_iff.1 h'

Premises used: Iff.mp, EMetric.mem_nhdsWithin_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 g : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
h' : g =ᶠ[𝓝[s] x] f
h'' : g x = f x
r : ℝ≥0∞
hr : HasFPowerSeriesWithinOnBall f p s x r
obtain : ∀ (ε : ℝ≥0∞) (εpos : ε > 0) (hε : Metric.eball x ε ∩ s ⊆ {y : E | g y = f y}), HasFPowerSeriesWithinAt g p s x
⊢ HasFPowerSeriesWithinAt g p s x

Tactic:
obtain ⟨ε, εpos, hε⟩ : ∃ ε > 0, Metric.eball x ε ∩ s ⊆ {y | g y = f y} :=
    EMetric.mem_nhdsWithin_iff.1 h'

Premises used: Iff.mp, EMetric.mem_nhdsWithin_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 g : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
h' : g =ᶠ[𝓝[s] x] f
h'' : g x = f x
r : ℝ≥0∞
hr : HasFPowerSeriesWithinOnBall f p s x r
ε : ℝ≥0∞
εpos : ε > 0
hε : Metric.eball x ε ∩ s ⊆ {y : E | g y = f y}
r' : ℝ≥0∞ := min r ε
⊢ HasFPowerSeriesWithinAt g p s x

Tactic:
⟨r', ?_⟩

Premises used: HasFPowerSeriesWithinAt, Exists.intro