awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
α : Type u_9
A : Type u_10
inst_3 : NormedCommRing A
inst_4 : NormedAlgebra 𝕜 A
f : α → E → A
c : E
N : Finset α
h : ∀ n ∈ N, AnalyticAt 𝕜 (f n) c
x : E
⊢ Eq.{u_10 + 1} (α := A) ((∏ n ∈ N, f n) x) (∏ n ∈ N, f n x)

Tactic:
simp
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
α : Type u_1
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
A : Type u_9
inst_3 : NormedCommRing A
inst_4 : NormedAlgebra 𝕜 A
f : α → E → A
s : Set E
N : Finset α
h : ∀ n ∈ N, AnalyticOn 𝕜 (f n) s
⊢ AnalyticOn.{u_2, u_3, u_9} 𝕜 (F := A) (fun (z : E) ↦ ∏ n ∈ N, f n z) s

Tactic:
fun z zs ↦ N.analyticWithinAt_fun_prod (fun n m ↦ h n m z zs)

Premises used: AnalyticOn, Finset.analyticWithinAt_fun_prod
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
α : Type u_1
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
A : Type u_9
inst_3 : NormedCommRing A
inst_4 : NormedAlgebra 𝕜 A
f : α → E → A
s : Set E
N : Finset α
h : ∀ n ∈ N, AnalyticOn 𝕜 (f n) s
⊢ AnalyticOn.{u_2, u_3, u_9} 𝕜 (F := A) (∏ n ∈ N, f n) s

Tactic:
fun z zs ↦ N.analyticWithinAt_prod (fun n m ↦ h n m z zs)

Premises used: AnalyticOn, Finset.analyticWithinAt_prod
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
α : Type u_1
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
A : Type u_9
inst_3 : NormedCommRing A
inst_4 : NormedAlgebra 𝕜 A
f : α → E → A
s : Set E
N : Finset α
h : ∀ n ∈ N, AnalyticOnNhd 𝕜 (f n) s
⊢ AnalyticOnNhd.{u_2, u_3, u_9} 𝕜 (F := A) (fun (z : E) ↦ ∏ n ∈ N, f n z) s

Tactic:
fun z zs ↦ N.analyticAt_fun_prod (fun n m ↦ h n m z zs)

Premises used: AnalyticOnNhd, Finset.analyticAt_fun_prod
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
α : Type u_1
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
A : Type u_9
inst_3 : NormedCommRing A
inst_4 : NormedAlgebra 𝕜 A
f : α → E → A
s : Set E
N : Finset α
h : ∀ n ∈ N, AnalyticOnNhd 𝕜 (f n) s
⊢ AnalyticOnNhd.{u_2, u_3, u_9} 𝕜 (F := A) (∏ n ∈ N, f n) s

Tactic:
fun z zs ↦ N.analyticAt_prod (fun n m ↦ h n m z zs)

Premises used: AnalyticOnNhd, Finset.analyticAt_prod
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
α : Type u_9
A : Type u_10
inst_3 : NormedCommRing A
inst_4 : NormedAlgebra 𝕜 A
f : α → E → A
c : E
h : ∀ (a : α), AnalyticAt 𝕜 (f a) c
pos : ∀ (hf : (Function.mulSupport f).Finite), AnalyticAt.{u_2, u_3, u_10} 𝕜 (F := A) (∏ᶠ (n : α), f n) c
neg : ∀ (hf : ¬(Function.mulSupport f).Finite), AnalyticAt.{u_2, u_3, u_10} 𝕜 (F := A) (∏ᶠ (n : α), f n) c
⊢ AnalyticAt.{u_2, u_3, u_10} 𝕜 (F := A) (∏ᶠ (n : α), f n) c

Tactic:
by_cases hf : (Function.mulSupport f).Finite

Premises used: Set.Finite, Function.mulSupport
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
α : Type u_9
A : Type u_10
inst_3 : NormedCommRing A
inst_4 : NormedAlgebra 𝕜 A
f : α → E → A
c : E
h : ∀ (a : α), AnalyticAt 𝕜 (f a) c
hf : (Function.mulSupport f).Finite
⊢ AnalyticAt.{u_2, u_3, u_10} 𝕜 (F := A) (∏ᶠ (n : α), f n) c

Tactic:
simp_all [finprod_eq_prod _ hf, Finset.analyticAt_prod]

Premises used: Finset.analyticAt_prod, finprod_eq_prod
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
α : Type u_9
A : Type u_10
inst_3 : NormedCommRing A
inst_4 : NormedAlgebra 𝕜 A
f : α → E → A
c : E
h : ∀ (a : α), AnalyticAt 𝕜 (f a) c
hf : ¬(Function.mulSupport f).Finite
neg : AnalyticAt.{u_2, u_3, u_10} 𝕜 (F := A) 1 c
⊢ AnalyticAt.{u_2, u_3, u_10} 𝕜 (F := A) (∏ᶠ (n : α), f n) c

Tactic:
rw [finprod_of_infinite_mulSupport hf]

Premises used: finprod_of_infinite_mulSupport
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
α : Type u_9
A : Type u_10
inst_3 : NormedCommRing A
inst_4 : NormedAlgebra 𝕜 A
f : α → E → A
c : E
h : ∀ (a : α), AnalyticAt 𝕜 (f a) c
hf : ¬(Function.mulSupport f).Finite
⊢ AnalyticAt.{u_2, u_3, u_10} 𝕜 (F := A) 1 c

Tactic:
apply analyticAt_const

Premises used: analyticAt_const
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → E →L[𝕜] F
pf : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
s : Set E
x : E
r : ℝ≥0∞
z : F
hf : HasFPowerSeriesWithinOnBall (𝕜 := 𝕜) f pf s x r
rw : r ≤ pf.radius (𝕜 := 𝕜) (E := E) (F := E →L[𝕜] F)
⊢ r ≤ (pf.unshift z).radius

Tactic:
rw [FormalMultilinearSeries.radius_unshift]

Premises used: FormalMultilinearSeries.radius_unshift
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → E →L[𝕜] F
pf : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
s : Set E
x : E
r : ℝ≥0∞
z : F
hf : HasFPowerSeriesWithinOnBall (𝕜 := 𝕜) f pf s x r
⊢ r ≤ pf.radius (𝕜 := 𝕜) (E := E) (F := E →L[𝕜] F)

Tactic:
hf.r_le

Premises used: HasFPowerSeriesWithinOnBall.r_le
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → E →L[𝕜] F
pf : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
s : Set E
x : E
r : ℝ≥0∞
z : F
hf : HasFPowerSeriesWithinOnBall (𝕜 := 𝕜) f pf s x r
⊢ r ≤ pf.radius (𝕜 := 𝕜) (E := E) (F := E →L[𝕜] F)

Tactic:
exact hf.r_le

Premises used: HasFPowerSeriesWithinOnBall.r_le
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → E →L[𝕜] F
pf : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
s : Set E
x : E
r : ℝ≥0∞
z : F
hf : HasFPowerSeriesWithinOnBall (𝕜 := 𝕜) f pf s x r
y : E
hy : x + y ∈ insert x s
h'y : Membership.mem (γ := Set E) (Metric.eball 0 r) y
h :
  HasSum.{u_4, 0} (α := F)
    (fun (n : ℕ) ↦ ((pf.unshift z (n + 1) : (a : (i : Fin (n + 1)) → E) → F) fun (x : Fin (n + 1)) ↦ y : F))
    ((f (x + y) : (a : E) → F) (x + y - x) : F)
⊢ HasSum (fun (n : ℕ) ↦ (pf.unshift z n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y)
    (HAdd.hAdd (β := F) z ((f (x + y) : (a : E) → F) (x + y - x) : F))

Tactic:
apply HasSum.zero_add

Premises used: HasSum.zero_add
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → E →L[𝕜] F
pf : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
s : Set E
x : E
r : ℝ≥0∞
z : F
hf : HasFPowerSeriesWithinOnBall (𝕜 := 𝕜) f pf s x r
y : E
hy : x + y ∈ insert x s
h'y : Membership.mem (γ := Set E) (Metric.eball 0 r) y
h :
  HasSum.{u_4, 0} (α := F)
    (fun (n : ℕ) ↦
      ((((pf n : (a : (i : Fin n) → E) → E →L[𝕜] F)
                (Fin.init (α := fun (i : Fin (n + 1)) ↦ E) fun (x : Fin (n + 1)) ↦ y) :
              E →L[𝕜] F) :
            (a : E) → F)
          y :
        F))
    ((f (x + y) : (a : E) → F) y : F)
⊢ HasSum.{u_4, 0} (α := F)
    (fun (n : ℕ) ↦ ((pf.unshift z (n + 1) : (a : (i : Fin (n + 1)) → E) → F) fun (x : Fin (n + 1)) ↦ y : F))
    ((f (x + y) : (a : E) → F) (x + y - x) : F)

Tactic:
simp only [FormalMultilinearSeries.unshift, Nat.succ_eq_add_one,
      continuousMultilinearCurryRightEquiv_symm_apply', add_sub_cancel_left]

Premises used: Nat.succ_eq_add_one, add_sub_cancel_left, continuousMultilinearCurryRightEquiv_symm_apply', FormalMultilinearSeries.unshift
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → E →L[𝕜] F
pf : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
s : Set E
x : E
r : ℝ≥0∞
z : F
hf : HasFPowerSeriesWithinOnBall (𝕜 := 𝕜) f pf s x r
y : E
hy : x + y ∈ insert x s
h'y : Membership.mem (γ := Set E) (Metric.eball 0 r) y
⊢ HasSum.{u_4, 0} (α := F)
    (fun (n : ℕ) ↦
      ((((pf n : (a : (i : Fin n) → E) → E →L[𝕜] F)
                (Fin.init (α := fun (i : Fin (n + 1)) ↦ E) fun (x : Fin (n + 1)) ↦ y) :
              E →L[𝕜] F) :
            (a : E) → F)
          y :
        F))
    ((f (x + y) : (a : E) → F) y : F)

Tactic:
(ContinuousLinearMap.apply 𝕜 F y).hasSum (hf.hasSum hy h'y)

Premises used: ContinuousLinearMap.hasSum, ContinuousLinearMap.apply, HasFPowerSeriesWithinOnBall.hasSum, DFunLike.coe
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → E →L[𝕜] F
pf : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
s : Set E
x : E
r : ℝ≥0∞
z : F
hf : HasFPowerSeriesWithinOnBall (𝕜 := 𝕜) f pf s x r
y : E
hy : x + y ∈ insert x s
h'y : Membership.mem (γ := Set E) (Metric.eball 0 r) y
⊢ HasSum.{u_4, 0} (α := F)
    (fun (n : ℕ) ↦
      ((((pf n : (a : (i : Fin n) → E) → E →L[𝕜] F)
                (Fin.init (α := fun (i : Fin (n + 1)) ↦ E) fun (x : Fin (n + 1)) ↦ y) :
              E →L[𝕜] F) :
            (a : E) → F)
          y :
        F))
    ((f (x + y) : (a : E) → F) y : F)

Tactic:
exact (ContinuousLinearMap.apply 𝕜 F y).hasSum (hf.hasSum hy h'y)

Premises used: ContinuousLinearMap.hasSum, ContinuousLinearMap.apply, HasFPowerSeriesWithinOnBall.hasSum, DFunLike.coe
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → E →L[𝕜] F
pf : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
x : E
r : ℝ≥0∞
z : F
hf : HasFPowerSeriesOnBall (𝕜 := 𝕜) f pf x r
rw : r ≤ pf.radius (𝕜 := 𝕜) (E := E) (F := E →L[𝕜] F)
⊢ r ≤ (pf.unshift z).radius

Tactic:
rw [FormalMultilinearSeries.radius_unshift]

Premises used: FormalMultilinearSeries.radius_unshift
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → E →L[𝕜] F
pf : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
x : E
r : ℝ≥0∞
z : F
hf : HasFPowerSeriesOnBall (𝕜 := 𝕜) f pf x r
⊢ r ≤ pf.radius (𝕜 := 𝕜) (E := E) (F := E →L[𝕜] F)

Tactic:
hf.r_le

Premises used: HasFPowerSeriesOnBall.r_le
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → E →L[𝕜] F
pf : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
x : E
r : ℝ≥0∞
z : F
hf : HasFPowerSeriesOnBall (𝕜 := 𝕜) f pf x r
⊢ r ≤ pf.radius (𝕜 := 𝕜) (E := E) (F := E →L[𝕜] F)

Tactic:
exact hf.r_le

Premises used: HasFPowerSeriesOnBall.r_le
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → E →L[𝕜] F
pf : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
x : E
r : ℝ≥0∞
z : F
hf : HasFPowerSeriesOnBall (𝕜 := 𝕜) f pf x r
y : E
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
h :
  HasSum.{u_4, 0} (α := F)
    (fun (n : ℕ) ↦ ((pf.unshift z (n + 1) : (a : (i : Fin (n + 1)) → E) → F) fun (x : Fin (n + 1)) ↦ y : F))
    ((f (x + y) : (a : E) → F) (x + y - x) : F)
⊢ HasSum (fun (n : ℕ) ↦ (pf.unshift z n : (a : (i : Fin n) → E) → F) fun (x : Fin n) ↦ y)
    (HAdd.hAdd (β := F) z ((f (x + y) : (a : E) → F) (x + y - x) : F))

Tactic:
apply HasSum.zero_add

Premises used: HasSum.zero_add
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → E →L[𝕜] F
pf : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
x : E
r : ℝ≥0∞
z : F
hf : HasFPowerSeriesOnBall (𝕜 := 𝕜) f pf x r
y : E
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
h :
  HasSum.{u_4, 0} (α := F)
    (fun (n : ℕ) ↦
      ((((pf n : (a : (i : Fin n) → E) → E →L[𝕜] F)
                (Fin.init (α := fun (i : Fin (n + 1)) ↦ E) fun (x : Fin (n + 1)) ↦ y) :
              E →L[𝕜] F) :
            (a : E) → F)
          y :
        F))
    ((f (x + y) : (a : E) → F) y : F)
⊢ HasSum.{u_4, 0} (α := F)
    (fun (n : ℕ) ↦ ((pf.unshift z (n + 1) : (a : (i : Fin (n + 1)) → E) → F) fun (x : Fin (n + 1)) ↦ y : F))
    ((f (x + y) : (a : E) → F) (x + y - x) : F)

Tactic:
simp only [FormalMultilinearSeries.unshift, Nat.succ_eq_add_one,
      continuousMultilinearCurryRightEquiv_symm_apply', add_sub_cancel_left]

Premises used: Nat.succ_eq_add_one, add_sub_cancel_left, continuousMultilinearCurryRightEquiv_symm_apply', FormalMultilinearSeries.unshift
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → E →L[𝕜] F
pf : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
x : E
r : ℝ≥0∞
z : F
hf : HasFPowerSeriesOnBall (𝕜 := 𝕜) f pf x r
y : E
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
⊢ HasSum.{u_4, 0} (α := F)
    (fun (n : ℕ) ↦
      ((((pf n : (a : (i : Fin n) → E) → E →L[𝕜] F)
                (Fin.init (α := fun (i : Fin (n + 1)) ↦ E) fun (x : Fin (n + 1)) ↦ y) :
              E →L[𝕜] F) :
            (a : E) → F)
          y :
        F))
    ((f (x + y) : (a : E) → F) y : F)

Tactic:
(ContinuousLinearMap.apply 𝕜 F y).hasSum (hf.hasSum hy)

Premises used: ContinuousLinearMap.hasSum, HasFPowerSeriesOnBall.hasSum, ContinuousLinearMap.apply, DFunLike.coe
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → E →L[𝕜] F
pf : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
x : E
r : ℝ≥0∞
z : F
hf : HasFPowerSeriesOnBall (𝕜 := 𝕜) f pf x r
y : E
hy : Membership.mem (γ := Set E) (Metric.eball 0 r) y
⊢ HasSum.{u_4, 0} (α := F)
    (fun (n : ℕ) ↦
      ((((pf n : (a : (i : Fin n) → E) → E →L[𝕜] F)
                (Fin.init (α := fun (i : Fin (n + 1)) ↦ E) fun (x : Fin (n + 1)) ↦ y) :
              E →L[𝕜] F) :
            (a : E) → F)
          y :
        F))
    ((f (x + y) : (a : E) → F) y : F)

Tactic:
exact (ContinuousLinearMap.apply 𝕜 F y).hasSum (hf.hasSum hy)

Premises used: ContinuousLinearMap.hasSum, HasFPowerSeriesOnBall.hasSum, ContinuousLinearMap.apply, DFunLike.coe
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
f : E → E →L[𝕜] F
pf : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)
s : Set E
x : E
z : F
hf : HasFPowerSeriesWithinAt (𝕜 := 𝕜) f pf s x
⊢ HasFPowerSeriesWithinAt (fun (y : E) ↦ HAdd.hAdd (β := F) z ((f y : (a : E) → F) (y - x) : F)) (pf.unshift z) s x

Tactic:
let ⟨_, hrf⟩ := hf
  hrf.unshift.hasFPowerSeriesWithinAt

Premises used: HasFPowerSeriesWithinOnBall.hasFPowerSeriesWithinAt, HSub.hSub, HasFPowerSeriesWithinOnBall.unshift, _private.0.HasFPowerSeriesWithinAt.unshift.match_1, HAdd.hAdd, HasFPowerSeriesWithinAt, DFunLike.coe, FormalMultilinearSeries.unshift
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
u : E →L[𝕜] F
f : F → G
pf : FormalMultilinearSeries 𝕜 F G
s : Set F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f pf s ((u : (a : E) → F) x) r
hab : r ≤ pf.radius
⊢ r / ‖u‖ₑ ≤ pf.radius / ‖u‖ₑ

Tactic:
gcongr
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
u : E →L[𝕜] F
f : F → G
pf : FormalMultilinearSeries 𝕜 F G
s : Set F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f pf s ((u : (a : E) → F) x) r
⊢ r ≤ pf.radius

Tactic:
hf.r_le

Premises used: HasFPowerSeriesWithinOnBall.r_le
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
u : E →L[𝕜] F
f : F → G
pf : FormalMultilinearSeries 𝕜 F G
s : Set F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f pf s ((u : (a : E) → F) x) r
⊢ r ≤ pf.radius

Tactic:
exact hf.r_le

Premises used: HasFPowerSeriesWithinOnBall.r_le
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
u : E →L[𝕜] F
f : F → G
pf : FormalMultilinearSeries 𝕜 F G
s : Set F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f pf s ((u : (a : E) → F) x) r
⊢ pf.radius / ‖u‖ₑ ≤ FormalMultilinearSeries.radius (pf.compContinuousLinearMap u)

Tactic:
pf.div_le_radius_compContinuousLinearMap _

Premises used: FormalMultilinearSeries.div_le_radius_compContinuousLinearMap
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
u : E →L[𝕜] F
f : F → G
pf : FormalMultilinearSeries 𝕜 F G
s : Set F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f pf s ((u : (a : E) → F) x) r
_ : r / ‖u‖ₑ ≤ pf.radius / ‖u‖ₑ
⊢ r / ‖u‖ₑ ≤ FormalMultilinearSeries.radius (pf.compContinuousLinearMap u)

Tactic:
calc
      _ ≤ pf.radius / ‖u‖ₑ := by
        gcongr
        exact hf.r_le
      _ ≤ _ := pf.div_le_radius_compContinuousLinearMap _

Premises used: FormalMultilinearSeries.radius, FormalMultilinearSeries.div_le_radius_compContinuousLinearMap
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
u : E →L[𝕜] F
f : F → G
pf : FormalMultilinearSeries 𝕜 F G
s : Set F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f pf s ((u : (a : E) → F) x) r
simp : ¬r = 0
⊢ 0 < r / ‖u‖ₑ

Tactic:
simp only [ENNReal.div_pos_iff, ne_eq, enorm_ne_top, not_false_eq_true, and_true]

Premises used: and_true, ENNReal.div_pos_iff, ne_eq, not_false_eq_true, enorm_ne_top
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
u : E →L[𝕜] F
f : F → G
pf : FormalMultilinearSeries 𝕜 F G
s : Set F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f pf s ((u : (a : E) → F) x) r
⊢ ¬r = 0

Tactic:
pos_iff_ne_zero.mp hf.r_pos

Premises used: Iff.mp, HasFPowerSeriesWithinOnBall.r_pos, pos_iff_ne_zero
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
u : E →L[𝕜] F
f : F → G
pf : FormalMultilinearSeries 𝕜 F G
s : Set F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f pf s ((u : (a : E) → F) x) r
⊢ ¬r = 0

Tactic:
exact pos_iff_ne_zero.mp hf.r_pos

Premises used: Iff.mp, HasFPowerSeriesWithinOnBall.r_pos, pos_iff_ne_zero
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
u : E →L[𝕜] F
f : F → G
pf : FormalMultilinearSeries 𝕜 F G
s : Set F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f pf s ((u : (a : E) → F) x) r
y : E
hy1 : Membership.mem (γ := Set E) (insert x ((⇑u : (a : E) → F) ⁻¹' s)) (x + y)
hy2 : Membership.mem (γ := Set E) (Metric.eball 0 (r / ‖u‖ₑ)) y
⊢ HasSum (fun (n : ℕ) ↦ (pf n : (a : (i : Fin n) → F) → G) fun (x : Fin n) ↦ ((↑u : E →ₗ[𝕜] F) : (a : E) → F) y)
    (f (HAdd.hAdd (α := F) (β := F) ((u : (a : E) → F) x : F) (((↑u : E →ₗ[𝕜] F) : (a : E) → F) y : F)))

Tactic:
hf.hasSum _ _

Premises used: HasFPowerSeriesWithinOnBall.hasSum
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
u : E →L[𝕜] F
f : F → G
pf : FormalMultilinearSeries 𝕜 F G
s : Set F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f pf s ((u : (a : E) → F) x) r
y : E
hy1 : Membership.mem (γ := Set E) (insert x ((⇑u : (a : E) → F) ⁻¹' s)) (x + y)
hy2 : Membership.mem (γ := Set E) (Metric.eball 0 (r / ‖u‖ₑ)) y
h :
  (f ∘ (⇑u : (a : E) → F)) (x + y) =
    f (HAdd.hAdd (α := F) (β := F) ((u : (a : E) → F) x : F) (((↑u : E →ₗ[𝕜] F) : (a : E) → F) y : F))
convert_2 :
  HAdd.hAdd (α := F) (β := F) ((u : (a : E) → F) x : F) (((↑u : E →ₗ[𝕜] F) : (a : E) → F) y : F) ∈
    insert (α := F) ((u : (a : E) → F) x : F) s
convert_3 : Membership.mem.{u_4, u_4} (α := F) (γ := Set F) (Metric.eball 0 r) (((↑u : E →ₗ[𝕜] F) : (a : E) → F) y : F)
⊢ HasSum (fun (n : ℕ) ↦ (pf.compContinuousLinearMap u n : (a : (i : Fin n) → E) → G) fun (x : Fin n) ↦ y)
    ((f ∘ (⇑u : (a : E) → F)) (x + y))

Tactic:
convert! hf.hasSum _ _

Premises used: HasFPowerSeriesWithinOnBall.hasSum
-- Module: Mathlib.Analysis.Analytic.Constructions
Goal:
𝕜 : Type u_2
inst : NontriviallyNormedField 𝕜
E : Type u_3
F : Type u_4
G : Type u_5
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace 𝕜 E
inst_3 : NormedAddCommGroup F
inst_4 : NormedSpace 𝕜 F
inst_5 : NormedAddCommGroup G
inst_6 : NormedSpace 𝕜 G
u : E →L[𝕜] F
f : F → G
pf : FormalMultilinearSeries 𝕜 F G
s : Set F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesWithinOnBall f pf s ((u : (a : E) → F) x) r
y : E
hy1 : Membership.mem (γ := Set E) (insert x ((⇑u : (a : E) → F) ⁻¹' s)) (x + y)
hy2 : Membership.mem (γ := Set E) (Metric.eball 0 (r / ‖u‖ₑ)) y
⊢ (f ∘ (⇑u : (a : E) → F)) (x + y) =
    f (HAdd.hAdd (α := F) (β := F) ((u : (a : E) → F) x : F) (((↑u : E →ₗ[𝕜] F) : (a : E) → F) y : F))

Tactic:
simp