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 : 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
h : ∀ (x : ℕ), Eq.{u_3 + 1} (α := F) ((p x : (a : (i : Fin x) → E) → F) fun (x : Fin x) ↦ y : F) (0 : F)
⊢ HasSum.{u_3, 0} (α := F) (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y) 0

Tactic:
convert! hasSum_zero

Premises used: hasSum_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
y : E
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
x_1 : ℕ
h : Eq.{u_3 + 1} (α := F) ((0 : (a : (i : Fin x_1) → E) → F) fun (x : Fin x_1) ↦ y : F) (0 : F)
h₁ h₂ : Eq.{u_3 + 1} (α := F) 0 0
⊢ Eq.{u_3 + 1} (α := F) ((p x_1 : (a : (i : Fin x_1) → E) → F) fun (x : Fin x_1) ↦ y : F) (0 : F)

Tactic:
rw [hp, ContinuousMultilinearMap.zero_apply]

Premises used: ContinuousMultilinearMap.zero_apply
-- 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 : edist (x + y) x < r
refine_2₁ : ‖x + y - x‖ₑ < r
refine_2₂ : ‖y + x - x‖ₑ < r
refine_2₃ : ‖y‖ₑ < r
refine_2₄ : edist y 0 < r
refine_2₅ refine_2₆ refine_2₇ refine_2₈ : Membership.mem (γ := Set E) (Metric.eball 0 r) y
⊢ x + y ∈ Metric.eball x r

Tactic:
rwa [Metric.mem_eball, edist_eq_enorm_sub, add_comm, add_sub_cancel_right,
        ← edist_zero_right, ← Metric.mem_eball]

Premises used: edist_eq_enorm_sub, add_comm, edist_zero_right, add_sub_cancel_right, 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
pf : FormalMultilinearSeries 𝕜 E F
x : E
hf : HasFiniteFPowerSeriesAt f pf x 0
⊢ f =ᶠ[𝓝 x] 0

Tactic:
Filter.eventuallyEq_iff_exists_mem.mpr (let ⟨r, hf⟩ := hf; ⟨Metric.eball x r,
    Metric.eball_mem_nhds x hf.r_pos, fun y hy ↦ hf.eq_zero_of_bound_zero y hy⟩)

Premises used: Iff.mpr, Membership.mem, Exists, nhds, HasFiniteFPowerSeriesOnBall.toHasFPowerSeriesOnBall, Set.EqOn, Metric.eball, _private.0.HasFiniteFPowerSeriesAt.eventually_zero_of_bound_zero.match_1, Metric.eball_mem_nhds, And, And.intro, Exists.intro, Filter.eventuallyEq_iff_exists_mem, OfNat.ofNat, HasFPowerSeriesOnBall.r_pos, HasFiniteFPowerSeriesOnBall.eq_zero_of_bound_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
pf : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFiniteFPowerSeriesOnBall f pf x 1 r
y : E
hy : y ∈ Metric.eball x r
rw : 0 < r
⊢ x ∈ Metric.eball x r

Tactic:
rw [Metric.mem_eball, edist_self]

Premises used: PseudoEMetricSpace.edist_self, 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
pf : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFiniteFPowerSeriesOnBall f pf x 1 r
y : E
hy : y ∈ Metric.eball x r
⊢ 0 < r

Tactic:
hf.r_pos

Premises used: HasFiniteFPowerSeriesOnBall.toHasFPowerSeriesOnBall, HasFPowerSeriesOnBall.r_pos
-- 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 1 r
y : E
hy : y ∈ Metric.eball x r
⊢ 0 < r

Tactic:
exact hf.r_pos

Premises used: HasFiniteFPowerSeriesOnBall.toHasFPowerSeriesOnBall, HasFPowerSeriesOnBall.r_pos
-- 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 1 r
y : E
hy : y ∈ Metric.eball x r
rw : pf.partialSum 1 (y - x) = pf.partialSum 1 (x - x)
⊢ f y = f x

Tactic:
rw [hf.eq_partialSum' y hy 1 le_rfl, hf.eq_partialSum' x
    (by rw [Metric.mem_eball, edist_self]; exact hf.r_pos) 1 le_rfl]

Premises used: le_rfl, 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 1 r
y : E
hy : y ∈ Metric.eball x r
simp :
  Eq.{u_3 + 1} (α := F) ((pf 0 : (a : (i : Fin 0) → E) → F) fun (x_1 : Fin 0) ↦ y - x : F)
    ((pf 0 : (a : (i : Fin 0) → E) → F) fun (x_1 : Fin 0) ↦ x - x : F)
⊢ pf.partialSum 1 (y - x) = pf.partialSum 1 (x - x)

Tactic:
simp only [FormalMultilinearSeries.partialSum, Finset.range_one, Finset.sum_singleton]

Premises used: FormalMultilinearSeries.partialSum, Finset.sum_singleton, Finset.range_one
-- 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 1 r
y : E
hy : y ∈ Metric.eball x r
h : Eq.{u_2 + 1} (α := (i : Fin 0) → E) (fun (x_1 : Fin 0) ↦ y - x) fun (x_1 : Fin 0) ↦ x - x
⊢ Eq.{u_3 + 1} (α := F) ((pf 0 : (a : (i : Fin 0) → E) → F) fun (x_1 : Fin 0) ↦ y - x : F)
    ((pf 0 : (a : (i : Fin 0) → E) → F) fun (x_1 : Fin 0) ↦ x - x : F)

Tactic:
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 : E → F
pf : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFiniteFPowerSeriesOnBall f pf x 1 r
y : E
hy : y ∈ Metric.eball x r
h : ∀ (x_1 : Fin 0), y - x = x - x
⊢ Eq.{u_2 + 1} (α := (i : Fin 0) → E) (fun (x_1 : Fin 0) ↦ y - x) fun (x_1 : Fin 0) ↦ x - x

Tactic:
apply funext

Premises used: funext
-- 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 1 r
y : E
hy : y ∈ Metric.eball x r
⊢ ∀ (x_1 : Fin 0), y - x = x - x

Tactic:
simp only [IsEmpty.forall_iff]

Premises used: IsEmpty.forall_iff
-- 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
hf : HasFiniteFPowerSeriesAt f pf x 1
⊢ f =ᶠ[𝓝 x] fun (x_1 : E) ↦ f x

Tactic:
Filter.eventuallyEq_iff_exists_mem.mpr (let ⟨r, hf⟩ := hf; ⟨Metric.eball x r,
    Metric.eball_mem_nhds x hf.r_pos, fun y hy ↦ hf.eq_const_of_bound_one y hy⟩)

Premises used: Iff.mpr, HasFiniteFPowerSeriesOnBall.eq_const_of_bound_one, Membership.mem, Exists, nhds, HasFiniteFPowerSeriesOnBall.toHasFPowerSeriesOnBall, Set.EqOn, Metric.eball, Metric.eball_mem_nhds, And, _private.0.HasFiniteFPowerSeriesAt.eventually_const_of_bound_one.match_1, And.intro, Exists.intro, Filter.eventuallyEq_iff_exists_mem, HasFPowerSeriesOnBall.r_pos
-- 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
⊢ ContinuousOn f (Metric.eball x r)

Tactic:
hf.1.continuousOn

Premises used: HasFiniteFPowerSeriesOnBall.toHasFPowerSeriesOnBall, HasFPowerSeriesOnBall.continuousOn
-- 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
⊢ ContinuousAt f x

Tactic:
hf.hasFPowerSeriesAt.continuousAt

Premises used: HasFiniteFPowerSeriesAt.hasFPowerSeriesAt, HasFPowerSeriesAt.continuousAt
-- 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
x : E
hf : CPolynomialAt 𝕜 f x
⊢ ContinuousAt f x

Tactic:
hf.analyticAt.continuousAt

Premises used: CPolynomialAt.analyticAt, AnalyticAt.continuousAt
-- 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 : Set E
hf : CPolynomialOn 𝕜 f s
⊢ ContinuousOn f s

Tactic:
hf.analyticOnNhd.continuousOn

Premises used: CPolynomialOn.analyticOnNhd, AnalyticOnNhd.continuousOn
-- 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
fa : CPolynomialOn 𝕜 f univ
rw : ContinuousOn f univ
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f

Tactic:
rw [← continuousOn_univ]

Premises used: continuousOn_univ
-- 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
fa : CPolynomialOn 𝕜 f univ
⊢ ContinuousOn f univ

Tactic:
fa.continuousOn

Premises used: CPolynomialOn.continuousOn
-- 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
fa : CPolynomialOn 𝕜 f univ
⊢ ContinuousOn f univ

Tactic:
exact fa.continuousOn

Premises used: CPolynomialOn.continuousOn
-- 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
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
x : E
m : ℕ
hm : m ∉ Finset.range n
⊢ n ≤ m

Tactic:
rw [Finset.mem_range, not_lt] at hm

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
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
x : E
m : ℕ
hm : n ≤ m
rw : Eq.{u_3 + 1} (α := F) ((0 : (a : (i : Fin m) → E) → F) fun (x_1 : Fin m) ↦ x : F) (0 : F)
⊢ Eq.{u_3 + 1} (α := F) ((p m : (a : (i : Fin m) → E) → F) fun (x_1 : Fin m) ↦ x : F) (0 : F)

Tactic:
rw [hn m hm]
-- 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
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
x : E
m : ℕ
hm : n ≤ m
⊢ Eq.{u_3 + 1} (α := F) ((0 : (a : (i : Fin m) → E) → F) fun (x_1 : Fin m) ↦ x : F) (0 : F)

Tactic:
rfl
-- 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
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
rw rw₁ : LE.le (α := ℝ≥0∞) ∞ ∞
⊢ ∞ ≤ p.radius

Tactic:
rw [radius_eq_top_of_forall_image_add_eq_zero p n fun _ => hn _ (Nat.le_add_left _ _)]

Premises used: Nat.le_add_left, HAdd.hAdd, FormalMultilinearSeries.radius_eq_top_of_forall_image_add_eq_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
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
y : E
h : Membership.mem (γ := Set E) (Metric.eball 0 ∞) y
rw : HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y) (p.sum y)
⊢ HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y) (p.sum (0 + y))

Tactic:
rw [zero_add]

Premises used: zero_add
-- 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
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
y : E
h : Membership.mem (γ := Set E) (Metric.eball 0 ∞) y
⊢ HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y) (p.sum y)

Tactic:
p.hasSum_of_finite hn y

Premises used: FormalMultilinearSeries.hasSum_of_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
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
y : E
h : Membership.mem (γ := Set E) (Metric.eball 0 ∞) y
⊢ HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y) (p.sum y)

Tactic:
exact p.hasSum_of_finite hn y

Premises used: FormalMultilinearSeries.hasSum_of_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∞
n : ℕ
h : HasFiniteFPowerSeriesOnBall f p x n r
y : E
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
⊢ f (x + y) = p.sum y

Tactic:
(h.hasSum hy).tsum_eq.symm

Premises used: HasFiniteFPowerSeriesOnBall.toHasFPowerSeriesOnBall, HasFPowerSeriesOnBall.hasSum, HasSum.tsum_eq, Eq.symm, FormalMultilinearSeries.sum
-- 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
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
rw : ContinuousOn p.sum (Metric.eball 0 ∞)
rw₁ : E
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace]
    p.sum

Tactic:
rw [← continuousOn_univ, ← Metric.eball_top]

Premises used: Metric.eball_top, continuousOn_univ
-- 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
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
⊢ ContinuousOn p.sum (Metric.eball 0 ∞)

Tactic:
(p.hasFiniteFPowerSeriesOnBall_of_finite hn).continuousOn

Premises used: HasFiniteFPowerSeriesOnBall.continuousOn, FormalMultilinearSeries.hasFiniteFPowerSeriesOnBall_of_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
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
k l : ℕ
s : Finset (Fin (k + l))
hs : s.card = l
hkl : n ≤ k + l
rw :
  ZeroHomClass
    (ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (k + l)) ↦ E) F ≃ₗᵢ[𝕜]
      ContinuousMultilinearMap 𝕜 (fun (i : Fin l) ↦ E)
        (ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin k) ↦ E) F))
    (ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (k + l)) ↦ E) F)
    (ContinuousMultilinearMap 𝕜 (fun (i : Fin l) ↦ E)
      (ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin k) ↦ E) F))
⊢ p.changeOriginSeriesTerm k l s hs = 0

Tactic:
rw [changeOriginSeriesTerm, hn _ hkl, map_zero]

Premises used: map_zero, FormalMultilinearSeries.changeOriginSeriesTerm
-- 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
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
k m : ℕ
hm : n ≤ k + m
⊢ Eq (α :=
    ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E)
      (ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin k) ↦ E) F))
    (∑ s : { s : Finset (Fin (k + m)) // s.card = m }, p.changeOriginSeriesTerm k m (↑s : Finset (Fin (k + m))) ⋯) 0

Tactic:
Finset.sum_eq_zero (fun _ _ => p.changeOriginSeriesTerm_bound hn _ _ _ hm)

Premises used: Finset.sum_eq_zero, FormalMultilinearSeries.changeOriginSeries._proof_2, FormalMultilinearSeries.changeOriginSeriesTerm_bound
-- 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
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
k m : ℕ
hm : n ≤ k + m
⊢ Eq (α :=
    ContinuousMultilinearMap 𝕜 (fun (i : Fin m) ↦ E)
      (ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin k) ↦ E) F))
    (∑ s : { s : Finset (Fin (k + m)) // s.card = m }, p.changeOriginSeriesTerm k m (↑s : Finset (Fin (k + m))) ⋯) 0

Tactic:
exact Finset.sum_eq_zero (fun _ _ => p.changeOriginSeriesTerm_bound hn _ _ _ hm)

Premises used: Finset.sum_eq_zero, FormalMultilinearSeries.changeOriginSeriesTerm_bound
-- 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
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
k : ℕ
h :
  ∀ (x : E) (x_1 : (i : Fin k) → E),
    Eq.{u_3 + 1} (α := F) (((p.changeOriginSeries k).sum x : (a : (i : Fin k) → E) → F) x_1 : F)
      (((p.changeOriginSeries k).partialSum (n - k) x : (a : (i : Fin k) → E) → F) x_1 : F)
⊢ (p.changeOriginSeries k).sum = (p.changeOriginSeries k).partialSum (n - k)

Tactic:
ext x
-- 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
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
k : ℕ
x : E
x_1 : (i : Fin k) → E
h :
  ∀ b ∉ Finset.range (n - k),
    Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin k) ↦ E) F)
      ((p.changeOriginSeries k b : (a : (i : Fin b) → E) → ContinuousMultilinearMap 𝕜 (fun (i : Fin k) ↦ E) F)
        fun (x_2 : Fin b) ↦ x)
      0
⊢ Eq.{u_3 + 1} (α := F) (((p.changeOriginSeries k).sum x : (a : (i : Fin k) → E) → F) x_1 : F)
    (((p.changeOriginSeries k).partialSum (n - k) x : (a : (i : Fin k) → E) → F) x_1 : F)

Tactic:
rw [partialSum, FormalMultilinearSeries.sum,
    tsum_eq_sum (f := fun m => p.changeOriginSeries k m (fun _ => x)) (s := Finset.range (n - k))]

Premises used: FormalMultilinearSeries.partialSum, tsum_eq_sum, FormalMultilinearSeries.sum
-- 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
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
k : ℕ
x : E
x_1 : (i : Fin k) → E
m : ℕ
hm : m ∉ Finset.range (n - k)
⊢ n - k ≤ m

Tactic:
rw [Finset.mem_range, not_lt] at hm

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
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
k : ℕ
x : E
x_1 : (i : Fin k) → E
m : ℕ
hm : n - k ≤ m
rw : n ≤ m + k
⊢ n ≤ k + m

Tactic:
rw [add_comm]

Premises used: add_comm
-- 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
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
k : ℕ
x : E
x_1 : (i : Fin k) → E
m : ℕ
hm : n - k ≤ m
⊢ n ≤ m + k

Tactic:
Nat.le_add_of_sub_le hm

Premises used: Nat.le_add_of_sub_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
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
k : ℕ
x : E
x_1 : (i : Fin k) → E
m : ℕ
hm : n - k ≤ m
⊢ n ≤ m + k

Tactic:
exact Nat.le_add_of_sub_le hm

Premises used: Nat.le_add_of_sub_le