awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomial (hypothesis)
Goal:
𝕜 : Type u_1
F : Type u_3
G : Type u_4
inst : NontriviallyNormedField 𝕜
inst_1 : NormedAddCommGroup F
inst_2 : NormedSpace 𝕜 F
inst_3 : NormedAddCommGroup G
inst_4 : NormedSpace 𝕜 G
ι : Type u_5
Em : ι → Type u_6
inst_5 : (i : ι) → NormedAddCommGroup (Em i)
inst_6 : (i : ι) → NormedSpace.{u_1, u_6} 𝕜 (Em i)
inst_7 : Fintype ι
f : ContinuousMultilinearMap 𝕜 Em (G →L[𝕜] F)
x : ((i : ι) → Em i) × G
⊢ CPolynomialAt 𝕜 (F := F)
    (fun (p : ((i : ι) → Em i) × G) ↦ (((f : (a : (i : ι) → Em i) → G →L[𝕜] F) p.1 : G →L[𝕜] F) : (a : G) → F) p.2) x
have this : CPolynomialAt 𝕜 (F := G × ((i : ι) → Em i))
  (⇑(↑(ContinuousLinearEquiv.prodComm 𝕜 ((i : ι) → Em i) G) : ((i : ι) → Em i) × G →L[𝕜] G × ((i : ι) → Em i)) :
    (a : ((i : ι) → Em i) × G) → G × ((i : ι) → Em i))
  x
Tactic: have : CPolynomialAt 𝕜 (ContinuousLinearEquiv.prodComm 𝕜 (Π i, Em i) G).toContinuousLinearMap x :=
    ContinuousLinearMap.cpolynomialAt _ _
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomialDef (hypothesis)
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 : ℕ
r : ℝ≥0∞
finite : ∀ (m : ℕ), n ≤ m → p m = 0
pos : 0 < r
sum_eq :
  ∀ (y : E),
    Membership.mem (γ := Set E) (Metric.eball 0 r) y →
      (∑ i ∈ Finset.range n, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ y) = f (x + y)
y : E
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
m : ℕ
hm : m ∉ Finset.range n
⊢ Eq.{u_3 + 1} (α := F) ((p m : (a : (i : Fin m) → E) → F) fun (x : Fin m) ↦ y : F) (0 : F)
have hm₁ : n ≤ m
Tactic: rw [Finset.mem_range, not_lt] at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomialDef (goal)
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 : ℕ
r : ℝ≥0∞
finite : ∀ (m : ℕ), n ≤ m → p m = 0
pos : 0 < r
sum_eq :
  ∀ (y : E),
    Membership.mem (γ := Set E) (Metric.eball 0 r) y →
      (∑ i ∈ Finset.range n, (p i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ y) = f (x + y)
y : E
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
m : ℕ
hm : n ≤ m
⊢ Eq.{u_3 + 1} (α := F) ((p m : (a : (i : Fin m) → E) → F) fun (x : Fin m) ↦ y : F) (0 : F)
have rw : Eq.{u_3 + 1} (α := F) ((0 : (a : (i : Fin m) → E) → F) fun (x : Fin m) ↦ y : F) (0 : F)
Tactic: rw [finite m hm]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomialDef (goal)
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
⊢ HasFiniteFPowerSeriesAt f p x m
have rcases : ∀ (r : ℝ≥0∞) (hr : HasFiniteFPowerSeriesOnBall f p x n r), HasFiniteFPowerSeriesAt f p x m
Tactic: rcases h with ⟨r, hr⟩
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomialDef (goal)
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
⊢ g.compFormalMultilinearSeries p m = 0
have 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
Tactic: rw [compFormalMultilinearSeries_apply, h.finite m hm]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomialDef (goal)
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
⊢ 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
have 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)
Tactic: ext
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomialDef (goal)
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
⊢ CPolynomialAt.{u_1, u_2, u_4} 𝕜 (F := G) ((⇑g : (a : F) → G) ∘ f) x
have 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
Tactic: rcases h x hx with ⟨p, n, r, hp⟩
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomialDef (hypothesis)
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
⊢ Eq.{u_3 + 1} (α := F) ((p N : (a : (i : Fin N) → E) → F) fun (x : Fin N) ↦ y : F) (0 : F)
have hN₁ : m ≤ N
Tactic: simp only [Finset.mem_range, not_lt] at hN
Cleared hypotheses: hN
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomialDef (goal)
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
⊢ Eq.{u_3 + 1} (α := F) ((p N : (a : (i : Fin N) → E) → F) fun (x : Fin N) ↦ y : F) (0 : F)
have rw : Eq.{u_3 + 1} (α := F) ((0 : (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]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomialDef (goal)
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)
⊢ Eq.{u_3 + 1} (α := F) ((p N : (a : (i : Fin N) → E) → F) fun (x : Fin N) ↦ y : F) (0 : F)
have rw₁ : Eq.{u_3 + 1} (α := F) 0 0
Tactic: rw [hf.finite _ (le_trans hm hN), ContinuousMultilinearMap.zero_apply]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomialDef (goal)
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
⊢ f y = p.partialSum m (y - x)
have rw : ∀ (hy : Membership.mem (γ := Set E) (Metric.eball 0 r) (y - x)) (m : ℕ) (hm : n ≤ m), f y = p.partialSum m (y - x)
Tactic: rw [Metric.mem_eball, edist_eq_enorm_sub, ← mem_eball_zero_iff] at hy
Cleared hypotheses: hy, m, hm
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomialDef (goal)
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
⊢ f y = p.partialSum m (y - x)
have rw : f y = f (x + (y - x))
Tactic: rw [← (HasFiniteFPowerSeriesOnBall.eq_partialSum hf _ hy m hm), add_sub_cancel]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomialDef (goal)
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))
⊢ f y = p.partialSum m (y - x)
have rw₁ : f y = f y
Tactic: rw [← (HasFiniteFPowerSeriesOnBall.eq_partialSum hf _ hy m hm), add_sub_cancel]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomialDef (goal)
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
⊢ f y = 0
have 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
Tactic: rw [hf.eq_partialSum' y hy 0 le_rfl, FormalMultilinearSeries.partialSum]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomialDef (goal)
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
have refine_1 : r ≤ p.radius
Tactic: refine ⟨⟨?_, r_pos, ?_⟩, fun n _ ↦ hp n⟩
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomialDef (goal)
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
⊢ HasFiniteFPowerSeriesOnBall f p x 0 r
have 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))
Tactic: refine ⟨⟨?_, r_pos, ?_⟩, fun n _ ↦ hp n⟩
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomialDef (goal)
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 : ℕ
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 0)) ↦ E) F) (p (n + 0)) 0
have rw : p n = 0
Tactic: rw [add_zero]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomialDef (goal)
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 ≤ p.radius
have refine_1 : r ≤ ∞
Tactic: rw [p.radius_eq_top_of_forall_image_add_eq_zero 0 (fun n ↦ by rw [add_zero]; exact hp n)]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomialDef (goal)
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 (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y) (f (x + y))
have refine_2 : HasSum.{u_3, 0} (α := F) (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y) 0
Tactic: rw [hf (x + y)]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomialDef (goal)
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
⊢ HasSum (fun (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y) (f (x + y))
have refine_2₁ : x + y ∈ Metric.eball x r
Tactic: rw [hf (x + y)]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomialDef (goal)
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 (n : ℕ) ↦ (p n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y) 0
have h : ∀ (x : ℕ), Eq.{u_3 + 1} (α := F) ((p x : (a : (i : Fin x) → E) → F) fun (x : Fin x) ↦ y : F) (0 : F)
Tactic: convert! hasSum_zero
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomialDef (goal)
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 : ℕ
⊢ Eq.{u_3 + 1} (α := F) ((p x_1 : (a : (i : Fin x_1) → E) → F) fun (x : Fin x_1) ↦ y : F) (0 : F)
have h : Eq.{u_3 + 1} (α := F) ((0 : (a : (i : Fin x_1) → E) → F) fun (x : Fin x_1) ↦ y : F) (0 : F)
Tactic: rw [hp, ContinuousMultilinearMap.zero_apply]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomialDef (goal)
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)
⊢ Eq.{u_3 + 1} (α := F) ((p x_1 : (a : (i : Fin x_1) → E) → F) fun (x : Fin x_1) ↦ y : F) (0 : F)
have h₁ : Eq.{u_3 + 1} (α := F) 0 0
Tactic: rw [hp, ContinuousMultilinearMap.zero_apply]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomialDef (goal)
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 + y ∈ Metric.eball x r
have refine_2 : edist (x + y) x < r
Tactic: rwa [Metric.mem_eball, edist_eq_enorm_sub, add_comm, add_sub_cancel_right,
        ← edist_zero_right, ← Metric.mem_eball]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomialDef (goal)
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
⊢ x + y ∈ Metric.eball x r
have refine_2₁ : ‖x + y - x‖ₑ < r
Tactic: rwa [Metric.mem_eball, edist_eq_enorm_sub, add_comm, add_sub_cancel_right,
        ← edist_zero_right, ← Metric.mem_eball]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomialDef (goal)
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
⊢ x + y ∈ Metric.eball x r
have refine_2₂ : ‖y + x - x‖ₑ < r
Tactic: rwa [Metric.mem_eball, edist_eq_enorm_sub, add_comm, add_sub_cancel_right,
        ← edist_zero_right, ← Metric.mem_eball]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomialDef (goal)
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
⊢ x + y ∈ Metric.eball x r
have refine_2₃ : ‖y‖ₑ < r
Tactic: rwa [Metric.mem_eball, edist_eq_enorm_sub, add_comm, add_sub_cancel_right,
        ← edist_zero_right, ← Metric.mem_eball]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomialDef (goal)
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
⊢ x + y ∈ Metric.eball x r
have refine_2₄ : edist y 0 < r
Tactic: rwa [Metric.mem_eball, edist_eq_enorm_sub, add_comm, add_sub_cancel_right,
        ← edist_zero_right, ← Metric.mem_eball]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomialDef (goal)
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 ∈ Metric.eball x r
have rw : 0 < r
Tactic: rw [Metric.mem_eball, edist_self]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomialDef (goal)
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
⊢ f y = f x
have rw : pf.partialSum 1 (y - x) = pf.partialSum 1 (x - 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]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomialDef (goal)
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
⊢ pf.partialSum 1 (y - x) = pf.partialSum 1 (x - x)
have 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)
Tactic: simp only [FormalMultilinearSeries.partialSum, Finset.range_one, Finset.sum_singleton]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomialDef (goal)
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
⊢ 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)
have h : Eq.{u_2 + 1} (α := (i : Fin 0) → E) (fun (x_1 : Fin 0) ↦ y - x) fun (x_1 : Fin 0) ↦ x - x
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomialDef (goal)
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
⊢ Eq.{u_2 + 1} (α := (i : Fin 0) → E) (fun (x_1 : Fin 0) ↦ y - x) fun (x_1 : Fin 0) ↦ x - x
have h : ∀ (x_1 : Fin 0), y - x = x - x
Tactic: apply funext
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomialDef (goal)
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
⊢ Continuous[PseudoMetricSpace.toUniformSpace.toTopologicalSpace, PseudoMetricSpace.toUniformSpace.toTopologicalSpace] f
have rw : ContinuousOn f univ
Tactic: rw [← continuousOn_univ]
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomialDef (hypothesis)
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
⊢ Eq.{u_3 + 1} (α := F) ((p m : (a : (i : Fin m) → E) → F) fun (x_1 : Fin m) ↦ x : F) (0 : F)
have hm₁ : n ≤ m
Tactic: rw [Finset.mem_range, not_lt] at hm
Cleared hypotheses: hm
-- Lean 4 proof step from Mathlib.Analysis.Analytic.CPolynomialDef (goal)
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) ((p m : (a : (i : Fin m) → E) → F) fun (x_1 : Fin m) ↦ x : F) (0 : F)
have rw : Eq.{u_3 + 1} (α := F) ((0 : (a : (i : Fin m) → E) → F) fun (x_1 : Fin m) ↦ x : F) (0 : F)
Tactic: rw [hn m hm]