awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Analytic.CPolynomialDef
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∞
n : ℕ
hf : HasFiniteFPowerSeriesOnBall f p x n r
hg : EqOn f g (Metric.eball x r)
⊢ HasFiniteFPowerSeriesOnBall g p x n r

Tactic:
⟨hf.1.congr hg, hf.finite⟩

Premises used: HasFPowerSeriesOnBall.congr, HasFiniteFPowerSeriesOnBall.mk, HasFiniteFPowerSeriesOnBall.toHasFPowerSeriesOnBall, HasFiniteFPowerSeriesOnBall.finite
-- Module: Mathlib.Analysis.Analytic.CPolynomialDef
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∞
m n : ℕ
h : HasFiniteFPowerSeriesOnBall f p x n r
hmn : n ≤ m
⊢ HasFiniteFPowerSeriesOnBall f p x m r

Tactic:
⟨h.toHasFPowerSeriesOnBall, fun i hi ↦ h.finite i (hmn.trans hi)⟩

Premises used: HasFiniteFPowerSeriesOnBall.mk, HasFiniteFPowerSeriesOnBall.toHasFPowerSeriesOnBall, HasFiniteFPowerSeriesOnBall.finite, LE.le.trans
-- Module: Mathlib.Analysis.Analytic.CPolynomialDef
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
m n : ℕ
h : HasFiniteFPowerSeriesAt f p x n
hmn : n ≤ m
rcases : ∀ (r : ℝ≥0∞) (hr : HasFiniteFPowerSeriesOnBall f p x n r), HasFiniteFPowerSeriesAt f p x m
⊢ HasFiniteFPowerSeriesAt f p x m

Tactic:
rcases h with ⟨r, hr⟩
-- Module: Mathlib.Analysis.Analytic.CPolynomialDef
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
m n : ℕ
hmn : n ≤ m
r : ℝ≥0∞
hr : HasFiniteFPowerSeriesOnBall f p x n r
⊢ HasFiniteFPowerSeriesAt f p x m

Tactic:
⟨r, hr.of_le hmn⟩

Premises used: HasFiniteFPowerSeriesAt, Exists.intro, HasFiniteFPowerSeriesOnBall.of_le
-- Module: Mathlib.Analysis.Analytic.CPolynomialDef
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
m n : ℕ
hmn : n ≤ m
r : ℝ≥0∞
hr : HasFiniteFPowerSeriesOnBall f p x n r
⊢ HasFiniteFPowerSeriesAt f p x m

Tactic:
exact ⟨r, hr.of_le hmn⟩
-- Module: Mathlib.Analysis.Analytic.CPolynomialDef
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∞
n : ℕ
hf : HasFiniteFPowerSeriesOnBall f p x n r
y : E
⊢ HasFiniteFPowerSeriesOnBall (fun (z : E) ↦ f (z - y)) p (x + y) n r

Tactic:
⟨hf.1.comp_sub y, hf.finite⟩

Premises used: HasFPowerSeriesOnBall.comp_sub, HasFiniteFPowerSeriesOnBall.mk, HasFiniteFPowerSeriesOnBall.toHasFPowerSeriesOnBall, HasFiniteFPowerSeriesOnBall.finite
-- Module: Mathlib.Analysis.Analytic.CPolynomialDef
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∞
n : ℕ
hf : HasFiniteFPowerSeriesOnBall f p x n r
r'_pos : 0 < r'
hr : r' ≤ r
⊢ HasFiniteFPowerSeriesOnBall f p x n r'

Tactic:
⟨hf.1.mono r'_pos hr, hf.finite⟩

Premises used: HasFiniteFPowerSeriesOnBall.mk, HasFiniteFPowerSeriesOnBall.toHasFPowerSeriesOnBall, HasFiniteFPowerSeriesOnBall.finite, HasFPowerSeriesOnBall.mono
-- Module: Mathlib.Analysis.Analytic.CPolynomialDef
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
n : ℕ
hf : HasFiniteFPowerSeriesAt f p x n
hg : f =ᶠ[𝓝 x] g
⊢ HasFiniteFPowerSeriesAt g p x n

Tactic:
Exists.imp (fun _ hg ↦ ⟨hg, hf.finite⟩) (hf.hasFPowerSeriesAt.congr hg)

Premises used: HasFiniteFPowerSeriesAt.finite, HasFPowerSeriesAt.congr, HasFiniteFPowerSeriesAt.hasFPowerSeriesAt, HasFiniteFPowerSeriesOnBall.mk, Exists.imp, HasFiniteFPowerSeriesAt
-- Module: Mathlib.Analysis.Analytic.CPolynomialDef
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
n : ℕ
hf : HasFiniteFPowerSeriesAt f p x n
⊢ ∀ᶠ (r : ℝ≥0∞) in 𝓝[>] 0, HasFiniteFPowerSeriesOnBall f p x n r

Tactic:
hf.hasFPowerSeriesAt.eventually.mono fun _ h ↦ ⟨h, hf.finite⟩

Premises used: HasFiniteFPowerSeriesAt.finite, HasFiniteFPowerSeriesAt.hasFPowerSeriesAt, HasFiniteFPowerSeriesOnBall.mk, HasFPowerSeriesAt.eventually, Filter.Eventually.mono
-- Module: Mathlib.Analysis.Analytic.CPolynomialDef
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
x : E
hf : CPolynomialAt 𝕜 f x
hg : f =ᶠ[𝓝 x] g
⊢ CPolynomialAt 𝕜 g x

Tactic:
let ⟨_, _, hpf⟩ := hf
  (hpf.congr hg).cpolynomialAt

Premises used: HasFiniteFPowerSeriesAt.congr, HasFiniteFPowerSeriesAt.cpolynomialAt, CPolynomialAt, _private.0.CPolynomialAt.congr.match_1
-- Module: Mathlib.Analysis.Analytic.CPolynomialDef
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
x : E
h : f =ᶠ[𝓝 x] g
⊢ CPolynomialAt 𝕜 f x ↔ CPolynomialAt 𝕜 g x

Tactic:
⟨fun hf ↦ hf.congr h, fun hg ↦ hg.congr h.symm⟩

Premises used: Iff.intro, CPolynomialAt.congr, Filter.EventuallyEq.symm
-- Module: Mathlib.Analysis.Analytic.CPolynomialDef
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 t : Set E
hf : CPolynomialOn 𝕜 f t
hst : s ⊆ t
⊢ CPolynomialOn 𝕜 f s

Tactic:
fun z hz => hf z (hst hz)

Premises used: CPolynomialOn
-- Module: Mathlib.Analysis.Analytic.CPolynomialDef
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
s : Set E
hf : CPolynomialOn 𝕜 f s
hg : f =ᶠ[𝓝ˢ s] g
⊢ CPolynomialOn 𝕜 g s

Tactic:
fun z hz => (hf z hz).congr (mem_nhdsSet_iff_forall.mp hg z hz)

Premises used: mem_nhdsSet_iff_forall, Iff.mp, CPolynomialAt.congr, CPolynomialOn
-- Module: Mathlib.Analysis.Analytic.CPolynomialDef
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
s : Set E
h : f =ᶠ[𝓝ˢ s] g
⊢ CPolynomialOn 𝕜 f s ↔ CPolynomialOn 𝕜 g s

Tactic:
⟨fun hf => hf.congr' h, fun hg => hg.congr' h.symm⟩

Premises used: Iff.intro, CPolynomialOn.congr', Filter.EventuallyEq.symm
-- Module: Mathlib.Analysis.Analytic.CPolynomialDef
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
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
hf : CPolynomialOn 𝕜 f s
hg : EqOn f g s
⊢ CPolynomialOn 𝕜 g s

Tactic:
hf.congr' <| mem_nhdsSet_iff_forall.mpr
    (fun _ hz => eventuallyEq_iff_exists_mem.mpr ⟨s, hs.mem_nhds hz, hg⟩)

Premises used: Iff.mpr, mem_nhdsSet_iff_forall, And.intro, IsOpen.mem_nhds, Exists.intro, Filter.eventuallyEq_iff_exists_mem, CPolynomialOn.congr'
-- Module: Mathlib.Analysis.Analytic.CPolynomialDef
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
s : Set E
hs : IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s
h : EqOn f g s
⊢ CPolynomialOn 𝕜 f s ↔ CPolynomialOn 𝕜 g s

Tactic:
⟨fun hf => hf.congr hs h, fun hg => hg.congr hs h.symm⟩

Premises used: Iff.intro, CPolynomialOn.congr, Set.EqOn.symm
-- Module: Mathlib.Analysis.Analytic.CPolynomialDef
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
n : ℕ
g : F →L[𝕜] G
h : HasFiniteFPowerSeriesOnBall f p x n r
m : ℕ
hm : n ≤ m
rw :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin m) ↦ E) G)
    (g.compContinuousMultilinearMap (M₁ := fun (i : Fin m) ↦ E) 0) 0
⊢ g.compFormalMultilinearSeries p m = 0

Tactic:
rw [compFormalMultilinearSeries_apply, h.finite m hm]

Premises used: ContinuousLinearMap.compFormalMultilinearSeries_apply, HasFiniteFPowerSeriesOnBall.finite
-- Module: Mathlib.Analysis.Analytic.CPolynomialDef
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
n : ℕ
g : F →L[𝕜] G
h : HasFiniteFPowerSeriesOnBall f p x n r
m : ℕ
hm : n ≤ m
H :
  ∀ (x : (i : Fin m) → E),
    Eq.{u_4 + 1} (α := G)
      ((g.compContinuousMultilinearMap (M₁ := fun (i : Fin m) ↦ E) 0 : (a : (i : Fin m) → E) → G) x : G)
      ((0 : (a : (i : Fin m) → E) → G) x : G)
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_4} 𝕜 (fun (i : Fin m) ↦ E) G)
    (g.compContinuousMultilinearMap (M₁ := fun (i : Fin m) ↦ E) 0) 0

Tactic:
ext
-- Module: Mathlib.Analysis.Analytic.CPolynomialDef
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
n : ℕ
g : F →L[𝕜] G
h : HasFiniteFPowerSeriesOnBall f p x n r
m : ℕ
hm : n ≤ m
x_1 : (i : Fin m) → E
⊢ Eq.{u_4 + 1} (α := G)
    ((g.compContinuousMultilinearMap (M₁ := fun (i : Fin m) ↦ E) 0 : (a : (i : Fin m) → E) → G) x_1 : G)
    ((0 : (a : (i : Fin m) → E) → G) x_1 : G)

Tactic:
map_zero g

Premises used: map_zero
-- Module: Mathlib.Analysis.Analytic.CPolynomialDef
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
n : ℕ
g : F →L[𝕜] G
h : HasFiniteFPowerSeriesOnBall f p x n r
m : ℕ
hm : n ≤ m
x_1 : (i : Fin m) → E
⊢ Eq.{u_4 + 1} (α := G)
    ((g.compContinuousMultilinearMap (M₁ := fun (i : Fin m) ↦ E) 0 : (a : (i : Fin m) → E) → G) x_1 : G)
    ((0 : (a : (i : Fin m) → E) → G) x_1 : G)

Tactic:
exact map_zero g

Premises used: map_zero
-- Module: Mathlib.Analysis.Analytic.CPolynomialDef
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F
s : Set E
g : F →L[𝕜] G
h : CPolynomialOn 𝕜 f s
x : E
hx : x ∈ s
rcases :
  ∀ (p : FormalMultilinearSeries 𝕜 E F) (n : ℕ) (r : ℝ≥0∞) (hp : HasFiniteFPowerSeriesOnBall f p x n r),
    CPolynomialAt.{u_1, u_2, u_4} 𝕜 (F := G) ((⇑g : (a : F) → G) ∘ f) x
⊢ CPolynomialAt.{u_1, u_2, u_4} 𝕜 (F := G) ((⇑g : (a : F) → G) ∘ f) x

Tactic:
rcases h x hx with ⟨p, n, r, hp⟩
-- Module: Mathlib.Analysis.Analytic.CPolynomialDef
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F
s : Set E
g : F →L[𝕜] G
h : CPolynomialOn 𝕜 f s
x : E
hx : x ∈ s
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
r : ℝ≥0∞
hp : HasFiniteFPowerSeriesOnBall f p x n r
⊢ CPolynomialAt.{u_1, u_2, u_4} 𝕜 (F := G) ((⇑g : (a : F) → G) ∘ f) x

Tactic:
⟨g.compFormalMultilinearSeries p, n, r, g.comp_hasFiniteFPowerSeriesOnBall hp⟩

Premises used: ContinuousLinearMap.comp_hasFiniteFPowerSeriesOnBall, Exists.intro, CPolynomialAt, ContinuousLinearMap.compFormalMultilinearSeries
-- Module: Mathlib.Analysis.Analytic.CPolynomialDef
Goal:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E → F
s : Set E
g : F →L[𝕜] G
h : CPolynomialOn 𝕜 f s
x : E
hx : x ∈ s
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
r : ℝ≥0∞
hp : HasFiniteFPowerSeriesOnBall f p x n r
⊢ CPolynomialAt.{u_1, u_2, u_4} 𝕜 (F := G) ((⇑g : (a : F) → G) ∘ f) x

Tactic:
exact ⟨g.compFormalMultilinearSeries p, n, r, g.comp_hasFiniteFPowerSeriesOnBall hp⟩
-- Module: Mathlib.Analysis.Analytic.CPolynomialDef
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∞
n : ℕ
hf : HasFiniteFPowerSeriesOnBall f p x n r
y : E
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
m : ℕ
hm : n ≤ m
N : ℕ
hN : N ∉ Finset.range m
simp : Eq.{u_3 + 1} (α := F) ((p N : (a : (i : Fin N) → E) → F) fun (x : Fin N) ↦ y : F) (0 : F)
⊢ Eq.{u_3 + 1} (α := F) ((fun (m : ℕ) ↦ ((p m : (a : (i : Fin m) → E) → F) fun (x : Fin m) ↦ y : F)) N) 0

Tactic:
simp only
-- Module: Mathlib.Analysis.Analytic.CPolynomialDef
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∞
n : ℕ
hf : HasFiniteFPowerSeriesOnBall f p x n r
y : E
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
m : ℕ
hm : n ≤ m
N : ℕ
hN : N ∉ Finset.range m
⊢ m ≤ N

Tactic:
simp only [Finset.mem_range, not_lt] at hN

Premises used: Finset.mem_range, not_lt
-- Module: Mathlib.Analysis.Analytic.CPolynomialDef
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∞
n : ℕ
hf : HasFiniteFPowerSeriesOnBall f p x n r
y : E
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
m : ℕ
hm : n ≤ m
N : ℕ
hN : m ≤ N
rw : Eq.{u_3 + 1} (α := F) ((0 : (a : (i : Fin N) → E) → F) fun (x : Fin N) ↦ y : F) (0 : F)
rw₁ rw₂ : Eq.{u_3 + 1} (α := F) 0 0
⊢ Eq.{u_3 + 1} (α := F) ((p N : (a : (i : Fin N) → E) → F) fun (x : Fin N) ↦ y : F) (0 : F)

Tactic:
rw [hf.finite _ (le_trans hm hN), ContinuousMultilinearMap.zero_apply]

Premises used: HasFiniteFPowerSeriesOnBall.finite, ContinuousMultilinearMap.zero_apply, le_trans
-- Module: Mathlib.Analysis.Analytic.CPolynomialDef
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∞
n : ℕ
hf : HasFiniteFPowerSeriesOnBall f p x n r
y : E
hy : y ∈ Metric.eball x r
m : ℕ
hm : n ≤ m
rw : ∀ (hy : Membership.mem (γ := Set E) (Metric.eball 0 r) (y - x)) (m : ℕ) (hm : n ≤ m), f y = p.partialSum m (y - x)
⊢ f y = p.partialSum m (y - x)

Tactic:
rw [Metric.mem_eball, edist_eq_enorm_sub, ← mem_eball_zero_iff] at hy

Premises used: edist_eq_enorm_sub, mem_eball_zero_iff, Metric.mem_eball
-- Module: Mathlib.Analysis.Analytic.CPolynomialDef
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∞
n : ℕ
hf : HasFiniteFPowerSeriesOnBall f p x n r
y : E
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) (y - x)
m : ℕ
hm : n ≤ m
rw : f y = f (x + (y - x))
rw₁ rw₂ : f y = f y
⊢ f y = p.partialSum m (y - x)

Tactic:
rw [← (HasFiniteFPowerSeriesOnBall.eq_partialSum hf _ hy m hm), add_sub_cancel]

Premises used: HasFiniteFPowerSeriesOnBall.eq_partialSum, add_sub_cancel
-- Module: Mathlib.Analysis.Analytic.CPolynomialDef
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
pf : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFiniteFPowerSeriesOnBall f pf x 0 r
y : E
hy : y ∈ Metric.eball x r
rw : Eq.{u_3 + 1} (α := F) (∑ k ∈ Finset.range 0, (pf k : (a : (i : Fin k) → E) → F) fun (x_1 : Fin k) ↦ y - x) 0
⊢ f y = 0

Tactic:
rw [hf.eq_partialSum' y hy 0 le_rfl, FormalMultilinearSeries.partialSum]

Premises used: le_rfl, FormalMultilinearSeries.partialSum, HasFiniteFPowerSeriesOnBall.eq_partialSum', OfNat.ofNat
-- Module: Mathlib.Analysis.Analytic.CPolynomialDef
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
pf : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFiniteFPowerSeriesOnBall f pf x 0 r
y : E
hy : y ∈ Metric.eball x r
⊢ Eq.{u_3 + 1} (α := F) (∑ k ∈ Finset.range 0, (pf k : (a : (i : Fin k) → E) → F) fun (x_1 : Fin k) ↦ y - x) 0

Tactic:
simp only [Finset.range_zero, Finset.sum_empty]

Premises used: Finset.sum_empty, Finset.range_zero
-- Module: Mathlib.Analysis.Analytic.CPolynomialDef
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 : ∀ y ∈ Metric.eball x r, f y = 0
r_pos : 0 < r
hp : ∀ (n : ℕ), p n = 0
⊢ HasFiniteFPowerSeriesOnBall f p x 0 r

Tactic:
⟨⟨?_, r_pos, ?_⟩, fun n _ ↦ hp n⟩

Premises used: HasFiniteFPowerSeriesOnBall.mk, HasFPowerSeriesOnBall.mk
-- Module: Mathlib.Analysis.Analytic.CPolynomialDef
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 : ∀ y ∈ Metric.eball x r, f y = 0
r_pos : 0 < r
hp : ∀ (n : ℕ), p n = 0
refine_1 : r ≤ p.radius
refine_2 :
  ∀ {y : E},
    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))
⊢ HasFiniteFPowerSeriesOnBall f p x 0 r

Tactic:
refine ⟨⟨?_, r_pos, ?_⟩, fun n _ ↦ hp n⟩
-- Module: Mathlib.Analysis.Analytic.CPolynomialDef
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 : ∀ y ∈ Metric.eball x r, f y = 0
r_pos : 0 < r
hp : ∀ (n : ℕ), p n = 0
n : ℕ
rw : p n = 0
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 0)) ↦ E) F) (p (n + 0)) 0

Tactic:
rw [add_zero]

Premises used: add_zero
-- Module: Mathlib.Analysis.Analytic.CPolynomialDef
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 : ∀ y ∈ Metric.eball x r, f y = 0
r_pos : 0 < r
hp : ∀ (n : ℕ), p n = 0
n : ℕ
⊢ p n = 0

Tactic:
hp n
-- Module: Mathlib.Analysis.Analytic.CPolynomialDef
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 : ∀ y ∈ Metric.eball x r, f y = 0
r_pos : 0 < r
hp : ∀ (n : ℕ), p n = 0
n : ℕ
⊢ p n = 0

Tactic:
exact hp n
-- Module: Mathlib.Analysis.Analytic.CPolynomialDef
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 : ∀ y ∈ Metric.eball x r, f y = 0
r_pos : 0 < r
hp : ∀ (n : ℕ), p n = 0
refine_1 : r ≤ ∞
⊢ r ≤ p.radius

Tactic:
rw [p.radius_eq_top_of_forall_image_add_eq_zero 0 (fun n ↦ by rw [add_zero]; exact hp n)]

Premises used: FormalMultilinearSeries.radius_eq_top_of_forall_image_add_eq_zero, OfNat.ofNat
-- Module: Mathlib.Analysis.Analytic.CPolynomialDef
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 : ∀ y ∈ Metric.eball x r, f y = 0
r_pos : 0 < r
hp : ∀ (n : ℕ), p n = 0
⊢ r ≤ ∞

Tactic:
le_top

Premises used: le_top
-- Module: Mathlib.Analysis.Analytic.CPolynomialDef
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 : ∀ y ∈ Metric.eball x r, f y = 0
r_pos : 0 < r
hp : ∀ (n : ℕ), p n = 0
⊢ r ≤ ∞

Tactic:
exact le_top

Premises used: le_top
-- Module: Mathlib.Analysis.Analytic.CPolynomialDef
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 : ∀ y ∈ Metric.eball x r, f y = 0
r_pos : 0 < r
hp : ∀ (n : ℕ), p n = 0
y : E
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
refine_2 : HasSum.{u_3, 0} (α := F) (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y) 0
refine_2₁ : x + y ∈ Metric.eball x r
⊢ HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y) (f (x + y))

Tactic:
rw [hf (x + y)]

Premises used: HAdd.hAdd
-- Module: Mathlib.Analysis.Analytic.CPolynomialDef
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 : ∀ y ∈ Metric.eball x r, f y = 0
r_pos : 0 < r
hp : ∀ (n : ℕ), p n = 0
y : E
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
⊢ HasSum.{u_3, 0} (α := F) (fun (x : ℕ) ↦ 0) 0

Tactic:
hasSum_zero

Premises used: hasSum_zero