awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Analytic.IteratedFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
x : E
h : ContDiffWithinAt 𝕜 ω f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
σ : Perm (Fin n)
x_1 : (i : Fin n) → E
⊢ Eq.{u_3 + 1} (α := F)
    ((ContinuousMultilinearMap.domDomCongr σ (iteratedFDerivWithin 𝕜 n f s x) : (a : (i : Fin n) → E) → F) x_1 : F)
    ((iteratedFDerivWithin 𝕜 n f s x : (a : (i : Fin n) → E) → F) x_1 : F)

Tactic:
h.iteratedFDerivWithin_comp_perm hs hx _ _

Premises used: ContDiffWithinAt.iteratedFDerivWithin_comp_perm
-- Module: Mathlib.Analysis.Analytic.IteratedFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
s : Set E
x : E
h : ContDiffWithinAt 𝕜 ω f s x
hs : UniqueDiffOn 𝕜 s
hx : x ∈ s
n : ℕ
σ : Perm (Fin n)
x_1 : (i : Fin n) → E
⊢ Eq.{u_3 + 1} (α := F)
    ((ContinuousMultilinearMap.domDomCongr σ (iteratedFDerivWithin 𝕜 n f s x) : (a : (i : Fin n) → E) → F) x_1 : F)
    ((iteratedFDerivWithin 𝕜 n f s x : (a : (i : Fin n) → E) → F) x_1 : F)

Tactic:
exact h.iteratedFDerivWithin_comp_perm hs hx _ _

Premises used: ContDiffWithinAt.iteratedFDerivWithin_comp_perm
-- Module: Mathlib.Analysis.Analytic.IteratedFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
h : AnalyticOn 𝕜 f univ
n : ℕ
v : Fin n → E
σ : Perm (Fin n)
rw :
  Eq.{u_3 + 1} (α := F)
    ((iteratedFDerivWithin 𝕜 n f univ x : (a : (i : Fin n) → E) → F) (v ∘ (⇑σ : (a : Fin n) → Fin n)) : F)
    ((iteratedFDerivWithin 𝕜 n f univ x : (a : (i : Fin n) → E) → F) v : F)
⊢ Eq.{u_3 + 1} (α := F) ((iteratedFDeriv 𝕜 n f x : (a : (i : Fin n) → E) → F) (v ∘ (⇑σ : (a : Fin n) → Fin n)) : F)
    ((iteratedFDeriv 𝕜 n f x : (a : (i : Fin n) → E) → F) v : F)

Tactic:
rw [← iteratedFDerivWithin_univ]

Premises used: iteratedFDerivWithin_univ
-- Module: Mathlib.Analysis.Analytic.IteratedFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
h : AnalyticOn 𝕜 f univ
n : ℕ
v : Fin n → E
σ : Perm (Fin n)
⊢ Eq.{u_3 + 1} (α := F)
    ((iteratedFDerivWithin 𝕜 n f univ x : (a : (i : Fin n) → E) → F) (v ∘ (⇑σ : (a : Fin n) → Fin n)) : F)
    ((iteratedFDerivWithin 𝕜 n f univ x : (a : (i : Fin n) → E) → F) v : F)

Tactic:
h.iteratedFDerivWithin_comp_perm uniqueDiffOn_univ (mem_univ x) _ _

Premises used: AnalyticOn.iteratedFDerivWithin_comp_perm, uniqueDiffOn_univ, Set.mem_univ
-- Module: Mathlib.Analysis.Analytic.IteratedFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
h : AnalyticOn 𝕜 f univ
n : ℕ
v : Fin n → E
σ : Perm (Fin n)
⊢ Eq.{u_3 + 1} (α := F)
    ((iteratedFDerivWithin 𝕜 n f univ x : (a : (i : Fin n) → E) → F) (v ∘ (⇑σ : (a : Fin n) → Fin n)) : F)
    ((iteratedFDerivWithin 𝕜 n f univ x : (a : (i : Fin n) → E) → F) v : F)

Tactic:
exact h.iteratedFDerivWithin_comp_perm uniqueDiffOn_univ (mem_univ x) _ _

Premises used: AnalyticOn.iteratedFDerivWithin_comp_perm, uniqueDiffOn_univ, Set.mem_univ
-- Module: Mathlib.Analysis.Analytic.IteratedFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
h : AnalyticOn 𝕜 f univ
n : ℕ
σ : Perm (Fin n)
rw :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (x : Fin n) ↦ E) F)
    (ContinuousMultilinearMap.domDomCongr σ (iteratedFDerivWithin 𝕜 n f univ x)) (iteratedFDerivWithin 𝕜 n f univ x)
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (x : Fin n) ↦ E) F)
    (ContinuousMultilinearMap.domDomCongr σ (iteratedFDeriv 𝕜 n f x)) (iteratedFDeriv 𝕜 n f x)

Tactic:
rw [← iteratedFDerivWithin_univ]

Premises used: iteratedFDerivWithin_univ
-- Module: Mathlib.Analysis.Analytic.IteratedFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
h : AnalyticOn 𝕜 f univ
n : ℕ
σ : Perm (Fin n)
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (x : Fin n) ↦ E) F)
    (ContinuousMultilinearMap.domDomCongr σ (iteratedFDerivWithin 𝕜 n f univ x)) (iteratedFDerivWithin 𝕜 n f univ x)

Tactic:
h.domDomCongr_iteratedFDerivWithin uniqueDiffOn_univ (mem_univ x) _

Premises used: AnalyticOn.domDomCongr_iteratedFDerivWithin, uniqueDiffOn_univ, Set.mem_univ
-- Module: Mathlib.Analysis.Analytic.IteratedFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
h : AnalyticOn 𝕜 f univ
n : ℕ
σ : Perm (Fin n)
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (x : Fin n) ↦ E) F)
    (ContinuousMultilinearMap.domDomCongr σ (iteratedFDerivWithin 𝕜 n f univ x)) (iteratedFDerivWithin 𝕜 n f univ x)

Tactic:
exact h.domDomCongr_iteratedFDerivWithin uniqueDiffOn_univ (mem_univ x) _

Premises used: AnalyticOn.domDomCongr_iteratedFDerivWithin, uniqueDiffOn_univ, Set.mem_univ
-- Module: Mathlib.Analysis.Analytic.IteratedFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
h : ContDiffAt 𝕜 ω f x
n : ℕ
v : Fin n → E
σ : Perm (Fin n)
rw :
  Eq.{u_3 + 1} (α := F)
    ((iteratedFDerivWithin 𝕜 n f univ x : (a : (i : Fin n) → E) → F) (v ∘ (⇑σ : (a : Fin n) → Fin n)) : F)
    ((iteratedFDerivWithin 𝕜 n f univ x : (a : (i : Fin n) → E) → F) v : F)
⊢ Eq.{u_3 + 1} (α := F) ((iteratedFDeriv 𝕜 n f x : (a : (i : Fin n) → E) → F) (v ∘ (⇑σ : (a : Fin n) → Fin n)) : F)
    ((iteratedFDeriv 𝕜 n f x : (a : (i : Fin n) → E) → F) v : F)

Tactic:
rw [← iteratedFDerivWithin_univ]

Premises used: iteratedFDerivWithin_univ
-- Module: Mathlib.Analysis.Analytic.IteratedFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
h : ContDiffAt 𝕜 ω f x
n : ℕ
v : Fin n → E
σ : Perm (Fin n)
⊢ Eq.{u_3 + 1} (α := F)
    ((iteratedFDerivWithin 𝕜 n f univ x : (a : (i : Fin n) → E) → F) (v ∘ (⇑σ : (a : Fin n) → Fin n)) : F)
    ((iteratedFDerivWithin 𝕜 n f univ x : (a : (i : Fin n) → E) → F) v : F)

Tactic:
h.iteratedFDerivWithin_comp_perm uniqueDiffOn_univ (mem_univ x) _ _

Premises used: uniqueDiffOn_univ, Set.mem_univ, ContDiffWithinAt.iteratedFDerivWithin_comp_perm
-- Module: Mathlib.Analysis.Analytic.IteratedFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
h : ContDiffAt 𝕜 ω f x
n : ℕ
v : Fin n → E
σ : Perm (Fin n)
⊢ Eq.{u_3 + 1} (α := F)
    ((iteratedFDerivWithin 𝕜 n f univ x : (a : (i : Fin n) → E) → F) (v ∘ (⇑σ : (a : Fin n) → Fin n)) : F)
    ((iteratedFDerivWithin 𝕜 n f univ x : (a : (i : Fin n) → E) → F) v : F)

Tactic:
exact h.iteratedFDerivWithin_comp_perm uniqueDiffOn_univ (mem_univ x) _ _

Premises used: uniqueDiffOn_univ, Set.mem_univ, ContDiffWithinAt.iteratedFDerivWithin_comp_perm
-- Module: Mathlib.Analysis.Analytic.IteratedFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
h : ContDiffAt 𝕜 ω f x
n : ℕ
σ : Perm (Fin n)
rw :
  Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (x : Fin n) ↦ E) F)
    (ContinuousMultilinearMap.domDomCongr σ (iteratedFDerivWithin 𝕜 n f univ x)) (iteratedFDerivWithin 𝕜 n f univ x)
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (x : Fin n) ↦ E) F)
    (ContinuousMultilinearMap.domDomCongr σ (iteratedFDeriv 𝕜 n f x)) (iteratedFDeriv 𝕜 n f x)

Tactic:
rw [← iteratedFDerivWithin_univ]

Premises used: iteratedFDerivWithin_univ
-- Module: Mathlib.Analysis.Analytic.IteratedFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
h : ContDiffAt 𝕜 ω f x
n : ℕ
σ : Perm (Fin n)
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (x : Fin n) ↦ E) F)
    (ContinuousMultilinearMap.domDomCongr σ (iteratedFDerivWithin 𝕜 n f univ x)) (iteratedFDerivWithin 𝕜 n f univ x)

Tactic:
h.domDomCongr_iteratedFDerivWithin uniqueDiffOn_univ (mem_univ x) _

Premises used: ContDiffWithinAt.domDomCongr_iteratedFDerivWithin, uniqueDiffOn_univ, Set.mem_univ
-- Module: Mathlib.Analysis.Analytic.IteratedFDeriv
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → F
x : E
h : ContDiffAt 𝕜 ω f x
n : ℕ
σ : Perm (Fin n)
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (x : Fin n) ↦ E) F)
    (ContinuousMultilinearMap.domDomCongr σ (iteratedFDerivWithin 𝕜 n f univ x)) (iteratedFDerivWithin 𝕜 n f univ x)

Tactic:
exact h.domDomCongr_iteratedFDerivWithin uniqueDiffOn_univ (mem_univ x) _

Premises used: ContDiffWithinAt.domDomCongr_iteratedFDerivWithin, uniqueDiffOn_univ, Set.mem_univ
-- Module: Mathlib.Analysis.Analytic.Linear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E →L[𝕜] F
x : E
⊢ (f.fpowerSeries x).radius = ∞

Tactic:
(f.fpowerSeries x).radius_eq_top_of_forall_image_add_eq_zero 2 fun _ => rfl

Premises used: ContinuousLinearMap.fpowerSeries, FormalMultilinearSeries.radius_eq_top_of_forall_image_add_eq_zero, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Analytic.Linear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E →L[𝕜] F
x : E
⊢ ∞ ≤ (f.fpowerSeries x).radius

Tactic:
simp
-- Module: Mathlib.Analysis.Analytic.Linear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E →L[𝕜] F
x y : E
h : Membership.mem (γ := Set E) (Metric.eball 0 ∞) y
⊢ HasSum (fun (n : ℕ) ↦ (f.fpowerSeries x (n + 2) : (a : (i : Fin (n + 2)) → E) → F) fun (x : Fin (n + 2)) ↦ y)
    (HSub.hSub (α := F) (β := F) ((f : (a : E) → F) (x + y) : F)
      (∑ i ∈ Finset.range 2, (f.fpowerSeries x i : (a : (i : Fin i) → E) → F) fun (x : Fin i) ↦ y : F))

Tactic:
simp [Finset.sum_range_succ, hasSum_zero, fpowerSeries]

Premises used: ContinuousLinearMap.fpowerSeries, hasSum_zero, Finset.sum_range_succ
-- Module: Mathlib.Analysis.Analytic.Linear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E →L[𝕜] F
x : E
m : ℕ
hm : LE.le (α := ℕ) 2 0
linarith : HMul.hMul (α := ℤ) 2 (-1) + HSub.hSub (α := ℤ) 2 0 = 0
linarith₁ : GT.gt (α := ℤ) 2 0
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 0) ↦ E) F) (f.fpowerSeries x 0) 0

Tactic:
linarith
-- Module: Mathlib.Analysis.Analytic.Linear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E →L[𝕜] F
x : E
m : ℕ
hm : LE.le (α := ℕ) 2 1
linarith : -1 + HSub.hSub (α := ℤ) 2 1 = 0
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin 1) ↦ E) F) (f.fpowerSeries x 1) 0

Tactic:
linarith
-- Module: Mathlib.Analysis.Analytic.Linear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E →L[𝕜] F
x : E
m n : ℕ
hm : 2 ≤ n + 2
⊢ Eq (α := ContinuousMultilinearMap.{u_1, 0, u_2, u_3} 𝕜 (fun (i : Fin (n + 2)) ↦ E) F) (f.fpowerSeries x (n + 2)) 0

Tactic:
simp [fpowerSeries]

Premises used: ContinuousLinearMap.fpowerSeries
-- Module: Mathlib.Analysis.Analytic.Linear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E →L[𝕜] F
x : E
m : ℕ
hm : 2 ≤ m
⊢ f.fpowerSeries x m = 0

Tactic:
match m with
    | 0 | 1 => linarith
    | n + 2 => simp [fpowerSeries]
-- Module: Mathlib.Analysis.Analytic.Linear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E →L[𝕜] F
x : E
⊢ HasFPowerSeriesOnBall (⇑f : (a : E) → F) (f.fpowerSeries x) x ∞

Tactic:
(f.hasFiniteFPowerSeriesOnBall x).toHasFPowerSeriesOnBall

Premises used: HasFiniteFPowerSeriesOnBall.toHasFPowerSeriesOnBall, ContinuousLinearMap.hasFiniteFPowerSeriesOnBall
-- Module: Mathlib.Analysis.Analytic.Linear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E →L[𝕜] F
x : E
⊢ HasFPowerSeriesAt (⇑f : (a : E) → F) (f.fpowerSeries x) x

Tactic:
⟨∞, f.hasFPowerSeriesOnBall x⟩

Premises used: ContinuousLinearMap.hasFPowerSeriesOnBall, Exists.intro, HasFPowerSeriesAt, Top.top
-- Module: Mathlib.Analysis.Analytic.Linear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E →L[𝕜] F
x : E
⊢ CPolynomialAt.{u_1, u_2, u_3} 𝕜 (F := F) (⇑f : (a : E) → F) x

Tactic:
(f.hasFiniteFPowerSeriesOnBall x).cpolynomialAt

Premises used: HasFiniteFPowerSeriesOnBall.cpolynomialAt, ContinuousLinearMap.hasFiniteFPowerSeriesOnBall
-- Module: Mathlib.Analysis.Analytic.Linear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E →L[𝕜] F
x : E
⊢ AnalyticAt.{u_1, u_2, u_3} 𝕜 (F := F) (⇑f : (a : E) → F) x

Tactic:
(f.hasFPowerSeriesAt x).analyticAt

Premises used: ContinuousLinearMap.hasFPowerSeriesAt, HasFPowerSeriesAt.analyticAt
-- Module: Mathlib.Analysis.Analytic.Linear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E →L[𝕜] F
s : Set E
⊢ CPolynomialOn.{u_1, u_2, u_3} 𝕜 (F := F) (⇑f : (a : E) → F) s

Tactic:
fun x _ ↦ f.cpolynomialAt x

Premises used: ContinuousLinearMap.cpolynomialAt, CPolynomialOn
-- Module: Mathlib.Analysis.Analytic.Linear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E →L[𝕜] F
s : Set E
⊢ AnalyticOnNhd.{u_1, u_2, u_3} 𝕜 (F := F) (⇑f : (a : E) → F) s

Tactic:
fun x _ ↦ f.analyticAt x

Premises used: AnalyticOnNhd, ContinuousLinearMap.analyticAt
-- Module: Mathlib.Analysis.Analytic.Linear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E →L[𝕜] F
s : Set E
x : E
⊢ AnalyticWithinAt.{u_1, u_2, u_3} 𝕜 (F := F) (⇑f : (a : E) → F) s x

Tactic:
(f.analyticAt x).analyticWithinAt

Premises used: ContinuousLinearMap.analyticAt, AnalyticAt.analyticWithinAt
-- Module: Mathlib.Analysis.Analytic.Linear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E →L[𝕜] F
s : Set E
⊢ AnalyticOn.{u_1, u_2, u_3} 𝕜 (F := F) (⇑f : (a : E) → F) s

Tactic:
fun x _ ↦ f.analyticWithinAt _ x

Premises used: ContinuousLinearMap.analyticWithinAt, AnalyticOn
-- Module: Mathlib.Analysis.Analytic.Linear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E →L[𝕜] F →L[𝕜] G
m : Fin 2 → E × F
⊢ Eq.{u_4 + 1} (α := G) ((f.uncurryBilinear : (a : (i : Fin 2) → E × F) → G) m : G)
    ((((f : (a : E) → F →L[𝕜] G) (m 0).1 : F →L[𝕜] G) : (a : F) → G) (m 1).2 : G)

Tactic:
rfl

Premises used: Fin.succ, Fin.ofNat, rfl
-- Module: Mathlib.Analysis.Analytic.Linear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E →L[𝕜] F →L[𝕜] G
x : E × F
⊢ Eq (α := ContinuousMultilinearMap 𝕜 (fun (i : Fin 0) ↦ E × F) G) (f.fpowerSeriesBilinear x 0)
    (ContinuousMultilinearMap.uncurry0 𝕜 (E × F) ((((f : (a : E) → F →L[𝕜] G) x.1 : F →L[𝕜] G) : (a : F) → G) x.2))

Tactic:
rfl

Premises used: ContinuousLinearMap.fpowerSeriesBilinear, rfl
-- Module: Mathlib.Analysis.Analytic.Linear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E →L[𝕜] F →L[𝕜] G
x : E × F
⊢ Eq (α := ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E × F) G) (f.fpowerSeriesBilinear x 1)
    ((LinearIsometryEquiv.symm (continuousMultilinearCurryFin1 𝕜 (E × F) G) :
        (a : E × F →L[𝕜] G) → ContinuousMultilinearMap 𝕜 (fun (i : Fin 1) ↦ E × F) G)
      ((f.deriv₂ : (a : E × F) → E × F →L[𝕜] G) x))

Tactic:
rfl

Premises used: ContinuousLinearMap.fpowerSeriesBilinear, rfl
-- Module: Mathlib.Analysis.Analytic.Linear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E →L[𝕜] F →L[𝕜] G
x : E × F
⊢ f.fpowerSeriesBilinear x 2 = f.uncurryBilinear

Tactic:
rfl

Premises used: ContinuousLinearMap.fpowerSeriesBilinear, rfl
-- Module: Mathlib.Analysis.Analytic.Linear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E →L[𝕜] F →L[𝕜] G
x : E × F
n : ℕ
⊢ Eq (α := ContinuousMultilinearMap 𝕜 (fun (i : Fin (n + 3)) ↦ E × F) G) (f.fpowerSeriesBilinear x (n + 3)) 0

Tactic:
rfl

Premises used: ContinuousLinearMap.fpowerSeriesBilinear, rfl
-- Module: Mathlib.Analysis.Analytic.Linear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E →L[𝕜] F →L[𝕜] G
x : E × F
⊢ (f.fpowerSeriesBilinear x).radius (𝕜 := 𝕜) (E := E × F) (F := G) = ∞

Tactic:
(f.fpowerSeriesBilinear x).radius_eq_top_of_forall_image_add_eq_zero 3 fun _ => rfl

Premises used: ContinuousLinearMap.fpowerSeriesBilinear, FormalMultilinearSeries.radius_eq_top_of_forall_image_add_eq_zero, OfNat.ofNat, rfl
-- Module: Mathlib.Analysis.Analytic.Linear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E →L[𝕜] F →L[𝕜] G
x : E × F
⊢ ∞ ≤ (f.fpowerSeriesBilinear x).radius (𝕜 := 𝕜) (E := E × F) (F := G)

Tactic:
simp
-- Module: Mathlib.Analysis.Analytic.Linear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E →L[𝕜] F →L[𝕜] G
x y : E × F
h : Membership.mem (γ := Set (E × F)) (Metric.eball 0 ∞) y
simp :
  HasSum
    (fun (n : ℕ) ↦ (f.fpowerSeriesBilinear x (n + 3) : (a : (i : Fin (n + 3)) → E × F) → G) fun (x : Fin (n + 3)) ↦ y)
    (HAdd.hAdd (β := G)
        (HAdd.hAdd (α := G) (β := G) ((((f : (a : E) → F →L[𝕜] G) x.1 : F →L[𝕜] G) : (a : F) → G) x.2 : G)
          ((((f.deriv₂ : (a : E × F) → E × F →L[𝕜] G) (x.1, x.2) : E × F →L[𝕜] G) : (a : E × F) → G) (y.1, y.2) : G))
        ((((f : (a : E) → F →L[𝕜] G) y.1 : F →L[𝕜] G) : (a : F) → G) y.2 : G) -
      HAdd.hAdd (β := G)
        (HAdd.hAdd (β := G)
          (HAdd.hAdd (α := G) (β := G)
            (∑ i ∈ Finset.range 0, (f.fpowerSeriesBilinear x i : (a : (i : Fin i) → E × F) → G) fun (x : Fin i) ↦ y : G)
            ((f.fpowerSeriesBilinear x 0 : (a : (i : Fin 0) → E × F) → G) fun (x : Fin 0) ↦ y : G))
          ((f.fpowerSeriesBilinear x 1 : (a : (i : Fin 1) → E × F) → G) fun (x : Fin 1) ↦ y : G))
        ((f.fpowerSeriesBilinear x 2 : (a : (i : Fin 2) → E × F) → G) fun (x : Fin 2) ↦ y : G))
⊢ HasSum
    (fun (n : ℕ) ↦ (f.fpowerSeriesBilinear x (n + 3) : (a : (i : Fin (n + 3)) → E × F) → G) fun (x : Fin (n + 3)) ↦ y)
    (HSub.hSub (α := G) (β := G) ((((f : (a : E) → F →L[𝕜] G) (x + y).1 : F →L[𝕜] G) : (a : F) → G) (x + y).2 : G)
      (∑ i ∈ Finset.range 3, (f.fpowerSeriesBilinear x i : (a : (i : Fin i) → E × F) → G) fun (x : Fin i) ↦ y : G))

Tactic:
simp only [Finset.sum_range_succ, Prod.fst_add, Prod.snd_add, f.map_add_add]

Premises used: ContinuousLinearMap.map_add_add, Prod.fst_add, Finset.sum_range_succ, Prod.snd_add
-- Module: Mathlib.Analysis.Analytic.Linear
Goal:
𝕜 : Type u_1
inst : NontriviallyNormedField 𝕜
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
F : Type u_3
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
G : Type u_4
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
f : E →L[𝕜] F →L[𝕜] G
x y : E × F
h : Membership.mem (γ := Set (E × F)) (Metric.eball 0 ∞) y
⊢ HasSum
    (fun (n : ℕ) ↦ (f.fpowerSeriesBilinear x (n + 3) : (a : (i : Fin (n + 3)) → E × F) → G) fun (x : Fin (n + 3)) ↦ y)
    (HAdd.hAdd (β := G)
        (HAdd.hAdd (α := G) (β := G) ((((f : (a : E) → F →L[𝕜] G) x.1 : F →L[𝕜] G) : (a : F) → G) x.2 : G)
          ((((f.deriv₂ : (a : E × F) → E × F →L[𝕜] G) (x.1, x.2) : E × F →L[𝕜] G) : (a : E × F) → G) (y.1, y.2) : G))
        ((((f : (a : E) → F →L[𝕜] G) y.1 : F →L[𝕜] G) : (a : F) → G) y.2 : G) -
      HAdd.hAdd (β := G)
        (HAdd.hAdd (β := G)
          (HAdd.hAdd (α := G) (β := G)
            (∑ i ∈ Finset.range 0, (f.fpowerSeriesBilinear x i : (a : (i : Fin i) → E × F) → G) fun (x : Fin i) ↦ y : G)
            ((f.fpowerSeriesBilinear x 0 : (a : (i : Fin 0) → E × F) → G) fun (x : Fin 0) ↦ y : G))
          ((f.fpowerSeriesBilinear x 1 : (a : (i : Fin 1) → E × F) → G) fun (x : Fin 1) ↦ y : G))
        ((f.fpowerSeriesBilinear x 2 : (a : (i : Fin 2) → E × F) → G) fun (x : Fin 2) ↦ y : G))

Tactic:
simp [fpowerSeriesBilinear, hasSum_zero]

Premises used: ContinuousLinearMap.fpowerSeriesBilinear, hasSum_zero