awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Analytic.Within
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
y : E
lt : edist y 0 < r
⊢ edist y 0 < p.radius

Tactic:
exact lt_of_lt_of_le lt h.r_le

Premises used: HasFPowerSeriesWithinOnBall.r_le, lt_of_lt_of_le
-- Module: Mathlib.Analysis.Analytic.Within
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
g : E → F
hfg : EqOn f g (insert x s ∩ eball x r)
hg : HasFPowerSeriesOnBall g p x r
⊢ HasFPowerSeriesWithinOnBall f p s x r

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

Premises used: HasFPowerSeriesWithinOnBall.mk, HasFPowerSeriesOnBall.r_le, HasFPowerSeriesOnBall.r_pos
-- Module: Mathlib.Analysis.Analytic.Within
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
g : E → F
hfg : EqOn f g (insert x s ∩ eball x r)
hg : HasFPowerSeriesOnBall g p x r
mpr :
  ∀ {y : E},
    x + y ∈ insert x s →
      Membership.mem (γ := Set E) (eball 0 r) y →
        HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y) (f (x + y))
⊢ HasFPowerSeriesWithinOnBall f p s x r

Tactic:
refine ⟨hg.r_le, hg.r_pos, ?_⟩
-- Module: Mathlib.Analysis.Analytic.Within
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
g : E → F
hfg : EqOn f g (insert x s ∩ eball x r)
hg : HasFPowerSeriesOnBall g p x r
y : E
ys : x + y ∈ insert x s
lt : Membership.mem (γ := Set E) (eball 0 r) y
mpr : HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y) (g (x + y))
mpr₁ : x + y ∈ insert x s ∩ eball x r
⊢ HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y) (f (x + y))

Tactic:
rw [hfg]
-- Module: Mathlib.Analysis.Analytic.Within
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
g : E → F
hfg : EqOn f g (insert x s ∩ eball x r)
hg : HasFPowerSeriesOnBall g p x r
y : E
ys : x + y ∈ insert x s
lt : Membership.mem (γ := Set E) (eball 0 r) y
⊢ HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y) (g (x + y))

Tactic:
hg.hasSum lt

Premises used: HasFPowerSeriesOnBall.hasSum
-- Module: Mathlib.Analysis.Analytic.Within
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
g : E → F
hfg : EqOn f g (insert x s ∩ eball x r)
hg : HasFPowerSeriesOnBall g p x r
y : E
ys : x + y ∈ insert x s
lt : Membership.mem (γ := Set E) (eball 0 r) y
⊢ HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y) (g (x + y))

Tactic:
exact hg.hasSum lt

Premises used: HasFPowerSeriesOnBall.hasSum
-- Module: Mathlib.Analysis.Analytic.Within
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
g : E → F
hfg : EqOn f g (insert x s ∩ eball x r)
hg : HasFPowerSeriesOnBall g p x r
y : E
ys : x + y ∈ insert x s
lt : Membership.mem (γ := Set E) (eball 0 r) y
⊢ x + y ∈ insert x s ∩ eball x r

Tactic:
⟨ys, ?_⟩

Premises used: Set.Mem, setOf, Set.inter, And.intro
-- Module: Mathlib.Analysis.Analytic.Within
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
g : E → F
hfg : EqOn f g (insert x s ∩ eball x r)
hg : HasFPowerSeriesOnBall g p x r
y : E
ys : x + y ∈ insert x s
lt : Membership.mem (γ := Set E) (eball 0 r) y
mpr : x + y ∈ eball x r
⊢ x + y ∈ insert x s ∩ eball x r

Tactic:
refine ⟨ys, ?_⟩
-- Module: Mathlib.Analysis.Analytic.Within
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
g : E → F
hfg : EqOn f g (insert x s ∩ eball x r)
hg : HasFPowerSeriesOnBall g p x r
y : E
ys : x + y ∈ insert x s
lt : Membership.mem (γ := Set E) (eball 0 r) y
⊢ x + y ∈ eball x r

Tactic:
simpa only [mem_eball, edist_eq_enorm_sub, add_sub_cancel_left, sub_zero] using lt

Premises used: edist_eq_enorm_sub, sub_zero, add_sub_cancel_left, Metric.mem_eball
-- Module: Mathlib.Analysis.Analytic.Within
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
mp : HasFPowerSeriesWithinAt f p s x → ∃ (g : E → F), f =ᶠ[𝓝[insert x s] x] g ∧ HasFPowerSeriesAt g p x
mpr : (∃ (g : E → F), f =ᶠ[𝓝[insert x s] x] g ∧ HasFPowerSeriesAt g p x) → HasFPowerSeriesWithinAt f p s x
⊢ HasFPowerSeriesWithinAt f p s x ↔ ∃ (g : E → F), f =ᶠ[𝓝[insert x s] x] g ∧ HasFPowerSeriesAt g p x

Tactic:
constructor
-- Module: Mathlib.Analysis.Analytic.Within
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p s x r
mp :
  ∀ (g : E → F) (e : EqOn f g (insert x s ∩ eball x r)) (h : HasFPowerSeriesOnBall g p x r),
    ∃ (g : E → F), f =ᶠ[𝓝[insert x s] x] g ∧ HasFPowerSeriesAt g p x
⊢ ∃ (g : E → F), f =ᶠ[𝓝[insert x s] x] g ∧ HasFPowerSeriesAt g p x

Tactic:
rcases hasFPowerSeriesWithinOnBall_iff_exists_hasFPowerSeriesOnBall.mp h with ⟨g, e, h⟩

Premises used: hasFPowerSeriesWithinOnBall_iff_exists_hasFPowerSeriesOnBall, Iff.mp
-- Module: Mathlib.Analysis.Analytic.Within
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h_1 : HasFPowerSeriesWithinOnBall f p s x r
g : E → F
e : EqOn f g (insert x s ∩ eball x r)
h : HasFPowerSeriesOnBall g p x r
⊢ ∃ (g : E → F), f =ᶠ[𝓝[insert x s] x] g ∧ HasFPowerSeriesAt g p x

Tactic:
⟨g, ?_, ⟨r, h⟩⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Analysis.Analytic.Within
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h_1 : HasFPowerSeriesWithinOnBall f p s x r
g : E → F
e : EqOn f g (insert x s ∩ eball x r)
h : HasFPowerSeriesOnBall g p x r
mp : f =ᶠ[𝓝[insert x s] x] g
⊢ ∃ (g : E → F), f =ᶠ[𝓝[insert x s] x] g ∧ HasFPowerSeriesAt g p x

Tactic:
refine ⟨g, ?_, ⟨r, h⟩⟩
-- Module: Mathlib.Analysis.Analytic.Within
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h_1 : HasFPowerSeriesWithinOnBall f p s x r
g : E → F
e : EqOn f g (insert x s ∩ eball x r)
h : HasFPowerSeriesOnBall g p x r
⊢ f =ᶠ[𝓝[insert x s] x] g

Tactic:
Filter.eventuallyEq_iff_exists_mem.mpr ⟨_, ?_, e⟩

Premises used: Iff.mpr, And.intro, Exists.intro, Filter.eventuallyEq_iff_exists_mem
-- Module: Mathlib.Analysis.Analytic.Within
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h_1 : HasFPowerSeriesWithinOnBall f p s x r
g : E → F
e : EqOn f g (insert x s ∩ eball x r)
h : HasFPowerSeriesOnBall g p x r
mp : insert x s ∩ eball x r ∈ 𝓝[insert x s] x
⊢ f =ᶠ[𝓝[insert x s] x] g

Tactic:
refine Filter.eventuallyEq_iff_exists_mem.mpr ⟨_, ?_, e⟩

Premises used: Iff.mpr, And.intro, Exists.intro, Filter.eventuallyEq_iff_exists_mem
-- Module: Mathlib.Analysis.Analytic.Within
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h_1 : HasFPowerSeriesWithinOnBall f p s x r
g : E → F
e : EqOn f g (insert x s ∩ eball x r)
h : HasFPowerSeriesOnBall g p x r
⊢ insert x s ∩ eball x r ∈ 𝓝[insert x s] x

Tactic:
inter_mem_nhdsWithin _ (eball_mem_nhds _ h.r_pos)

Premises used: inter_mem_nhdsWithin, Metric.eball_mem_nhds, HasFPowerSeriesOnBall.r_pos
-- Module: Mathlib.Analysis.Analytic.Within
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
h_1 : HasFPowerSeriesWithinOnBall f p s x r
g : E → F
e : EqOn f g (insert x s ∩ eball x r)
h : HasFPowerSeriesOnBall g p x r
⊢ insert x s ∩ eball x r ∈ 𝓝[insert x s] x

Tactic:
exact inter_mem_nhdsWithin _ (eball_mem_nhds _ h.r_pos)

Premises used: inter_mem_nhdsWithin, Metric.eball_mem_nhds, HasFPowerSeriesOnBall.r_pos
-- Module: Mathlib.Analysis.Analytic.Within
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
g : E → F
hfg : f =ᶠ[𝓝[insert x s] x] g
r : ℝ≥0∞
hg : HasFPowerSeriesOnBall g p x r
⊢ ∃ ε > 0, ∀ ⦃y : E⦄, dist y x < ε → y ∈ insert x s → f y = g y

Tactic:
simp only [eventuallyEq_nhdsWithin_iff, Metric.eventually_nhds_iff] at hfg

Premises used: Metric.eventually_nhds_iff, eventuallyEq_nhdsWithin_iff
-- Module: Mathlib.Analysis.Analytic.Within
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
g : E → F
r : ℝ≥0∞
hg : HasFPowerSeriesOnBall g p x r
hfg : ∃ ε > 0, ∀ ⦃y : E⦄, dist y x < ε → y ∈ insert x s → f y = g y
mpr :
  ∀ (e : ℝ) (e0 : e > 0) (hfg : ∀ ⦃y : E⦄, dist y x < e → y ∈ insert x s → f y = g y), HasFPowerSeriesWithinAt f p s x
⊢ HasFPowerSeriesWithinAt f p s x

Tactic:
rcases hfg with ⟨e, e0, hfg⟩
-- Module: Mathlib.Analysis.Analytic.Within
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
g : E → F
r : ℝ≥0∞
hg : HasFPowerSeriesOnBall g p x r
e : ℝ
e0 : e > 0
hfg : ∀ ⦃y : E⦄, dist y x < e → y ∈ insert x s → f y = g y
⊢ HasFPowerSeriesWithinAt f p s x

Tactic:
⟨min r (.ofReal e), ?_⟩

Premises used: ENNReal.ofReal, HasFPowerSeriesWithinAt, Exists.intro, Min.min
-- Module: Mathlib.Analysis.Analytic.Within
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
g : E → F
r : ℝ≥0∞
hg : HasFPowerSeriesOnBall g p x r
e : ℝ
e0 : e > 0
hfg : ∀ ⦃y : E⦄, dist y x < e → y ∈ insert x s → f y = g y
mpr : HasFPowerSeriesWithinOnBall f p s x (min r (ENNReal.ofReal e))
⊢ HasFPowerSeriesWithinAt f p s x

Tactic:
refine ⟨min r (.ofReal e), ?_⟩
-- Module: Mathlib.Analysis.Analytic.Within
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
g : E → F
r : ℝ≥0∞
hg : HasFPowerSeriesOnBall g p x r
e : ℝ
e0 : e > 0
hfg : ∀ ⦃y : E⦄, dist y x < e → y ∈ insert x s → f y = g y
⊢ HasFPowerSeriesWithinOnBall f p s x (min r (ENNReal.ofReal e))

Tactic:
hasFPowerSeriesWithinOnBall_iff_exists_hasFPowerSeriesOnBall.mpr ⟨g, ?_, ?_⟩

Premises used: Iff.mpr, hasFPowerSeriesWithinOnBall_iff_exists_hasFPowerSeriesOnBall, And.intro, Exists.intro
-- Module: Mathlib.Analysis.Analytic.Within
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
g : E → F
r : ℝ≥0∞
hg : HasFPowerSeriesOnBall g p x r
e : ℝ
e0 : e > 0
hfg : ∀ ⦃y : E⦄, dist y x < e → y ∈ insert x s → f y = g y
mpr : EqOn f g (insert x s ∩ eball x (min r (ENNReal.ofReal e)))
mpr₁ : HasFPowerSeriesOnBall g p x (min r (ENNReal.ofReal e))
⊢ HasFPowerSeriesWithinOnBall f p s x (min r (ENNReal.ofReal e))

Tactic:
refine hasFPowerSeriesWithinOnBall_iff_exists_hasFPowerSeriesOnBall.mpr ⟨g, ?_, ?_⟩

Premises used: Iff.mpr, hasFPowerSeriesWithinOnBall_iff_exists_hasFPowerSeriesOnBall, And.intro, Exists.intro
-- Module: Mathlib.Analysis.Analytic.Within
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
g : E → F
r : ℝ≥0∞
hg : HasFPowerSeriesOnBall g p x r
e : ℝ
e0 : e > 0
hfg : ∀ ⦃y : E⦄, dist y x < e → y ∈ insert x s → f y = g y
y : E
mpr : ∀ (ys : y ∈ insert x s) (xy : y ∈ eball x (min r (ENNReal.ofReal e))), f y = g y
⊢ y ∈ insert x s ∩ eball x (min r (ENNReal.ofReal e)) → f y = g y

Tactic:
⟨ys, xy⟩
-- Module: Mathlib.Analysis.Analytic.Within
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
g : E → F
r : ℝ≥0∞
hg : HasFPowerSeriesOnBall g p x r
e : ℝ
e0 : e > 0
hfg : ∀ ⦃y : E⦄, dist y x < e → y ∈ insert x s → f y = g y
y : E
ys : y ∈ insert x s
xy : y ∈ eball x (min r (ENNReal.ofReal e))
⊢ f y = g y

Tactic:
hfg ?_ ys
-- Module: Mathlib.Analysis.Analytic.Within
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
g : E → F
r : ℝ≥0∞
hg : HasFPowerSeriesOnBall g p x r
e : ℝ
e0 : e > 0
hfg : ∀ ⦃y : E⦄, dist y x < e → y ∈ insert x s → f y = g y
y : E
ys : y ∈ insert x s
xy : y ∈ eball x (min r (ENNReal.ofReal e))
mpr : dist y x < e
⊢ f y = g y

Tactic:
refine hfg ?_ ys
-- Module: Mathlib.Analysis.Analytic.Within
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
g : E → F
r : ℝ≥0∞
hg : HasFPowerSeriesOnBall g p x r
e : ℝ
e0 : e > 0
hfg : ∀ ⦃y : E⦄, dist y x < e → y ∈ insert x s → f y = g y
y : E
ys : y ∈ insert x s
xy : y ∈ eball x (min r (ENNReal.ofReal e))
⊢ edist y x < r ∧ dist y x < e

Tactic:
simp only [mem_eball, lt_min_iff, edist_lt_ofReal] at xy

Premises used: edist_lt_ofReal, lt_min_iff, Metric.mem_eball
-- Module: Mathlib.Analysis.Analytic.Within
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
g : E → F
r : ℝ≥0∞
hg : HasFPowerSeriesOnBall g p x r
e : ℝ
e0 : e > 0
hfg : ∀ ⦃y : E⦄, dist y x < e → y ∈ insert x s → f y = g y
y : E
ys : y ∈ insert x s
xy : edist y x < r ∧ dist y x < e
⊢ dist y x < e

Tactic:
xy.2

Premises used: And.right
-- Module: Mathlib.Analysis.Analytic.Within
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
g : E → F
r : ℝ≥0∞
hg : HasFPowerSeriesOnBall g p x r
e : ℝ
e0 : e > 0
hfg : ∀ ⦃y : E⦄, dist y x < e → y ∈ insert x s → f y = g y
y : E
ys : y ∈ insert x s
xy : edist y x < r ∧ dist y x < e
⊢ dist y x < e

Tactic:
exact xy.2

Premises used: And.right
-- Module: Mathlib.Analysis.Analytic.Within
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
g : E → F
r : ℝ≥0∞
hg : HasFPowerSeriesOnBall g p x r
e : ℝ
e0 : e > 0
hfg : ∀ ⦃y : E⦄, dist y x < e → y ∈ insert x s → f y = g y
⊢ 0 < ENNReal.ofReal e

Tactic:
positivity
-- Module: Mathlib.Analysis.Analytic.Within
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
g : E → F
r : ℝ≥0∞
hg : HasFPowerSeriesOnBall g p x r
e : ℝ
e0 : e > 0
hfg : ∀ ⦃y : E⦄, dist y x < e → y ∈ insert x s → f y = g y
⊢ HasFPowerSeriesOnBall g p x (min r (ENNReal.ofReal e))

Tactic:
exact hg.mono (lt_min hg.r_pos (by positivity)) (min_le_left _ _)

Premises used: lt_min, min_le_left, HasFPowerSeriesOnBall.mono, HasFPowerSeriesOnBall.r_pos
-- Module: Mathlib.Analysis.Analytic.Within
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
s : Set E
x : E
simp :
  (∃ (p : FormalMultilinearSeries 𝕜 E F) (g : E → F), f =ᶠ[𝓝[insert x s] x] g ∧ HasFPowerSeriesAt g p x) ↔
    ∃ (g : E → F), f =ᶠ[𝓝[insert x s] x] g ∧ ∃ (p : FormalMultilinearSeries 𝕜 E F), HasFPowerSeriesAt g p x
⊢ AnalyticWithinAt 𝕜 f s x ↔ ∃ (g : E → F), f =ᶠ[𝓝[insert x s] x] g ∧ AnalyticAt 𝕜 g x

Tactic:
simp only [AnalyticWithinAt, AnalyticAt, hasFPowerSeriesWithinAt_iff_exists_hasFPowerSeriesAt]

Premises used: hasFPowerSeriesWithinAt_iff_exists_hasFPowerSeriesAt, AnalyticWithinAt, AnalyticAt
-- Module: Mathlib.Analysis.Analytic.Within
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
s : Set E
x : E
simp :
  (∃ (g : E → F), f =ᶠ[𝓝[insert x s] x] g ∧ AnalyticAt 𝕜 g x) ↔
    ∃ (g : E → F), f x = g x ∧ EqOn f g (insert x s) ∧ AnalyticAt 𝕜 g x
⊢ AnalyticWithinAt 𝕜 f s x ↔ ∃ (g : E → F), f x = g x ∧ EqOn f g (insert x s) ∧ AnalyticAt 𝕜 g x

Tactic:
simp only [analyticWithinAt_iff_exists_analyticAt]

Premises used: analyticWithinAt_iff_exists_analyticAt
-- Module: Mathlib.Analysis.Analytic.Within
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
s : Set E
x : E
⊢ (∃ (g : E → F), f =ᶠ[𝓝[insert x s] x] g ∧ AnalyticAt 𝕜 g x) ↔
    ∃ (g : E → F), f x = g x ∧ EqOn f g (insert x s) ∧ AnalyticAt 𝕜 g x

Tactic:
⟨?_, ?_⟩

Premises used: Iff.intro
-- Module: Mathlib.Analysis.Analytic.Within
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
s : Set E
x : E
refine_1 :
  (∃ (g : E → F), f =ᶠ[𝓝[insert x s] x] g ∧ AnalyticAt 𝕜 g x) →
    ∃ (g : E → F), f x = g x ∧ EqOn f g (insert x s) ∧ AnalyticAt 𝕜 g x
refine_2 :
  (∃ (g : E → F), f x = g x ∧ EqOn f g (insert x s) ∧ AnalyticAt 𝕜 g x) →
    ∃ (g : E → F), f =ᶠ[𝓝[insert x s] x] g ∧ AnalyticAt 𝕜 g x
⊢ (∃ (g : E → F), f =ᶠ[𝓝[insert x s] x] g ∧ AnalyticAt 𝕜 g x) ↔
    ∃ (g : E → F), f x = g x ∧ EqOn f g (insert x s) ∧ AnalyticAt 𝕜 g x

Tactic:
refine ⟨?_, ?_⟩
-- Module: Mathlib.Analysis.Analytic.Within
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
s : Set E
x : E
g : E → F
hf : f =ᶠ[𝓝[insert x s] x] g
hg : AnalyticAt 𝕜 g x
refine_1 :
  ∀ (u : Set E) (u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u) (xu : x ∈ u)
    (hu : u ∩ insert x s ⊆ {x : E | (fun (x : E) ↦ f x = g x) x}),
    ∃ (g : E → F), f x = g x ∧ EqOn f g (insert x s) ∧ AnalyticAt 𝕜 g x
⊢ ∃ (g : E → F), f x = g x ∧ EqOn f g (insert x s) ∧ AnalyticAt 𝕜 g x

Tactic:
rcases mem_nhdsWithin.1 hf with ⟨u, u_open, xu, hu⟩

Premises used: mem_nhdsWithin, Iff.mp
-- Module: Mathlib.Analysis.Analytic.Within
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
s : Set E
x : E
g : E → F
hf : f =ᶠ[𝓝[insert x s] x] g
hg : AnalyticAt 𝕜 g x
u : Set E
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
hu : u ∩ insert x s ⊆ {x : E | (fun (x : E) ↦ f x = g x) x}
g' : (i : E) → F := u.piecewise (β := fun (i : E) ↦ F) g f
⊢ ∃ (g : E → F), f x = g x ∧ EqOn f g (insert x s) ∧ AnalyticAt 𝕜 g x

Tactic:
⟨g', ?_, ?_, ?_⟩

Premises used: And.intro, Exists.intro
-- Module: Mathlib.Analysis.Analytic.Within
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
F : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : CompleteSpace F
f : E → F
s : Set E
x : E
g : E → F
hf : f =ᶠ[𝓝[insert x s] x] g
hg : AnalyticAt 𝕜 g x
u : Set E
u_open : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] u
xu : x ∈ u
hu : u ∩ insert x s ⊆ {x : E | (fun (x : E) ↦ f x = g x) x}
g' : (i : E) → F := u.piecewise (β := fun (i : E) ↦ F) g f
refine_1 : f x = g' x
refine_1₁ : EqOn f g' (insert x s)
refine_1₂ : AnalyticAt 𝕜 g' x
⊢ ∃ (g : E → F), f x = g x ∧ EqOn f g (insert x s) ∧ AnalyticAt 𝕜 g x

Tactic:
refine ⟨g', ?_, ?_, ?_⟩