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 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 ε
refine : HasFPowerSeriesWithinOnBall g p s x r'
⊢ HasFPowerSeriesWithinAt g p s x

Tactic:
refine ⟨r', ?_⟩
-- Module: Mathlib.Analysis.Analytic.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f 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 ε
⊢ 0 < r'

Tactic:
simp [r', εpos, hr.r_pos]

Premises used: HasFPowerSeriesWithinOnBall.r_pos
-- Module: Mathlib.Analysis.Analytic.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f 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 ε
⊢ HasFPowerSeriesWithinOnBall f p s x r'

Tactic:
have := hr.of_le (r' := r') (by simp [r', εpos, hr.r_pos]) (min_le_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 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 ε
this : HasFPowerSeriesWithinOnBall f p s x r'
apply : EqOn g f (s ∩ Metric.eball x r')
⊢ HasFPowerSeriesWithinOnBall g p s x r'

Tactic:
apply this.congr _ h''

Premises used: HasFPowerSeriesWithinOnBall.congr
-- 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 ε
this : HasFPowerSeriesWithinOnBall f p s x r'
z : E
hz : z ∈ s ∩ Metric.eball x r'
⊢ g z = f z

Tactic:
hε ⟨Metric.eball_subset_eball (min_le_right _ _) hz.2, hz.1⟩

Premises used: Metric.eball_subset_eball, Set.Mem, setOf, And.right, And.left, And.intro, min_le_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 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 ε
this : HasFPowerSeriesWithinOnBall f p s x r'
z : E
hz : z ∈ s ∩ Metric.eball x r'
⊢ g z = f z

Tactic:
exact hε ⟨Metric.eball_subset_eball (min_le_right _ _) hz.2, hz.1⟩

Premises used: Metric.eball_subset_eball, And.right, And.left, And.intro, min_le_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 g : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
hg : EqOn f g (Metric.eball x r)
y : E
hy : 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:
hf.hasSum hy

Premises used: HasFPowerSeriesOnBall.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
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
hg : EqOn f g (Metric.eball x r)
y : E
hy : 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! hf.hasSum hy using 1

Premises used: HasFPowerSeriesOnBall.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
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
hg : EqOn f g (Metric.eball x r)
y : E
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
h : x + y ∈ Metric.eball x r
⊢ g (x + y) = f (x + y)

Tactic:
apply hg.symm

Premises used: Set.EqOn.symm
-- 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
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
hg : EqOn f g (Metric.eball x r)
y : E
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
⊢ x + y ∈ Metric.eball x r

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 g : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
hf : HasFPowerSeriesAt f p x
hg : f =ᶠ[𝓝 x] g
rcases : ∀ (r₁ : ℝ≥0∞) (h₁ : HasFPowerSeriesOnBall f p x r₁), HasFPowerSeriesAt g p x
⊢ HasFPowerSeriesAt g p x

Tactic:
rcases hf with ⟨r₁, 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
x : E
hg : f =ᶠ[𝓝 x] g
r₁ : ℝ≥0∞
h₁ : HasFPowerSeriesOnBall f p x r₁
rcases :
  ∀ (r₂ : ℝ≥0∞) (h₂pos : r₂ > 0) (h₂ : Metric.eball x r₂ ⊆ {x : E | (fun (x : E) ↦ f x = g x) x}),
    HasFPowerSeriesAt g p x
⊢ HasFPowerSeriesAt g p x

Tactic:
rcases EMetric.mem_nhds_iff.mp hg with ⟨r₂, h₂pos, h₂⟩

Premises used: EMetric.mem_nhds_iff, Iff.mp
-- Module: Mathlib.Analysis.Analytic.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f g : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
hg : f =ᶠ[𝓝 x] g
r₁ : ℝ≥0∞
h₁ : HasFPowerSeriesOnBall f p x r₁
r₂ : ℝ≥0∞
h₂pos : r₂ > 0
h₂ : Metric.eball x r₂ ⊆ {x : E | (fun (x : E) ↦ f x = g x) x}
⊢ HasFPowerSeriesAt g p x

Tactic:
⟨min r₁ r₂,
    (h₁.mono (lt_min h₁.r_pos h₂pos) inf_le_left).congr
      fun y hy => h₂ (Metric.eball_subset_eball inf_le_right hy)⟩

Premises used: HasFPowerSeriesOnBall.congr, Metric.eball_subset_eball, inf_le_right, lt_min, Exists.intro, inf_le_left, HasFPowerSeriesAt, HasFPowerSeriesOnBall.mono, HasFPowerSeriesOnBall.r_pos, Min.min
-- 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
x : E
hg : f =ᶠ[𝓝 x] g
r₁ : ℝ≥0∞
h₁ : HasFPowerSeriesOnBall f p x r₁
r₂ : ℝ≥0∞
h₂pos : r₂ > 0
h₂ : Metric.eball x r₂ ⊆ {x : E | (fun (x : E) ↦ f x = g x) x}
⊢ HasFPowerSeriesAt g p x

Tactic:
exact ⟨min r₁ r₂,
    (h₁.mono (lt_min h₁.r_pos h₂pos) inf_le_left).congr
      fun y hy => h₂ (Metric.eball_subset_eball inf_le_right 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∞
hf : HasFPowerSeriesWithinOnBall f p s x r
hg : HasFPowerSeriesWithinOnBall g p s x r
⊢ EqOn f g (insert x s ∩ Metric.eball x r)

Tactic:
fun _ hy ↦
  (hf.hasSum_sub hy).unique (hg.hasSum_sub hy)

Premises used: HasFPowerSeriesWithinOnBall.hasSum_sub, Set.EqOn, HasSum.unique
-- 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
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
hg : HasFPowerSeriesOnBall g p x r
⊢ EqOn f g (Metric.eball x r)

Tactic:
fun _ hy ↦
  (hf.hasSum_sub hy).unique (hg.hasSum_sub hy)

Premises used: Set.EqOn, HasSum.unique, HasFPowerSeriesOnBall.hasSum_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
hf : HasFPowerSeriesWithinAt f p s x
⊢ ∀ᶠ (r : ℝ≥0∞) in 𝓝[>] 0, HasFPowerSeriesWithinOnBall f p s x r

Tactic:
let ⟨_, hr⟩ := hf
  mem_of_superset (Ioo_mem_nhdsGT hr.r_pos) fun _ hr' => hr.of_le hr'.1 hr'.2.le

Premises used: Set.Ioi, HasFPowerSeriesWithinOnBall, nhdsWithin, Filter.Eventually, LT.lt.le, _private.0.HasFPowerSeriesWithinAt.eventually.match_1, And.right, And.left, HasFPowerSeriesWithinOnBall.r_pos, OfNat.ofNat, HasFPowerSeriesWithinOnBall.of_le, Ioo_mem_nhdsGT, Filter.mem_of_superset
-- Module: Mathlib.Analysis.Analytic.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
hf : HasFPowerSeriesAt f p x
⊢ ∀ᶠ (r : ℝ≥0∞) in 𝓝[>] 0, HasFPowerSeriesOnBall f p x r

Tactic:
let ⟨_, hr⟩ := hf
  mem_of_superset (Ioo_mem_nhdsGT hr.r_pos) fun _ hr' => hr.mono hr'.1 hr'.2.le

Premises used: Set.Ioi, nhdsWithin, Filter.Eventually, LT.lt.le, HasFPowerSeriesOnBall, And.right, And.left, _private.0.HasFPowerSeriesAt.radius_pos.match_1, OfNat.ofNat, HasFPowerSeriesOnBall.mono, Ioo_mem_nhdsGT, HasFPowerSeriesOnBall.r_pos, Filter.mem_of_superset
-- Module: Mathlib.Analysis.Analytic.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
⊢ ∀ (a : E),
    Membership.mem (γ := Set E) (Metric.eball 0 r) a →
      HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ a) (f (x + a))

Tactic:
fun _ => hf.hasSum

Premises used: Set.Mem, HasFPowerSeriesOnBall.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
h :
  ∀ (a : E),
    Membership.mem (γ := Set E)
      {x_1 : E |
        Membership.mem (γ := Set E) (Metric.eball 0 r) x_1 →
          Membership.mem (γ := Set E)
            {x_2 : E |
              (fun (y : E) ↦ HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y) (f (x + y)))
                x_2}
            x_1}
      a
h₁ :
  ∀ (a : E),
    Membership.mem (γ := Set E) (Metric.eball 0 r) a →
      HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ a) (f (x + a))
⊢ ∀ᶠ (y : E) in 𝓝 0, HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y) (f (x + y))

Tactic:
filter_upwards [Metric.eball_mem_nhds (0 : E) hf.r_pos] using fun _ => hf.hasSum

Premises used: HasFPowerSeriesOnBall.hasSum, Metric.eball_mem_nhds, OfNat.ofNat, HasFPowerSeriesOnBall.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
x : E
hf : HasFPowerSeriesAt f p x
⊢ ∀ᶠ (y : E) in 𝓝 0, HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y) (f (x + y))

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

Premises used: Filter.Eventually, nhds, HasFPowerSeriesOnBall.eventually_hasSum, HAdd.hAdd, HasSum, Nat, _private.0.HasFPowerSeriesAt.radius_pos.match_1, OfNat.ofNat, DFunLike.coe, SummationFilter.unconditional
-- 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
⊢ y ∈ Metric.eball x r → HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ y - x) (f y)

Tactic:
hf.hasSum_sub

Premises used: Set.Mem, HasFPowerSeriesOnBall.hasSum_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
h :
  ∀ (a : E),
    Membership.mem (γ := Set E)
      {x_1 : E |
        x_1 ∈ Metric.eball x r →
          Membership.mem (γ := Set E)
            {x_2 : E |
              (fun (y : E) ↦ HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x_3 : Fin n) ↦ y - x) (f y))
                x_2}
            x_1}
      a
h₁ h₂ : ∀ y ∈ Metric.eball x r, HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ y - x) (f y)
⊢ ∀ᶠ (y : E) in 𝓝 x, HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ y - x) (f y)

Tactic:
filter_upwards [Metric.eball_mem_nhds x hf.r_pos] with y using hf.hasSum_sub

Premises used: Metric.eball_mem_nhds, HasFPowerSeriesOnBall.hasSum_sub, HasFPowerSeriesOnBall.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
x : E
hf : HasFPowerSeriesAt f p x
⊢ ∀ᶠ (y : E) in 𝓝 x, HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ y - x) (f y)

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

Premises used: Filter.Eventually, HSub.hSub, nhds, HasSum, Nat, _private.0.HasFPowerSeriesAt.radius_pos.match_1, HasFPowerSeriesOnBall.eventually_hasSum_sub, DFunLike.coe, SummationFilter.unconditional
-- 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
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall.{u_1, u_2, u_3} (𝕜 := 𝕜) f 0 x r
z : E
hz : HasSum (fun (n : ℕ) ↦ (0 n : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ z - x) (f z)
⊢ f z = 0

Tactic:
hz.unique hasSum_zero

Premises used: hasSum_zero, HasSum.unique
-- 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
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall.{u_1, u_2, u_3} (𝕜 := 𝕜) f 0 x r
h :
  ∀ (a : E),
    Membership.mem (γ := Set E)
      {x_1 : E |
        Membership.mem (γ := Set E)
            {x_2 : E |
              (fun (y : E) ↦ HasSum (fun (n : ℕ) ↦ (0 n : (a : (i : Fin n) → E) → F) fun (x_3 : Fin n) ↦ y - x) (f y))
                x_2}
            x_1 →
          Membership.mem (γ := Set E) {x : E | (fun (z : E) ↦ f z = 0) x} x_1}
      a
h₁ h₂ :
  ∀ (z : E) (hz : HasSum (fun (n : ℕ) ↦ (0 n : (a : (i : Fin n) → E) → F) fun (x_1 : Fin n) ↦ z - x) (f z)), f z = 0
⊢ ∀ᶠ (z : E) in 𝓝 x, f z = 0

Tactic:
filter_upwards [hf.eventually_hasSum_sub] with z hz using hz.unique hasSum_zero

Premises used: HasFPowerSeriesOnBall.eventually_hasSum_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
x : E
hf : HasFPowerSeriesAt.{u_1, u_2, u_3} (𝕜 := 𝕜) f 0 x
⊢ ∀ᶠ (z : E) in 𝓝 x, f z = 0

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

Premises used: _private.0.HasFPowerSeriesAt.eventually_eq_zero.match_1, Filter.Eventually, nhds, HasFPowerSeriesOnBall.eventually_eq_zero, OfNat.ofNat, Eq
-- 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∞
mp : HasFPowerSeriesWithinOnBall f p univ x r → HasFPowerSeriesOnBall f p x r
mpr : HasFPowerSeriesOnBall f p x r → HasFPowerSeriesWithinOnBall f p univ x r
⊢ HasFPowerSeriesWithinOnBall f p univ x r ↔ HasFPowerSeriesOnBall f p x r

Tactic:
constructor
-- 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∞
h : HasFPowerSeriesWithinOnBall f p univ x r
y : E
m : Membership.mem (γ := Set E) (Metric.eball 0 r) y
⊢ Membership.mem (γ := Set E) (insert x univ) (x + y)

Tactic:
simp
-- Module: Mathlib.Analysis.Analytic.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
h : HasFPowerSeriesWithinOnBall f p univ x r
⊢ HasFPowerSeriesOnBall f p x r

Tactic:
refine ⟨h.r_le, h.r_pos, fun {y} m ↦ h.hasSum (by simp) m⟩
-- 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∞
h : HasFPowerSeriesOnBall f p x r
⊢ HasFPowerSeriesWithinOnBall f p univ x r

Tactic:
⟨h.r_le, h.r_pos, fun {y} _ m => h.hasSum m⟩

Premises used: HasFPowerSeriesWithinOnBall.mk, HasFPowerSeriesOnBall.r_le, HasFPowerSeriesOnBall.hasSum, HasFPowerSeriesOnBall.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
x : E
r : ℝ≥0∞
h : HasFPowerSeriesOnBall f p x r
⊢ HasFPowerSeriesWithinOnBall f p univ x r

Tactic:
exact ⟨h.r_le, h.r_pos, fun {y} _ m => h.hasSum m⟩
-- 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
⊢ HasFPowerSeriesWithinAt f p univ x ↔ HasFPowerSeriesAt f p x

Tactic:
simp only [HasFPowerSeriesWithinAt, hasFPowerSeriesWithinOnBall_univ, HasFPowerSeriesAt]

Premises used: hasFPowerSeriesWithinOnBall_univ, HasFPowerSeriesWithinAt, HasFPowerSeriesAt
-- 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 : HasFPowerSeriesOnBall f p x r
⊢ HasFPowerSeriesWithinOnBall f p univ x r

Tactic:
rw [← hasFPowerSeriesWithinOnBall_univ] at hf

Premises used: hasFPowerSeriesWithinOnBall_univ
-- Module: Mathlib.Analysis.Analytic.Basic
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f p univ x r
⊢ HasFPowerSeriesWithinOnBall f p s x r

Tactic:
hf.mono (subset_univ _)

Premises used: Set.subset_univ, HasFPowerSeriesWithinOnBall.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 univ x r
⊢ HasFPowerSeriesWithinOnBall f p s x r

Tactic:
exact hf.mono (subset_univ _)

Premises used: Set.subset_univ, HasFPowerSeriesWithinOnBall.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 t : Set E
x : E
hf : HasFPowerSeriesWithinAt f p s x
h : t ⊆ s
obtain : ∀ (r : ℝ≥0∞) (hp : HasFPowerSeriesWithinOnBall f p s x r), HasFPowerSeriesWithinAt f p t x
⊢ HasFPowerSeriesWithinAt f p t x

Tactic:
obtain ⟨r, hp⟩ := 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 t : Set E
x : E
h : t ⊆ s
r : ℝ≥0∞
hp : HasFPowerSeriesWithinOnBall f p s x r
⊢ HasFPowerSeriesWithinAt f p t x

Tactic:
⟨r, hp.mono h⟩

Premises used: HasFPowerSeriesWithinAt, Exists.intro, HasFPowerSeriesWithinOnBall.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 t : Set E
x : E
h : t ⊆ s
r : ℝ≥0∞
hp : HasFPowerSeriesWithinOnBall f p s x r
⊢ HasFPowerSeriesWithinAt f p t x

Tactic:
exact ⟨r, hp.mono 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 : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
hf : HasFPowerSeriesAt f p x
⊢ HasFPowerSeriesWithinAt f p univ x

Tactic:
rw [← hasFPowerSeriesWithinAt_univ] at hf

Premises used: hasFPowerSeriesWithinAt_univ